Theoretical Foundations of SAT/SMT Solving

This workshop is shared between the programs Satisfiability: Theory, Practice, and Beyond and Theoretical Foundations of Computer Systems.

Boolean satisfiability is a canonical hard problem: not only is it NP-complete, but we do not expect to have any algorithms for it that even slightly outperform exhaustive search in the worst case. Moreover, determining the satisfiability of certain simple formulas is provably hard for Resolution, the underlying proof system of most modern SAT solvers. This stands in stark contrast to the practical success of SAT solvers. Nowadays, they are used to solve industrial problems with millions of variables and tens of millions of clauses; the US Federal Communications Commission used SAT solvers to run its multibillion-dollar broadcast incentive auction. SAT solvers have been used to verify the London train system and schedule exams in large universities, and they are routinely used to verify large hardware subsystems. They have been used in proving combinatorial conjectures — for example, that it is possible to color the numbers 1 to 7,824 in two colors such that no Pythagorean triple of them consists of numbers of the same color, yet there is no such coloring for the numbers 1 to 7,825 — and there are combinatorial statements such as the Williamson conjecture that posits the existence of a certain special class of Hadamard matrices. Further, the architecture of conflict-driven clause-learning (CDCL) SAT solvers forms the basis of modern SMT solvers, a class of solvers for first-order theories critical to the success of many program analysis, testing, and verification methods.

This workshop will focus on the mystery of this drastic gap between the predicted theoretical hardness of SAT and related problems and the unreasonable success of heuristics on their practical instances. We expect the themes to range from the discussion of the special structure in practical instances and their distributions that might make them easier for heuristics, to theoretical characterizations of hard examples and complexity of restricted problems, to the interplay among the success of various solver heuristic types, properties of instances, and encoding strategies.

In response to the COVID-19 pandemic, Simons Institute events are currently taking place online. Please register to receive the Zoom webinar access details.

This workshop will take place every Wednesday from 8:30 a.m. - 10:30 a.m. (PST) starting February 10. 

If you require accommodation for communication, please contact our access coordinator at simonsevents [at] berkeley.edu with as much advance notice as possible.