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.
Complete list of metadatas

https://hal-univ-artois.archives-ouvertes.fr/hal-02380768
Contributor : Emmanuel Lonca <>
Submitted on : Tuesday, November 26, 2019 - 1:43:10 PM
Last modification on : Wednesday, November 27, 2019 - 1:40:22 AM

Identifiers

  • HAL Id : hal-02380768, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

23