6533b82cfe1ef96bd128f309

RESEARCH PRODUCT

Efficient CNF Encoding of Boolean Cardinality Constraints

Yacine BoufkhadOlivier Bailleux

subject

Discrete mathematicsTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESCardinalityUnit propagationComputer scienceConstrained optimizationData_CODINGANDINFORMATIONTHEORYVariable eliminationComputer Science::Computational ComplexityConjunctive normal formBoolean data typeSatisfiability

description

In this paper, we address the encoding into CNF clauses of Boolean cardinality constraints that arise in many practical applications. The proposed encoding is efficient with respect to unit propagation, which is implemented in almost all complete CNF satisfiability solvers. We prove the practical efficiency of this encoding on some problems arising in discrete tomography that involve many cardinality constraints. This encoding is also used together with a trivial variable elimination in order to re-encode parity learning benchmarks so that a simple Davis and Putnam procedure can solve them.

yearjournalcountryeditionlanguage
2003-01-01
https://doi.org/10.1007/978-3-540-45193-8_8