Encoding Linear Constraints with Implication Chains to CNF
Ignasi Abio, Valentin Mayer-Eichberger, Peter J Stuckey, G Pesant (ed.)
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | SPRINGER-VERLAG BERLIN | Published : 2015
Linear constraints are the most common constraints occurring in combinatorial problems. For some problems which combine linear constraints with highly combinatorial constraints, the best solving method is translation to SAT. Translation of a single linear constraint to SAT is a well studied problem, particularly for cardinality and pseudo- Boolean constraints. In this paper we describe how we can improve encodings of linear constraints by taking into account implication chains in the problem. The resulting encodings are smaller and can propagate more strongly than separate encodings. We illustrate benchmarks where the encoding improves performance.