是否有有时有效的算法可以解决#SAT？
https://cs.stackexchange.com/questions/8952
-
16-10-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian题
令$ b $为布尔公式，由通常的和或者，而不是操作员和某些变量组成。我想计算$ b $的满意作业数量。也就是说，我想找到真相值的不同作业的数量到$ b $假定真实值的$ b $的变量。例如，公式$ a lor b $具有三个令人满意的作业； $（a lor b） land（c lor lnot b）$有四个。这是 #sat问题.
显然，解决此问题的有效解决方案将意味着有效的SAT解决方案，这是不太可能的，实际上，这个问题是＃P-Complete，因此严格严格比SAT更难。因此，我不会期望有保证的解决方案。
但是众所周知，SAT本身的非常困难的实例相对较少。 （例如，见 Cheeseman 1991，“哪里 真的 严重问题是”。。解决方法虽然在最坏的情况下呈指数级，但在实践中的效率更高。
我的问题是：
是否知道任何算法都可以快速计算典型布尔公式的满足分配数量，即使这种算法在一般实例中需要指数时间？有什么比列举所有可能的作业更好的了吗？
解决方案
在一般情况下计数
您感兴趣的问题称为#SAT或模型计数。从某种意义上说，这是经典的＃P完整问题。模型计数很难，即使以$ 2 $ -SAT的价格！毫不奇怪，确切的方法只能处理大约数百个变量的实例。也存在近似方法，并且它们可能能够处理约1000个变量的实例。
精确的计数方法通常基于DPLL风格的详尽搜索或某种知识汇编。近似方法通常被归类为提供快速估计的方法，而无需提供任何保证和上限提供正确性保证的方法。还有其他可能不符合类别的方法，例如发现后门或坚持某些结构属性以保持公式（或其约束图）的方法。
那里有实际实现。一些确切的模型计数器是CDP，Relsat，Cachet，Sharpsat和C2D。精确求解器使用的主要技术是部分计数，组件分析（未经限制图），公式和组件缓存以及每个节点处的智能推理。基于知识汇编的另一种方法将输入CNF公式转换为另一种逻辑形式。从这种形式可以轻松推导模型计数（以新生产的公式的大小为多项式时间）。例如，一个人可能会将公式转换为二进制决策图（BDD）。然后，一个人可以将BDD从“ 1”叶子横穿到根部。或另一个示例，C2D采用了一个编译器，该编译器将CNF公式变成确定性分解的否定形式（D-DNNF）。
如果您的实例变大或您不在乎确切，那么也存在大致的方法。通过近似方法，我们关心并考虑与算法报告的估计值相关的估计质量以及正确的信心。 Wei和Selman [2]的一种方法使用MCMC采样来计算输入公式的真实模型计数的近似值。该方法是基于以下事实：如果一个人可以从公式$ phi $的解决方案集合（接近）中进行采样，那么可以计算出$ phi $的解决方案数量的良好估计。
Gogate和Dechter [3]使用一种称为SampleMinisat的模型计数技术。它基于布尔公式的无回溯搜索空间的采样。该技术建立在重要性重新采样的概念上，使用基于DPLL的SAT求解器来构建无回溯搜索空间。这可能是完全或近似完成的。还可以进行保证的估计抽样。基于[2]，Gomes等。 [4]表明，使用修改后的随机策略采样，可以通过高概率正确性保证在总模型计数上获得可证明的下限。
也有基于信仰传播（BP）的工作。参见Kroc等。 [5]和他们介绍的bpcount。在同一篇论文中，作者给出了第二种称为Minicount的方法，用于在模型计数上提供上限。还有一个统计框架，可以在某些统计假设下计算上限。
＃2-SAT和＃3-SAT的算法
如果您将注意力限制在＃2-SAT或＃3-SAT上，则有一些算法以$ O（1.3247^n）$和$ O（1.6894^n）$运行，分别用于这些问题[1]。这些算法有略有改进。例如，kutzkov [6]在＃3-sat的上限上进行了改进，并在时间$ o（1.6423^n）$中运行算法。
就像问题的性质一样，如果您想解决实践中的实例，很大程度上取决于实例的大小和结构。您知道的越多，选择正确的方法就越有能力。
[2] W. Wei和B. Selman。一种新的模型计数方法。在SAT05：第8届“可满足性测试理论与应用国际会议）中，计算机科学讲义的第3569卷，324-339，2005年。
[3] R. Gogate和R. DeChter。通过对无回溯搜索空间进行采样来近似计数。在AAAI-07：第22届全国人工智能会议上，198-203，温哥华，2007年。
[4] CP Gomes，J。Hoffmann，A。Sabharwal和B. Selman。从采样到模型计数。在IJCAI-07：第20届国际人工智能会议上，2293– 2299年，2007年。
其他提示
除了Juho列出的论文外，这里还有一些描述有关该主题的工作，尤其是在近似解决方案的数量上：
模型计数. 。 Carla P. Gomes，Ashish Sabharwal，Bart Selman满意度手册，iOS出版社。编辑：Armin Biere，Marijn Heule，Hans van Maaren和Toby Walsh。第20章，第633-654页，2009年。
- 这对主题和许多技术的介绍都有很好的概述。
使用XOR约束对组合空间的接近均匀采样。 Carla P. Gomes，Ashish Sabharwal，Bart Selman。 NIPS-06。第20届神经信息处理系统会议，第481-488页，加拿大卑诗省温哥华，2006年12月。
模型计数的简短：从理论到实践。 Carla P. Gomes，Joerg Hoffmann，Ashish Sabharwal，Bart Selman SAT-07。第10届国际理论和可满足性测试应用会议，LNCS第4501卷，第100-106页，里斯本，葡萄牙，2007年5月。
利用信念传播，回溯搜索和统计数据进行模型计数。 Lukas Kroc，Ashish Sabharwal，Bart Selman Anor-2011。 《运营纪事》，第184卷，第1卷，第209-231页，2011年。
快速精确模型计数的启发式方法。天·桑（Tian Sang），保罗·贝（Paul Beame）和亨利·考茨（Henry Kautz）。可满足性测试的理论和应用（SAT 2005），第226-240页。
