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

doi:10.1007/978-3-030-30048-7_2

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 proceeding › Conference contribution

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 language	English
Title of host publication	Principles and practice of constraint programming
Subtitle of host publication	25th international conference, CP 2019, Stamford, CT, USA, September 30 - October, 4, 2019, proceedings
Editors	Thomas Schiex, Simon de Givry
Place of Publication	Cham
Publisher	Springer
Pages	20-36
Number of pages	17
ISBN (Electronic)	9783030300487
ISBN (Print)	9783030300470
DOIs	https://doi.org/10.1007/978-3-030-30048-7_2
Publication status	Published - 30 Aug 2019
Event	25th International Conference on Principles and Practice of Constraint Programming, CP 2019 - Stamford , United States Duration: 30 Sept 2019 → 4 Oct 2019

Publication series

Name	Lecture notes in computer science
Volume	11802
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	25th International Conference on Principles and Practice of Constraint Programming, CP 2019
Country/Territory	United States
City	Stamford
Period	30/09/19 → 4/10/19

Keywords

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

Access to Document

10.1007/978-3-030-30048-7_2

Cite this

Ansótegui, C., Bofill, M., Coll, J., Dang, N., Esteban, J. L., Miguel, I., Nightingale, P., Salamon, A. Z., Suy, J., & Villaret, M. (2019). Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints. In T. Schiex, & S. de Givry (Eds.), Principles and practice of constraint programming: 25th international conference, CP 2019, Stamford, CT, USA, September 30 - October, 4, 2019, proceedings (pp. 20-36). (Lecture notes in computer science; Vol. 11802). Springer. https://doi.org/10.1007/978-3-030-30048-7_2

Ansótegui, Carlos ; Bofill, Miquel ; Coll, Jordi et al. / Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints. Principles and practice of constraint programming: 25th international conference, CP 2019, Stamford, CT, USA, September 30 - October, 4, 2019, proceedings. editor / Thomas Schiex ; Simon de Givry. Cham : Springer, 2019. pp. 20-36 (Lecture notes in computer science).

@inproceedings{355e4cce34d641dcab1e4936a096bf39,

title = "Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints",

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.",

keywords = "At-most-one constraint, Automatic CSP reformulation, Pseudo-Boolean, SAT",

author = "Carlos Ans{\'o}tegui and Miquel Bofill and Jordi Coll and Nguyen Dang and Esteban, {Juan Luis} and Ian Miguel and Peter Nightingale and Salamon, {Andr{\'a}s Z.} and Josep Suy and Mateu Villaret",

note = "Funding: Work supported by grants TIN2015-66293-R, TIN2016-76573-C2-1/2-P (MINECO/ FEDER, UE), Ayudas para Contratos Predoctorales 2016 (grant number BES2016-076867, funded by MINECO and co-funded by FSE), RTI2018-095609-B-I00 (MICINN/ FEDER, UE), and EPSRC EP/P015638/1.; 25th International Conference on Principles and Practice of Constraint Programming, CP 2019 ; Conference date: 30-09-2019 Through 04-10-2019",

year = "2019",

month = aug,

day = "30",

doi = "10.1007/978-3-030-30048-7_2",

language = "English",

isbn = "9783030300470",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "20--36",

editor = "Thomas Schiex and {de Givry}, Simon",

booktitle = "Principles and practice of constraint programming",

address = "Netherlands",

}

Ansótegui, C, Bofill, M, Coll, J, Dang, N, Esteban, JL, Miguel, I, Nightingale, P, Salamon, AZ, Suy, J & Villaret, M 2019, Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints. in T Schiex & S de Givry (eds), Principles and practice of constraint programming: 25th international conference, CP 2019, Stamford, CT, USA, September 30 - October, 4, 2019, proceedings. Lecture notes in computer science, vol. 11802, Springer, Cham, pp. 20-36, 25th International Conference on Principles and Practice of Constraint Programming, CP 2019, Stamford , United States, 30/09/19. https://doi.org/10.1007/978-3-030-30048-7_2

Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints. / Ansótegui, Carlos; Bofill, Miquel; Coll, Jordi et al.
Principles and practice of constraint programming: 25th international conference, CP 2019, Stamford, CT, USA, September 30 - October, 4, 2019, proceedings. ed. / Thomas Schiex; Simon de Givry. Cham: Springer, 2019. p. 20-36 (Lecture notes in computer science; Vol. 11802).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints

AU - Ansótegui, Carlos

AU - Bofill, Miquel

AU - Coll, Jordi

AU - Dang, Nguyen

AU - Esteban, Juan Luis

AU - Miguel, Ian

AU - Nightingale, Peter

AU - Salamon, András Z.

AU - Suy, Josep

AU - Villaret, Mateu

N1 - Funding: Work supported by grants TIN2015-66293-R, TIN2016-76573-C2-1/2-P (MINECO/ FEDER, UE), Ayudas para Contratos Predoctorales 2016 (grant number BES2016-076867, funded by MINECO and co-funded by FSE), RTI2018-095609-B-I00 (MICINN/ FEDER, UE), and EPSRC EP/P015638/1.

PY - 2019/8/30

Y1 - 2019/8/30

N2 - 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.

AB - 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.

KW - At-most-one constraint

KW - Automatic CSP reformulation

KW - Pseudo-Boolean

KW - SAT

UR - https://doi.org/10.1007/978-3-030-30048-7

U2 - 10.1007/978-3-030-30048-7_2

DO - 10.1007/978-3-030-30048-7_2

M3 - Conference contribution

AN - SCOPUS:85075736319

SN - 9783030300470

T3 - Lecture notes in computer science

SP - 20

EP - 36

BT - Principles and practice of constraint programming

A2 - Schiex, Thomas

A2 - de Givry, Simon

PB - Springer

CY - Cham

T2 - 25th International Conference on Principles and Practice of Constraint Programming, CP 2019

Y2 - 30 September 2019 through 4 October 2019

ER -

Ansótegui C, Bofill M, Coll J, Dang N, Esteban JL, Miguel I et al. Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints. In Schiex T, de Givry S, editors, Principles and practice of constraint programming: 25th international conference, CP 2019, Stamford, CT, USA, September 30 - October, 4, 2019, proceedings. Cham: Springer. 2019. p. 20-36. (Lecture notes in computer science). doi: 10.1007/978-3-030-30048-7_2

Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-Boolean constraints

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this