A Pseudo-Boolean (PB) constraint is a linear inequality constraint over Boolean literals. One of the popular, efficient ideas used to solve PB-problems (a set of PB-constraints) is to translate them to SAT instances (encodings) via, for example, sorting networks, then to process those instances using state-of-the-art SAT-solvers. In this paper we show an improvement of such technique. By using a variation of a greedy set cover algorithm, when adding constraints to our encoding, we reuse parts of the already encoded PB-instance in order to decrease the size (the number of variables and clauses) of the resulting SAT instance. The experimental evaluation shows that the proposed method increases the number of solved instances.

翻译：伪布尔（PB）约束是布尔文字上的线性不等式约束。解决伪布尔问题（一组PB约束）的一种流行且高效的方法是将其通过排序网络等方式转化为SAT实例（编码），然后使用先进的SAT求解器处理这些实例。本文展示了对此技术的改进。通过在添加约束时采用贪心集合覆盖算法的变体，我们重用已编码PB实例的部分内容，从而降低所得SAT实例的规模（变量和子句数量）。实验评估表明，所提方法增加了可求解实例的数量。