Всеволод Опарин

Мощность SAT-солверов с запоминанием клозов и перезапусками

Мы изучим работу SAT-солвера с запоминанием клозов на невыполнимых формулах. Алгоритм будет рассмотрен как система доказательств. Ключевой вопрос: достаточно ли сильна такая система, чтобы иметь доказательства невыполнимости настолько же короткие как резолюционные?

Как окажется, любое резолюционное доказательство можно проэмулировать SAT-солвером, раздув его не более чем в полином.

Доклад по статье Knot Pipatsrisawat and Adnan Darwiche "On the Power of Clause-Learning SAT Solvers with Restarts".