Skip to Main content Skip to Navigation
Conference papers

Detecting Cardinality Constraints in CNF

Abstract : We present novel approaches to detect cardinality constraints\r≠xpressed in CNF. The first approach is based on a syntactic analysis\r\nof specific data structures used in SAT solvers to represent binary and\r\nternary clauses, whereas the second approach is based on a semantic\r\nanalysis by unit propagation. The syntactic approach computes an approximation\r\nof the cardinality constraints AtMost-1 and AtMost-2 constraints\r\nvery fast, whereas the semantic approach has the property to be\r\ngeneric, i.e. it can detect cardinality constraints AtMost-k for any k, at\r\na higher computation cost. Our experimental results suggest that both\r\napproaches are efficient at recovering AtMost-1 and AtMost-2 cardinality\r\nconstraints.
Document type :
Conference papers
Complete list of metadata
Contributor : Emmanuel Lonca <>
Submitted on : Tuesday, November 26, 2019 - 1:43:10 PM
Last modification on : Wednesday, June 2, 2021 - 1:12:46 PM


  • HAL Id : hal-02380768, version 1



Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey. Detecting Cardinality Constraints in CNF. 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), 2014, Vienna, Austria. pp.285-301. ⟨hal-02380768⟩



Record views