Solving over-constrained problems with SAT

Abstract

We have defined a new formalism, based on Max-SAT, for encoding and solving over-constrained problems. Our formalism is an extension of Boolean CNF formulas in which we deal with blocks of Boolean clauses instead of dealing with individual clauses. Every block, formed by a set of clauses, is declared either as a hard block (i.e., must be satisfied by any solution) or as a soft block (i.e., can be violated by some solution). The idea behind the notion of block is that it encodes a problem constraint (for example, adjacent vertices have different colors); in general, it is not enough a single clause to encode a problem constraint. We call soft CNF formulas to this new kind of formulas. We have implemented two branch and bound solvers, Soft-SAT-S and Soft-SAT-D, for our problem solving approach. Given a soft CNF formula φ, our solvers search a truth assignment that satisfies all the hard blocks of φ and the maximum number of soft blocks. Both solvers are equipped with lazy data structures and a good performing lower bound. The variable selection heuristic in Soft-SAT-S is static while in Soft-SAT-D is dynamic. We conducted an experimental investigation for comparing our approach with weighted Max-SAT and Max-CSP. In the instances tested, we observed that Soft-SAT solvers are substantially superior to weighted Max-SAT solvers. On the one hand, our lower bound is of better quality because it takes into account the domain of the variables as in Max-CSP. On the other hand, the distinction between hard and soft blocks allows us to apply more powerful inference techniques; for example, unit clauses in hard blocks can be propagated. With respect to Max-CSP, we observed that Soft-SAT is very competitive as can be seen in the table below; it shows time in seconds. We compared Soft-SAT-S, Soft-SAT-D and the weighted CSP solvers PFC-MPRDAC1 and Toolbar2 on sets of 100 graph coloring instances generated with Culberson's generator. Experiments were performed on a 1.6 Ghz AMD64-Opteron with 1 Gbyte RAM. © Springer-Verlag Berlin Heidelberg 2005.