Incremental SAT Solving: save solving instance - change model between runs

Question

From my understanding incremental SAT solving helps to evaluate different models who are quite close to each other.

I want to use this to evaluate a model and if I change it later reevaluate it again using the previous solution for a faster result. However after looking into various SAT Solvers (Sat4J, Minisat, mathsat5) it seems like they are only able to solve incrementally when all models are presented within one run.

I'm quite new to SAT solving so I might be overlooking something. Is there no way to save a solving instance for later use? Is all learning lost on closing the instance?

Answer 1

In incremental mode, you can feed the solver with new constraints.

Depending on the settings, the solver may or may not forget previous learned clauses and heuristics.

To fully take advantage of the incremental mode and discard previously entered constraints in the system, you need to use "assumptions", i.e. specific variables which will activate or disable the constraints in the solver.

See e.g. this discussion in minisat newsgroup: https://groups.google.com/forum/#!topic/minisat/ffXxBpqKh90

Answer 2

SAT4J provides a mechanism, which allows you feed the solver and then remove parts of the clauses and add new ones clauses for the next check for satisfiability. Clauses to be removed need to be added to a ConstGroup. Unfortunately, it is slighly more complicated, as unit clauses need special handling. It works roughly like this:

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);
    }

Unfortunately, the removal of clauses is implemented in a rather naive way and requires quadratic effort in the number of clauses to be removed.

While this solution works in FeatureIDE (see isSatisfiable(Node node) in https://github.com/FeatureIDE/FeatureIDE/blob/develop/plugins/de.ovgu.featureide.fm.core/src/org/prop4j/SatSolver.java), it is likely that there are way more performant solutions out there.

The other solution with assumptions does not work in our case, as we have millions of queries to a single SAT solver instance with up-to 20,000 variables. Assumptions would increate the number of variables from 20 thousand to a million, which is unlikely to help.