A cardinality solver: More expressive constraints for free (Poster presentation)

Abstract

Despite the semantic simplicity of cardinality constraints, the CNF encodings typically used to solve them invariably turn one constraint into a large number of CNF clauses and/or auxiliary variables. This incurs a significant cost, both in space complexity and in runtime, that could be avoided by reasoning about cardinality constraints directly within a solver. Adding a single, native cardinality constraint instead of numerous clauses and/or auxiliary variables avoids any space overhead and simplifies the solver's procedures for reasoning about that constraint. Inspired by the simple observation that clauses are cardinality constraints themselves, and thus cardinality constraints generalize clauses, this work seeks to answer the question: How much of the research on developing efficient CNF SAT solvers can be applied to solving cardinality constraints? © 2012 Springer-Verlag.