Yu、Subramanyan、Tsiskaridze和Malik的论文("all SAT using Minimal Blocking Clause")描述了一种更有效的寻找所有SAT解的方法。
我找到了一种方法,可以使用此链接中描述的方法找到所有解决方案。
这很好用,但速度很慢。由于i_e从一开始就重新计算约束,因此它没有利用以前的计算。
现在,我在这个链接中看到,有一种更有效的方法可以找到使用MiniSat作为库的所有解决方案。但那里没有描述这种方式。
你能给我指一下正确的文档来有效地找到所有SAT解决方案吗?
谢谢。
迭代寻找解决方案和添加阻塞子句的基本策略是相同的,但阻塞子句是使用一种新颖的想法生成的,这减少了它们的大小。生成的阻塞子句比通常的天真部分赋值更小,因此每次迭代都包含更令人满意的赋值,从而加快了枚举过程。
据我所知,本文中包含的思想还没有公开实现,您可以下载并运行。