استدلال خودکار: رضایت پذیری

در این دوره یاد خواهید گرفت که چگونه از ابزارهای رضایتمندی (SAT/SMT) برای حل طیف وسیعی از مسائل استفاده کنید. چندین مثال اساسی برای به دست آوردن طعم برنامه ها ارائه شده است: مستطیل های مناسب برای چاپ پوستر، مشکلات زمان بندی، حل پازل ها و صحت برنامه. همچنین، نظریه اساسی ارائه شده است: وضوح به عنوان یک رویکرد اساسی برای رضایت‌پذیری گزاره، چارچوب CDCL برای مقیاس‌بندی برای فرمول‌های بزرگ، و روش سیمپلکس برای مقابله با نابرابری‌های خطی. رویکرد سبک برای دنبال کردن دوره استدلال خودکار: رضایت‌مندی، فقط تماشای سخنرانی‌ها و انجام آزمون‌های مربوطه است. برای دریافت طعمی از موضوع، ممکن است این کار به خوبی انجام شود. با این حال، رویکرد بسیار جالب‌تر این است که از این به عنوان مبنایی برای اعمال SAT/SMT بر روی چندین مشکل استفاده کنید، به عنوان مثال در مورد مشکلات ارائه شده در تکلیف افتخار.