伪布尔约束与至多一约束的SAT编码
人工智能
2021-10-18 v1
摘要
在使用命题可满足性（SAT）求解组合问题时，问题的编码至关重要。我们研究了伪布尔（PB）约束的编码，这是一种常见的算术约束，广泛出现在诸如时间表编排、调度和资源分配等各种组合问题中。在某些情况下，PB约束与其变量子集上的至多一（AMO）约束同时出现（形成PB(AMO)约束）。近期研究表明，在使用决策图对PB约束进行编码时考虑AMO，可以显著提高求解器效率。在本文中，我们将该方法扩展到其他最先进的PB约束编码，为PB(AMO)约束开发了几种新的编码。此外，我们提出了流行的广义累加器编码的一个更紧凑、更高效的版本，命名为约化广义累加器。这种新编码也针对PB(AMO)约束进行了适配，以获得进一步的增益。我们的实验表明，PB(AMO)约束的编码可以比PB约束的编码小得多。PB(AMO)编码使得在时间限制内能够求解的实例数量大大增加，并且在某些情况下求解时间提高了一个数量级以上。我们还观察到，在所考虑的编码中，没有单一的整体赢家，每种编码的效率可能取决于PB(AMO)的特性，例如系数值的大小。
引用
@article{arxiv.2110.08068,
title = {SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints},
author = {Miquel Bofill and Jordi Coll and Peter Nightingale and Josep Suy and Felix Ulrich-Oltean and Mateu Villaret},
journal= {arXiv preprint arXiv:2110.08068},
year = {2021}
}