Programming with Boolean Satisfaction

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 advocate the need for “optimizing compilers” for SAT encoding and present

BEE

(“

B

en-Gurion University

E

qui-propagation

E

ncoder”). Using

BEE

eases the encoding process and performs optimizations to simplify constraints prior to their encoding to CNF. I will describe these optimizations: equi-propagation, partial evaluation, and decomposition, and demonstrate their application.

BEE

is written in Prolog, and integrates directly with a SAT solver through a suitable Prolog interface, or else it outputs a DIMACS file.