 |
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.
https://hal-univ-artois.archives-ouvertes.fr/hal-02380768
Contributor : Emmanuel Lonca Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2019 - 1:43:10 PM
Last modification on : Wednesday, October 20, 2021 - 9:58:20 AM
Contributor : Emmanuel Lonca Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2019 - 1:43:10 PM
Last modification on : Wednesday, October 20, 2021 - 9:58:20 AM