آموزش استدلال خودکار: مسئله ارضای پذیری (Satisfiability) - آخرین آپدیت

مبانی SAT/SMT و مثال‌های SAT SAT/SMT basics, SAT examples

• مقدمه عمومی و کاربرد در چاپ پوستر General introduction, and an application to poster printing

• مقدمه‌ای بر SAT Introduction to SAT

• نحو (Syntax) و ابزارهای SMT SMT syntax and tools

• مسئله هشت وزیر Eight queens problem

• حساب دودویی: جمع Binary Arithmetic: addition

• حساب دودویی: ضرب Binary Arithmetic: multiplication

کاربردهای SMT SMT applications

• جایگذاری مستطیل‌ها Rectangle fitting

• حل سودوکو Solving Sudoku

• زمان‌بندی Scheduling

• بررسی مدل محدود (Bounded Model Checking) Bounded model checking

تئوری و الگوریتم‌های SAT مبتنی بر CNF Theory and algorithms for CNF-based SAT

• روش حل (Resolution) Resolution

• مثالی از روش حل Example of resolution

• الگوریتم DPLL DPLL

• تبدیل DPLL به روش حل Transforming DPLL to resolution

• مبانی CDCL CDCL basics

• بهینه‌سازی‌های CDCL CDCL optimizations

تئوری و الگوریتم‌های SAT/SMT Theory and algorithms for SAT/SMT

• تبدیل یک فرمول گزاره‌ای به CNF Transforming a propositional formula to CNF

• تبدیل تسایتین (Tseitin transformation) The Tseitin transfomation

• مقدمه‌ای بر روش سیمپلکس Introduction to the Simplex method

• بهینه‌سازی با روش سیمپلکس Optimizing by the Simplex method

• بررسی امکان‌پذیری با روش سیمپلکس Checking feasibility by the Simplex method

• روش سیمپلکس و SMT The Simplex method and SMT