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.
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-sat1 [at] lists.simons.berkeley.edu (at this address).