Spring 2021

Theoretical Foundations of SAT/SMT Solving

Feb. 22Feb. 26, 2021

Add to Calendar

Antonina Kolokolova (Memorial University of Newfoundland; co-chair), Moshe Vardi (Rice University; co-chair), Maria Luisa Bonet (Universidad Politécnica de Cataluña), Vijay Ganesh (University of Waterloo), Marijn Heule (Carnegie Mellon University), Kevin Leyton-Brown (University of British Columbia)

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 multi-billion-dollar broadcast incentive auction. SAT solvers have been used to verify the London train system, schedule exams in large universities, and are routinely used to verify large hardware sub-systems. They have been used in proving combinatorial conjectures, for example, that it is possible to color the numbers 1 to 7824 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 7825, and there are combinatorial statements such as the Williamson conjecture that posits the existence of 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 between the success of various solver heuristic types, properties of instances, and encoding strategies.

All events take place in the Calvin Lab auditorium.

Further details about this workshop will be posted in due course. Enquiries may be sent to the organizers workshop-sat-tfcs [at] (at this address).