Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-boolean constraints
Visualitza/Obre
10.1007/978-3-030-30048-7_2
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/170483
Tipus de documentText en actes de congrés
Data publicació2019
EditorSpringer
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Projecte
Abstract
Pseudo-Boolean (PB) constraints often have a critical role in constraint satisfaction and optimisation problems. Encoding PB constraints to SAT has proven to be an efficient approach in many applications, however care must be taken to encode them compactly and with good propagation properties. It has been shown that at-most-one (AMO) and exactly-one (EO) relations over subsets of the variables can be exploited in various encodings of PB constraints, improving their compactness and solving performance. In this paper we detect AMO and EO relations completely automatically and exploit them to improve SAT encodings that are based on Multi-Valued Decision Diagrams (MDDs). Our experiments show substantial reductions in encoding size and dramatic improvements in solving time thanks to automatic AMO and EO detection.
CitacióAnsótegui, C. [et al.]. Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-boolean constraints. A: International Conference on Principles and Practice of Constraint Programming. "Principles and Practice of Constraint Programming 25th International Conference, CP 2019: Stamford, CT, USA, September 30-October 4, 2019: proceedings". Berlín: Springer, 2019, p. 20-36.
ISBN978-3-030-30048-7
Versió de l'editorhttps://link.springer.com/chapter/10.1007/978-3-030-30048-7_2
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
CP2019.pdf | 324,2Kb | Visualitza/Obre |