Automatically Exploiting Symmetries in Constraint Programming

We introduce a framework for studying and solving a class of CSP formulations. The framework allows constraints to be expressed as linear and nonlinear equations, then compiles them into SAT instances via Boolean logic circuits. While in general reduction to SAT may lead to the loss of structure, we specifically detect several types of structure in high-level input and use them in compilation. Linearity is preserved by the use of pseudo-Boolean (PB) constraints in conjunction with a 0-1 ILP solver that extends common SAT-solving techniques. Symmetries are detected in high-level constraints by solving the graph automorphism problem on parse trees. Symmetry-breaking predicates are added during compilation. Our system generalizes earlier work [10; 2; 29] on symmetries in SAT and 0-1 ILP problems. Empirical evaluation is performed n instances of the social golfers and Hamming code generation problems. We show substantial speedups with symmetry-breaking, especially on unsatisfiable instances. In general, our runtimes with the specialized 0-1 ILP solver Pueblo [26] are competitive with results reported for ILOG Solver [28] in [15].