Friday December 23 2011, at 11h00 in Celestijnenlaan 200A (room 05.001)
Programming with Boolean Satisfaction
by Professor Mike Codish (Ben-Gurion University of the Negev)
In recent years, research on Boolean satisfiability (SAT) is generating remarkably powerful SAT solvers capable of handling larger and larger SAT instances. With the availability of progressively stronger SAT solvers, an accumulating number of applications have been developed which demonstrate that real world problems can often be solved by encoding them into SAT.
Tailgating the success of SAT technology are a variety of tools which can be applied to help specify and then compile problem instances to corresponding SAT instances. Typically, a constraint based modeling language is introduced and used to model instances. Then encoding techniques are applied to compile constraints to the language of an underlying solver such as SAT, SMT, or others.
In this talk I introduce the need for "optimizing compilers" for SAT encoding. I present a new technique called "equi-propagation" and describe how it is applied to improve SAT encodings. I survey recent applications to demonstrate the power of this optimization technique.