By the same authors

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

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

Standard

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; Dang, Nguyen; Esteban, Juan Luis; Miguel, Ian James; Nightingale, Peter; Salamon, András Z.; Suy, Josep; Villaret, Mateu.

Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming. Springer, 2019. p. 20-36.

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

Harvard

Ansótegui, C, Bofill, M, Coll, J, Dang, N, Esteban, JL, Miguel, IJ, 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 Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming. Springer, pp. 20-36.

APA

Ansótegui, C., Bofill, M., Coll, J., Dang, N., Esteban, J. L., Miguel, I. J., 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 Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming (pp. 20-36). Springer.

Vancouver

Ansótegui C, Bofill M, Coll J, Dang N, Esteban JL, Miguel IJ et al. Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints. In Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming. Springer. 2019. p. 20-36

Author

Ansótegui, Carlos ; Bofill, Miquel ; Coll, Jordi ; Dang, Nguyen ; Esteban, Juan Luis ; Miguel, Ian James ; Nightingale, Peter ; Salamon, András Z. ; Suy, Josep ; Villaret, Mateu. / Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints. Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming. Springer, 2019. pp. 20-36

Bibtex - Download

@inproceedings{c5e5f93df9144887a249b7f4cb6cc903,
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. ",
author = "Carlos Ans{\'o}tegui and Miquel Bofill and Jordi Coll and Nguyen Dang and Esteban, {Juan Luis} and Miguel, {Ian James} and Peter Nightingale and Salamon, {Andr{\'a}s Z.} and Josep Suy and Mateu Villaret",
year = "2019",
month = sep,
day = "30",
language = "English",
pages = "20--36",
booktitle = "Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming",
publisher = "Springer",

}

RIS (suitable for import to EndNote) - Download

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 James

AU - Nightingale, Peter

AU - Salamon, András Z.

AU - Suy, Josep

AU - Villaret, Mateu

PY - 2019/9/30

Y1 - 2019/9/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.

M3 - Conference contribution

SP - 20

EP - 36

BT - Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming

PB - Springer

ER -