Generalized Totalizer Encoding for Pseudo-Boolean Constraints
Generalized Totalizer Encoding for Pseudo-Boolean Constraints
复制标题
伪布尔约束的广义累加器编码
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Vasco M. Manquinho
中科院分区：
文献类型：
--
作者：
Saurabh Joshi;R. Martins;Vasco M. Manquinho
伪布尔约束，也称为0-1线性约束，用于模拟许多现实世界的问题。解决这些约束的常见方法是将它们编码为SAT公式。SAT求解器在这样的公式上的运行时间对给定的伪布尔约束的编码方式敏感。在本文中，我们提出了广义累加器编码（GTE），这是一个弧一致性保持扩展的累加器编码伪布尔约束。与其他一些编码不同，GTE所需的辅助变量的数量不依赖于系数的大小。相反，它取决于这些系数的不同组合的数量。我们展示了GTE相对于其他编码的优越性时，大的伪布尔约束有低数量的不同的系数。我们的实验结果还表明，GTE仍然具有竞争力，即使伪布尔约束不具有这一特点。
Pseudo-Boolean constraints, also known as 0-1 Integer Linear Constraints, are used to model many real-world problems. A common approach to solve these constraints is to encode them into a SAT formula. The runtime of the SAT solver on such formula is sensitive to the manner in which the given pseudo-Boolean constraints are encoded. In this paper, we propose generalized Totalizer encoding (GTE), which is an arc-consistency preserving extension of the Totalizer encoding to pseudo-Boolean constraints. Unlike some other encodings, the number of auxiliary variables required for GTE does not depend on the magnitudes of the coefficients. Instead, it depends on the number of distinct combinations of these coefficients. We show the superiority of GTE with respect to other encodings when large pseudo-Boolean constraints have low number of distinct coefficients. Our experimental results also show that GTE remains competitive even when the pseudo-Boolean constraints do not have this characteristic.