Mixed radix weight totalizer encoding for pseudo-boolean constraints

Abstract

Many problems in various fields can be expressed as the problem of optimizing the value of a pseudo-Boolean constraint which is a linear constraint over Boolean variables. This paper proposes a new technique, called Mixed Radix Weight Totalizer Encoding (MRWTE), which encodes pseudo-Boolean constraints into clauses that can be handled by a standard SAT solver. This new technique will allow us to fully exploit the latest improvements in SAT research. Unlike other encodings, the number of auxiliary variables required for MRWTE does not depend on the magnitudes of the coefficients. Instead, it depends on the number of distinct combinations of the coefficients. Our experimental results show that MRWTE compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-The-Art SAT solver.