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 Connect in order to contact the contributor
Submitted on : Wednesday, June 15, 2022 - 10:57:16 PM
Last modification on : Tuesday, June 21, 2022 - 7:33:29 AM


Files produced by the author(s)




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, ⟨10.1007/978-3-319-09284-3_22⟩. ⟨hal-02380768⟩



Record views


Files downloads