A Pigeon-Hole Based Encoding of Cardinality Constraints.
Saïd Jabbour, Lakhdar Saïs, Yakoub Salhi · ISAIM · 2013
In this paper, we propose a new encoding of the cardinality constraint ∑n i=1 xi > b. It makes an original use of the general formulation of the Pigeon-Hole principle to derive a formula in conjunctive normal form (CNF). Our PigeonHole based CNF encoding can be seen as a simple way to express the semantic of the cardinality constraint, that can be defined as how to put b pigeons into n holes. To derive an efficient CNF encoding that ensures constraint propagation, we exploit the set of symmetries of the Pigeon-Hole based formulation to derive an efficient CNF encoding of the cardinality constraint. More interestingly, the final CNF formula contains is b×(n−b) variables and clauses and belongs to the well-known Reverse-Horn tractable CNF formula, which can be decided by unit propagation. Our proposed Pigeon-Hole based encoding is theoretically compared with the currently well-known CNF encoding of the cardinality constraint.