A System for Embedding Global Constraints into SAT

ABSTRACT. Despite of being a dominant tool for solving some practical NP-complete problems, Propositional Satisfiability (SAT) also has a number of weaknesses, including its inability to compactly represent numerical constraints and its low level, unstructured language of clauses. In contrast, Constraint Programming (CP) has been widely used for scheduling and solving combinatorial search problems. In this report, We present a tight integration of SAT with CP, called SAT(gc),which embeds global constraints into SAT. A prototype is implemented by integrating the state of the art SAT solver zchaff and the generic constraint solver gecode. Experiments are carried out for benchmarks from puzzle domains and planning domains to reveal insights in compact representation, solving effectiveness, and novel usability of the new framework.