增量 SAT 求解：保存求解实例 - 在运行之间更改模型答案

【问题标题】：Incremental SAT Solving: save solving instance - change model between runs增量 SAT 求解：保存求解实例 - 在运行之间更改模型
【发布时间】：2016-05-24 07:27:26
【问题描述】：

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

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

我对 SAT 求解很陌生，所以我可能会忽略一些东西。有没有办法保存解决实例供以后使用？关闭实例会丢失所有学习内容吗？

【问题讨论】：

标签： sat sat4j

【解决方案1】：

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

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

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

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

【讨论】：

对不起，我觉得我没有明确表达我的意图。我想知道的是，学习的子句是否永久存储在某种形式的数据库中。从我所看到的情况来看，它们不是（而且没有办法“手动”保存它们）。因此，一旦我终止求解器，它们就会丢失。这意味着我无法评估模型，然后在 2 周后对其进行更改，并尝试通过使用第一次运行时学到的子句来缩短重新评估时间。
默认情况下，学习的约束保存在一组“可擦除”的约束中，特定于学习子句。由于该组子句在搜索过程中快速增长，SAT 求解器会定期删除该组中不太活跃的子句。

【解决方案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(Node node)），但很可能还有更多性能更高的解决方案。

另一种带有假设的解决方案在我们的案例中不起作用，因为我们有数百万个对具有多达 20,000 个变量的单个 SAT 求解器实例的查询。假设会使变量的数量从 2 万到 100 万不等，这不太可能有帮助。

【讨论】：