Beyond Satisfiability

There are at least two good reasons why breaking the boundaries of satisfiability is a timely proposal worthy of study. First, despite the universal expressive power of Boolean satisfiability for NP problems, expressing constraints as linear or even polynomial equations and inequalities over appropriate numeric domains is sometimes more natural and direct. It is thus natural to ask how algebraic or semialgebraic approaches to optimization and integer programming problems compare with pure SAT methods or how they can overcome the known theoretical limitations of SAT methods. Second, the range of combinatorial or optimization problems that researchers want to solve do not always fall within NP (e.g., QBF or SMT solving). Some of these problems may be efficiently solvable in the presence of an NP-oracle (i.e., they fall within the second level of the polynomial-time hierarchy), in which case using a solver for NP problems as an oracle could yield a solver for them. Recent examples where this has occurred with spectacular success include the problems of approximate counting or sampling solutions of a CNF formula. Pushing this line of reasoning even further, one may ask whether the methods that work well for satisfiability could be extended to solving quantified Boolean formulas (the canonical PSPACE-complete problem), which could have significant impact for systems verification tasks. The aim of this workshop is to explore the theoretical and practical challenges that underlie these and other ways of expanding the applicability of satisfiability methods beyond NP.

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

This workshop will take place every Tuesday from 8:30 a.m. to 10:30 a.m. (PDT).

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