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

TL;DR

This paper develops new and improved SAT encodings for Pseudo-Boolean constraints with At-Most-One conditions, significantly enhancing solver efficiency and enabling more instances to be solved faster.

Contribution

It introduces several novel encodings for PB(AMO) constraints, including a compact version of the Generalized Totalizer, improving efficiency over existing methods.

Findings

PB(AMO) encodings are smaller than PB encodings

PB(AMO) encodings solve more instances within time limits

Solving time varies with PB(AMO) characteristics

Abstract

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.