# SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints

arXiv: https://arxiv.org/abs/2110.08068 · HTML: https://mlsanity.com/paper/2110.08068/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 40 references that are in the map.
- First posted on arXiv 15 Oct 2021.

## Builds on (most cited first, 3 of 3)

- [A New Look at BDDs for Pseudo-Boolean Constraints](https://mlsanity.com/paper/1401.5860/) (2014)
- [Generalized Totalizer Encoding for Pseudo-Boolean Constraints](https://mlsanity.com/paper/1507.05920/) (2015)
- [Essence' Description](https://mlsanity.com/paper/1601.02865/) (2016)

## Built on by (most cited first, 3 of 3)

- [Savile Row Manual](https://mlsanity.com/paper/2201.03472/) (2021)
- [Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints](https://mlsanity.com/paper/2307.09342/) (2023)
- [PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas](https://mlsanity.com/paper/2312.15877/) (2023)

## Abstract (arXiv)

When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the problem is of vital importance. We study encodings of Pseudo-Boolean (PB) constraints, a common type of arithmetic constraint that appears in a wide variety of combinatorial problems such as timetabling, scheduling, and resource allocation. In some cases PB constraints occur together with at-most-one (AMO) constraints over subsets of their variables (forming PB(AMO) constraints). Recent work has shown that taking account of AMOs when encoding PB constraints using decision diagrams can produce a dramatic improvement in solver efficiency. In this paper we extend the approach to other state-of-the-art encodings of PB constraints, developing several new encodings for PB(AMO) constraints. Also, we present a more compact and efficient version of the popular Generalized Totalizer encoding, named Reduced Generalized Totalizer. This new encoding is also adapted for PB(AMO) constraints for a further gain. Our experiments show that the encodings of PB(AMO) constraints can be substantially smaller than those of PB constraints. PB(AMO) encodings allow many more instances to be solved within a time limit, and solving time is improved by more than one order of magnitude in some cases. 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.