SAT Encodings of Pseudo-Boolean Constraints with At-Most-One Relations.

Pseudo-Boolean (PB) constraints appear often in a large variety of constraint satisfaction problems. Encoding such constraints to SAT has proved to be an efficient approach in many applications. However, most of the existing encodings in the literature do not take profit from side constraints that often occur together with the PB constraints. In this work we introduce specialized encodings for PB constraints occurring together with at-most-one (AMO) constraints over subsets of their variables. We show that many state-of-the-art SAT encodings of PB constraints from the literature can be dramatically reduced in size thanks to the presence of AMO constraints. Moreover, the new encodings preserve the propagation properties of the original ones. Our experiments show a significant reduction in solving time thanks to the new encodings.