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

Question

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

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

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

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

谢谢。

Answer 1

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

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

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