Всеволод Опарин
Мощность SAT-солверов с запоминанием клозов и перезапусками
Мы изучим работу SAT-солвера с запоминанием клозов на невыполнимых формулах. Алгоритм будет рассмотрен как система доказательств. Ключевой вопрос: достаточно ли сильна такая система, чтобы иметь доказательства невыполнимости настолько же короткие как резолюционные?
Как окажется, любое резолюционное доказательство можно проэмулировать SAT-солвером, раздув его не более чем в полином.
Доклад по статье Knot Pipatsrisawat and Adnan Darwiche "On the Power of Clause-Learning SAT Solvers with Restarts".