2

我的 Java 程序从其数据生成一个大型 CNF 实例。该实例主要包含（在大多数情况下>95%）排他的 2 子句：(!av !b)。目前我使用 Sat4j 的默认求解器。当我启用程序中的所有条件时，求解器将无限期运行。我尝试过一些经验来优化启发式和配置，但没有成功。解决此类情况的适当启发式集是什么？

（一个例子。）

4

0 回答 0