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

Question

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

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

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

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

谢谢。

Answer 1

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

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

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