SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints (Extended Abstract)
Miquel Bofill, Jordi Coll, Peter Nightingale, Josep Suy, Felix Ulrich-Oltean, Mateu Villaret
Abstract
When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the constraints is of vital importance. Pseudo-Boolean (PB) constraints appear frequently in a wide variety of problems. When PB constraints occur together with at-most-one (AMO) constraints over the same variables, they can be combined into PB(AMO) constraints. In this paper we present new encodings for PB(AMO) constraints. Our experiments show that these encodings can be substantially smaller than those of PB constraints and allow many more instances to be solved within a time limit. We also observed that there is no single overall winner among the considered encodings, but efficiency of each encoding may depend on PB(AMO) characteristics such as the magnitude of coefficient values.
BibTeX
@inproceedings{ijcai2023p769,
title = {SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints (Extended Abstract)},
author = {Bofill, Miquel and Coll, Jordi and Nightingale, Peter and Suy, Josep and Ulrich-Oltean, Felix and Villaret, Mateu},
booktitle = {Proceedings of the Thirty-Second International Joint Conference on
Artificial Intelligence, {IJCAI-23}},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
editor = {Edith Elkind},
pages = {6853--6857},
year = {2023},
month = {8},
note = {Journal Track},
doi = {10.24963/ijcai.2023/769},
url = {https://doi.org/10.24963/ijcai.2023/769},
}