0

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

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

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

4

2 回答 2

0

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

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

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

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

于 2016-05-25T08:09:37.590 回答
0

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

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

于 2017-05-11T11:56:33.033 回答