Candidate: Jonathan Chung
Date: August 15, 2023
Time: 3:00 pm
Location: remote attendance
Supervisor(s): Arie Gurfinkel
Abstract
In spite of the fact that the SAT problem has been theoretically demonstrated to be intractable in the worst case (requiring exponential time), modern SAT solvers routinely solve problem instances containing millions of variables and constraints in practice. The impressive performance of modern SAT solvers on real-life SAT instances is, in part, made possible by a combination of many heuristics integrated into each component of the solvers. Although there has already been a monumental research effort in the development of SAT solvers, there is still room for improvement, even in critical areas of currently dominant SAT solving algorithms.
One candidate for improvement is the Boolean Constraint Propagation (BCP) algorithm, which systematically finds implications of variable assignments made by the solver. The traditional algorithm for BCP propagates variables greedily, in the order that their unit clauses are discovered. In this work, we develop an algorithm which allows BCP to prioritize propagations, choose a heuristic priority ordering of the variables, and demonstrate a class of instances where our prioritized BCP algorithm, combined with this heuristic ordering, is able to outperform the traditional BCP algorithm.
It is also possible to introduce new elements into the structure of SAT solving algorithms. The Extended Resolution (ER) proof system is theoretically stronger than the proof system underlying modern SAT solvers, so it is natural to try integrating ER into SAT solvers. We show that ER can be implemented into modern SAT solvers by the addition of three new major components, and we use this framework to test various ideas and heuristics for defining and using extension variables. One of our considered heuristics is shown to be generally competitive with the original solver while improving upon the baseline for a specific class of instances.