Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-boolean constraints
| Autor: | Carlos Ansótegui, Juan Luis Esteban, Nguyen Dang, Josep Suy, Jordi Coll, Ian Miguel, András Z. Salamon, Mateu Villaret, Peter Nightingale, Miquel Bofill |
|---|---|
| Přispěvatelé: | Universitat Politècnica de Catalunya. Departament de Ciències de la Computació |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
050101 languages & linguistics
Theoretical computer science Exploit Computer science Atmost-one constraint Constraint programming (Computer science) 05 social sciences Automatic CSP reformulation 02 engineering and technology Constraint satisfaction ENCODE Computer algorithms Compact space Algebra Boolean Informàtica::Informàtica teòrica [Àrees temàtiques de la UPC] Programació per restriccions (Informàtica) Encoding (memory) 0202 electrical engineering electronic engineering information engineering Algorismes computacionals 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences SAT Pseudo-Boolean Àlgebra booleana |
| Zdroj: | UPCommons. Portal del coneixement obert de la UPC Universitat Politècnica de Catalunya (UPC) Recercat. Dipósit de la Recerca de Catalunya instname Lecture Notes in Computer Science ISBN: 9783030300470 CP |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|