关于“基于有界决策图的桶消除算法上界”的注释
摘要：基于有序二进制决策图（BDD）的布尔可满足性（SAT）求解器，特别是那些可以生成不可满足性证明的求解器。通过理论分析，我们证明了一个基于BDD的SAT求解器可以在多项式时间内为鸽洞问题（PHP$_n$）生成一个不可满足性证明，即使问题是以标准的“直接”形式编码的。我们的方法基于桶消除，使用与桶中变量不同的变量顺序来构建BDD。我们的实验证明，这些证明的规模为$O(n^5)$。我们也证实了当BDD和桶使用相同的变量顺序时会导致指数级增长的情况。
作者：Randal E. Bryant
论文ID：2306.10337
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-21