Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints

Carlos Ansótegui, Miquel Bofill, Jordi Coll*, Nguyen Dang, Juan Luis Esteban, Ian Miguel, Peter Nightingale, András Z. Salamon, Josep Suy, Mateu Villaret

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming - 25th International Conference, CP 2019, Proceedings
EditorsThomas Schiex, Simon de Givry
PublisherSpringer
Pages20-36
Number of pages17
ISBN (Print)9783030300470
DOIs
Publication statusPublished - 2019
Event25th International Conference on Principles and Practice of Constraint Programming, CP 2019 - Stamford , United States
Duration: 30 Sept 20194 Oct 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11802 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Principles and Practice of Constraint Programming, CP 2019
Country/TerritoryUnited States
CityStamford
Period30/09/194/10/19

Keywords

  • At-most-one constraint
  • Automatic CSP reformulation
  • Pseudo-Boolean
  • SAT

Fingerprint

Dive into the research topics of 'Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints'. Together they form a unique fingerprint.

Cite this