optimization - minisat 如何有效地找到所有 SAT 解决方案

Question

我找到了一种使用此链接中描述的方式查找所有解决方案的方法。

这工作正常，但速度很慢。因为它从一开始就重新计算约束，所以 i_e 没有利用以前的计算。

现在，我在这个 链接中看到，有一种更有效的方法可以使用 MiniSat 作为库来查找所有解决方案。但是那里没有描述方法。

您能否为我指出正确的文档以有效地找到所有 SAT 解决方案？

谢谢。

Answer 1

Yu、Subramanyan、Tsiskaridze 和 Malik的论文（ “All-SAT using Minimal Blocking Clauses” ）中描述了一种更有效的查找所有 SAT 解决方案的方法。

迭代寻找解决方案和添加阻塞子句的基本策略是相同的，但是阻塞子句是使用一种新颖的思想生成的，从而减小了它们的大小。生成的阻塞子句比通常的幼稚部分赋值要小，因此每次迭代都包含更令人满意的赋值，从而加快了枚举过程。

据我所知，没有可以下载和运行的本文中包含的想法的公开实现。