增量SAT求解:保存求解实例-运行之间的更改模型

Question

根据我的理解，增量SAT求解有助于评估彼此非常接近的不同模型。

我想用它来评估一个模型，如果我后来更改了它，就使用以前的解决方案再次重新评估它，以获得更快的结果。然而，在研究了各种SAT解算器(Sat4J，Minisat，mathsat5)之后，似乎只有当所有模型都在一次运行中呈现时，它们才能增量地求解。

我对SAT的解决还是个新手，所以我可能忽略了一些东西。有没有办法保存解算实例以供以后使用？关闭实例会丢失所有的学习吗？

Answer 1

在增量模式下，可以为求解器提供新的约束。

根据设置，求解器可能会忘记以前学到的子句和启发式，也可能不会忘记。

要充分利用增量模式并丢弃以前在系统中输入的约束，您需要使用“假设”，即将激活或禁用求解器中的约束的特定变量。

例如，请参阅minisat新闻组中的讨论：https://groups.google.com/forum/#!topic/minisat/ffXxBpqKh90

Answer 2

SAT4J提供了一种机制，允许您提供求解器，然后删除部分子句并添加新的子句，以便进行下一次可满足性检查。要删除的子句需要添加到ConstGroup中。不幸的是，它稍微复杂一些，因为单位子句需要特殊处理。它的工作原理大致如下：

solver = initialize it with clauses which are not to be removed
boolean satisfiable;
ConstrGroup group = new ConstrGroup();
IVecInt unit = new VecInt();
try {
    for (all clauses to be added and removed) {
        if (unit clause) {
            unit.push(variable from clause);
        } else {
            group.add(solver.addClause(clause));
        }
        satisfiable = solver.isSatisfiable(unit);
    } catch (ContradictionException e) {
        satisfiable = false;
    } finally {
        group.removeFrom(solver);
    }

不幸的是，删除子句是以一种相当幼稚的方式实现的，并且需要对要删除的子句的数量进行二次努力。

虽然此解决方案在FeatureIDE中有效(请参阅https://github.com/FeatureIDE/FeatureIDE/blob/develop/plugins/de.ovgu.featureide.fm.core/src/org/prop4j/SatSolver.java中的isSatisfiable(节点节点))，但很可能还有更高性能的解决方案。

另一种带有假设的解决方案在我们的情况下不起作用，因为我们有数百万个查询到单个SAT求解器实例，其中最多有20,000个变量。假设会将变量的数量从20000增加到100万，这不太可能有帮助。