Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

By Carsten Sinz. 2005

577 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Learning Optimal Decision Trees with SAT (2018, methodology): “We used the sequential counters encoding [Sinz, 2005] to model a cardinality constraint as a Boolean formula.”
Optimal Decision Lists using SAT (2020, background): “Also note that any of the known cardinality encodings that can be used to represent the sum in (1) (Biere et al. 2009, Chapter 2) (also see (As ´ ın et al. 2009; Bailleux and Boufkhad 2003; Batcher 1968; Sinz 2005)).”
Computing Optimal Decision Sets with SAT (2020, background): “oolean formula, which can be clausiﬁed with the use of auxiliary variables [54]. Also note that any of the known cardinality encodings can be used to represent constraint (1) [9, Chapter 2] (also see [1, 5,7,53]). Finally, the size (in terms of the number of literals) of the proposed SAT encoding is”
Evading network anomaly detection systems: formal reasoning and practical techniques (2006, background): “These cardinality constraints can be efficiently represented in SAT [26].”
Translating Pseudo-Boolean Constraints into SAT (2006, methodology): “Using adder networks to implement a linear translation of PB-constraint to circuits has been done before in [33, 3, 31], but the construction presented here uses fewer adders.”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, background): “If the constraint represents a cardinality constraint, then some of the available encodings in the literature are one of the following encodings: the pairwise and bitwise encodings [104, 105] (but only for AtMost1 and AtLeast1), the ladder encoding [49], sequential counters [119], sorting networks [”
PySAT: A Python Toolkit for Prototyping with SAT Oracles (2018, background): “There are multiple ways to encode cardinality constraints into a set of clauses and most state-of-the-art cardinality encodings are supported by PySAT including pairwise and bitwise encodings [38], sequential counters [48], sorting networks [7], cardinality networks [3], ladder/regular [2, 16], tota”
Efficient SAT-Based Encodings of Conditional Cardinality Constraints (2018, methodology): “The sequential counter based encoding of a cardinality constraint proposed by Carsten Sinz in [15] is another well-known encoding that preserves the generalized arc consistency property.”
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints (2007, methodology): “The encodings presented in [33] require the use of additional variables and either O(n · k) or 7n − 3 log n − 6 additional clauses.”