SAT Encodings for Pseudo-Boolean Constraints Together with At-Most-One Constraints (Extended Abstract)
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.
Cite
Text
Bofill et al. "SAT Encodings for Pseudo-Boolean Constraints Together with At-Most-One Constraints (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2023. doi:10.24963/IJCAI.2023/769Markdown
[Bofill et al. "SAT Encodings for Pseudo-Boolean Constraints Together with At-Most-One Constraints (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2023.](https://mlanthology.org/ijcai/2023/bofill2023ijcai-sat/) doi:10.24963/IJCAI.2023/769BibTeX
@inproceedings{bofill2023ijcai-sat,
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 = {International Joint Conference on Artificial Intelligence},
year = {2023},
pages = {6853-6857},
doi = {10.24963/IJCAI.2023/769},
url = {https://mlanthology.org/ijcai/2023/bofill2023ijcai-sat/}
}