论文标题
重复使用伪树 - 树状编码中的比较器网络
Reusing Comparator Networks in Pseudo-Boolean Encodings
论文作者
论文摘要
伪树（PB）约束是对布尔文字的线性不等式约束。用于解决PB问题的流行，高效的想法之一（一组PB构成）是将它们转换为SAT实例（编码），例如对网络进行分类，然后使用最先进的Sat-Solvers处理这些实例。在本文中，我们展示了这种技术的改进。通过使用贪婪集封面算法的变体，在对我们的编码中添加约束时，我们将重复使用已编码的PB内置的一部分，以减少所得SAT实例的大小（变量和条款的数量）。实验评估表明，所提出的方法增加了解决实例的数量。
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.
