2013 | OriginalPaper | Chapter
A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints
Authors : Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Published in: Principles and Practice of Constraint Programming
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Adequate encodings for high-level constraints are a key ingredient for the application of SAT technology. In particular,
cardinality constraints
state that at most (at least, or exactly)
k
out of
n
propositional variables can be true. They are crucial in many applications. Although sophisticated encodings for cardinality constraints exist, it is well known that for small
n
and
k
straightforward encodings without auxiliary variables sometimes behave better, and that the choice of the right trade-off between minimizing either the number of variables or the number of clauses is highly application-dependent. Here we build upon previous work on Cardinality Networks to get the best of several worlds: we develop an arc-consistent encoding that, by recursively decomposing the constraint into smaller ones, allows one to decide which encoding to apply to each sub-constraint. This process minimizes a function
λ
·
num
_
vars
+
num
_
clauses
, where
λ
is a parameter that can be tuned by the user. Our careful experimental evaluation shows that (e.g., for
λ
= 5) this new technique produces much smaller encodings in variables
and
clauses, and indeed strongly improves SAT solvers’ performance.