有效辅助变量通过结构化重新编码
摘要：溯及成文，通过引入辅助变量，在理论上可以扩展分辨率。然而，试图在实践中利用这一潜力的努力取得了有限的成功。在这方面，一个相当有效的方法是有界变量添加（BVA），它通过引入新变量并消除子句，通常显著减少公式的大小。我们发现一些有启发性的例子，表明BVA引起的性能改进不仅来自大小的减少，还来自有效的辅助变量的引入。分析特定的装箱着色实例，我们发现BVA在公式随机化方面是脆弱的，依赖于变量顺序来打破平局。基于这种理解，我们以一种结构化的方式为BVA增加了一个打破平局的启发式方法。我们评估我们的新预处理技术Structured BVA (SBVA)，在之前的SAT竞赛中的29,000多个公式上显示出对随机化的鲁棒性。在模拟的竞赛环境中，我们的实现在随机化和原始公式上都优于BVA，并且似乎非常适用于某些公式族。
作者：Andrew Haberlandt, Harrison Green, Marijn J.H. Heule
论文ID：2307.01904
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-06