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.
翻译:当使用参数对称性(SAT)解决组合问题时,问题编码至关重要。我们研究了Pseudo-Boolean(PB)制约(PB)的编码,这是一种常见的算术制约,出现在诸如计时、时间安排和资源分配等广泛的组合问题中。在某些情况下,PB制约与最接近于一(AMO)的变量子集(制成PB(AMO)的制约)的制约(制成PB(AMO)的制约)同时出现。最近的工作表明,在使用决定图表对 PB 制约进行编码时,AMO的特性可以显著提高求解效率。在本文中,我们将这一方法推广到PB 制约的其他最先进的编码,为PB 制约制定新的编码。此外,我们提出的通用的通用调制解密(AMO) 限制的精度可能大大小于PB 级(AMO) 时间限制的编码,而我们所观察到的PMO 的精度则会比PMO 的精度要小得多。