On the bridge between Constraint Satisfaction and Boolean Satisfiability

VCLA and the Wolfgang Pauli Institute hosted a talk by Justyna Petke on May 30th, 2012

ABSTRACT

In the quest to find a general solving tool for combinatorial search problems the area of constraint programming has been developed. It has been successfully applied to many domains such as scheduling, planning, circuit verification, vehicle routing, configuration, networks, and bioinformatics. Constraint programming usually deals with problems defined on a finite domain known as constraint satisfaction problems (CSPs). These are all those problems specified by a set of variables and constraints that put restrictions on possible value assignments.

One way of finding the allowed value assignments to a CSP instance is to simply use a constraint solver. However, one could also transform the instance into a Boolean formula and use a Boolean satisfiability (SAT) solver. Even though such encodings frequently produce huge formulas, it is still sometimes beneficial to use SAT solvers due to their remarkable efficiency. However, little is known about why SAT solvers are so successful at finding solutions to various CSP instances. In this talk I will shed some light onto that question by connecting a central concept in CSP and a particular resolution rule. I will also show the influence of the different types of encodings on SAT solver performance.