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

Question

我找到了一种使用link 中描述的方法找到所有解决方案的方法。

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

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

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

谢谢。

Answer 1

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

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

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