SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One
  Constraints
  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.
