具有小子句密度的公式的图形化#SAT算法
摘要：用ZH演算法研究布尔可满足性问题#SAT的计数版本。利用这一方法，我们找到了#SAT的自然扩展，称为#SAT_pm，其中变量还附带相位标签，并且这个问题是GapP完备的。利用图形推理，在ZH演算法中找到了从#SAT到#2SAT_pm的规约。我们观察到，对于#2SAT的DPLL算法可以直接适应#2SAT_pm，并且这意味着Wahlstrom的O^*(1.2377^n)的上界也适用于#2SAT_pm。结合我们从#SAT到#2SAT_pm的规约，我们得到了更好的子句和变量的上下界，对于小子句密度(m/n < 2.25)，这些上下界比O^*(2^n)要好。据我们所知，这是独立于子句大小的第一个具有非平凡上界的#SAT算法。我们的算法在m/n < 1.85且k >= 4时改进了Dubois对于#kSAT的上界，并且在m/n < 1.21且k >= 6时改进了Williams的平均情况分析。我们还得到了关于子句的无条件上界O^*(1.88^m)对于#4SAT，并且对于1.2577 < m/n <= 7/3时对#3SAT得到了改进的上界。我们的结果表明，图形推理可以引发算法上的新思路，即使在ZH演算法原本设计用于量子计算的领域之外。
作者：Tuomas Laakkonen and Konstantinos Meichanetzidis and John van de Wetering
论文ID：2212.08048
分类：Computational Complexity
分类简称：cs.CC
提交时间：2022-12-16