Presentation slides:
Sam Buss
Extending SAT Solvers with Extended Resolution
Eduard Čech Lecture
Institute of Mathematics,
Czech Academic of Sciences
April 17, 2024.
Download
talk slides.
Related papers:
1. DRAT and Propagation
Redundancy Proofs Without New Variables
(joint with N. Thapen).
2. Extended Resolution
Learning Via Dual Implication Points
(with J. Chung, V. Ganesh and A. Oliveras).
Abstract:
Conflict-driven clause learning (CDCL) algorithms for
Satisfiability (SAT Solvers) are surprisingly successful in solving
large-scale problems, but are limited by the fact that they can generate
only resolution refutations. Extended resolution, which allows the
iterated introduction of new definitions, can be a much more powerful
proof system. However, we lack good SAT solver heuristics for searching for
extended resolution refutations. This talk will discuss progress towards
the effective use of extended resolution. This includes DRAT proofs,
propagation redundancy proofs, and recent work on dual implication
points. The last is based on a novel method for analyzing conflict
graphs to identify candidates for extension variables.
Parts of this talk are joint works with Neil Thapen and with
Jonathan Chung, Vijay Ganesh, and Albert Oliveras.