Efficient CNF Encoding of Boolean Cardinality Constraints

By O. Bailleux, Yacine Boufkhad. 2003

355 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Computer Vision and Pattern Recognition

How researchers see this paper

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

In Computational Theory and Mathematics

In Computer Vision and Pattern Recognition

Citations in the corpus

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): “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]).”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, background): “encoding for the AtMostK constraints corresponds to [20].”
Towards an Optimal CNF Encoding of Boolean Cardinality Constraints (2005, methodology): “Parallel binary counter (LT PAR) 7n− 3blog nc − 6 2n− 2 by search Bailleux & Boufkhad [4] O(n(2)) O(n · log n) by unit prop.”
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, neutral): “[17, 3, 15, 13, 1, 11]) and pseudo-boolean constraints (e.”
Translating Pseudo-Boolean Constraints into SAT (2006, background): “Some important special cases have been studied in [17, 4, 5, 6].”