From 718fa5ae2f010740862aad2dfb28cedac63e4be3 Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Wed, 17 Apr 2024 14:57:12 +0200 Subject: [PATCH] minor fix in load state (only affected stats) --- .../logicng/solvers/sat/LNGCoreSolver.java | 124 ++++++------------ 1 file changed, 43 insertions(+), 81 deletions(-) diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java index 5878bf35..a5f4e225 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java @@ -611,7 +611,7 @@ public void loadState(final SolverState solverState) { permDiff.shrinkTo(newVarsSize); final int newClausesSize = Math.min(state[2], clauses.size()); for (int i = clauses.size() - 1; i >= newClausesSize; i--) { - simpleRemoveClause(clauses.get(i)); + detachClause(clauses.get(i)); } clauses.shrinkTo(newClausesSize); int newLearntsLength = 0; @@ -620,7 +620,7 @@ public void loadState(final SolverState solverState) { if (learnt.getLearntOnState() <= solverState.getId()) { learnts.set(newLearntsLength++, learnt); } else { - simpleRemoveClause(learnt); + detachClause(learnt); } } learnts.shrinkTo(newLearntsLength); @@ -845,27 +845,18 @@ protected void detachClause(final LNGClause c) { * @param c the clause to remove */ protected void removeClause(final LNGClause c) { - if (c.isAtMost()) { - detachAtMost(c); - for (int i = 0; i < c.atMostWatchers(); i++) { - if (value(c.get(i)) == Tristate.FALSE && v(c.get(i)).reason() != null && v(c.get(i)).reason() == c) { - v(c.get(i)).setReason(null); - } - } - } else { - if (config.proofGeneration) { - final LNGIntVector vec = new LNGIntVector(c.size()); - vec.push(-1); - for (int i = 0; i < c.size(); i++) { - vec.push((var(c.get(i)) + 1) * (-2 * (sign(c.get(i)) ? 1 : 0) + 1)); - } - pgProof.push(vec); - } - - detachClause(c); - if (locked(c)) { - v(c.get(0)).setReason(null); + assert !c.isAtMost(); + if (config.proofGeneration) { + final LNGIntVector vec = new LNGIntVector(c.size()); + vec.push(-1); + for (int i = 0; i < c.size(); i++) { + vec.push((var(c.get(i)) + 1) * (-2 * (sign(c.get(i)) ? 1 : 0) + 1)); } + pgProof.push(vec); + } + detachClause(c); + if (locked(c)) { + v(c.get(0)).setReason(null); } } @@ -1072,22 +1063,12 @@ protected void analyzeAssumptionConflict(final int p) { protected void cancelUntil(final int level) { if (decisionLevel() > level) { - if (!computingBackbone) { - for (int c = trail.size() - 1; c >= trailLim.get(level); c--) { - final int x = var(trail.get(c)); - final LNGVariable v = vars.get(x); - v.assign(Tristate.UNDEF); - v.setPolarity(sign(trail.get(c))); - insertVarOrder(x); - } - } else { - for (int c = trail.size() - 1; c >= trailLim.get(level); c--) { - final int x = var(trail.get(c)); - final LNGVariable v = vars.get(x); - v.assign(Tristate.UNDEF); - v.setPolarity(!computingBackbone && sign(trail.get(c))); - insertVarOrder(x); - } + for (int c = trail.size() - 1; c >= trailLim.get(level); c--) { + final int x = var(trail.get(c)); + final LNGVariable v = vars.get(x); + v.assign(Tristate.UNDEF); + v.setPolarity(!computingBackbone && sign(trail.get(c))); + insertVarOrder(x); } qhead = trailLim.get(level); trail.removeElements(trail.size() - trailLim.get(level)); @@ -1545,58 +1526,39 @@ public void addAtMost(final LNGIntVector ps, final int rhs) { attachClause(cr); } - /** - * Detaches a given at-most clause. - * @param c the at-most clause. - */ - protected void detachAtMost(final LNGClause c) { - for (int i = 0; i < c.atMostWatchers(); i++) { - watches.get(c.get(i)).remove(new LNGWatcher(c, c.get(i))); - } - clausesLiterals -= c.size(); - } - protected int findNewWatchForAtMostClause(final LNGClause c, final int p) { assert c.isAtMost(); - int newWatch = LIT_ERROR; int numFalse = 0; int numTrue = 0; final int maxTrue = c.size() - c.atMostWatchers() + 1; for (int q = 0; q < c.atMostWatchers(); q++) { - final Tristate val = value(c.get(q)); - if (val == Tristate.UNDEF) { - continue; - } else if (val == Tristate.FALSE) { - numFalse++; - if (numFalse >= c.atMostWatchers() - 1) { - return p; - } - continue; - } - assert val == Tristate.TRUE; - numTrue++; - if (numTrue > maxTrue) { - return LIT_ERROR; - } - if (c.get(q) == p) { - assert newWatch == LIT_ERROR; - for (int next = c.atMostWatchers(); next < c.size(); next++) { - if (value(c.get(next)) != Tristate.TRUE) { - newWatch = c.get(next); - c.set(next, c.get(q)); - c.set(q, newWatch); - return newWatch; + switch (value(c.get(q))) { + case UNDEF: + continue; + case FALSE: + numFalse++; + if (numFalse >= c.atMostWatchers() - 1) { + return p; + } + continue; + case TRUE: + numTrue++; + if (numTrue > maxTrue) { + return LIT_ERROR; + } + if (c.get(q) == p) { + for (int next = c.atMostWatchers(); next < c.size(); next++) { + if (value(c.get(next)) != Tristate.TRUE) { + final int newWatch = c.get(next); + c.set(next, c.get(q)); + c.set(q, newWatch); + return newWatch; + } + } } - } - newWatch = LIT_UNDEF; } } - assert newWatch == LIT_UNDEF; - if (numTrue > 1) { - return LIT_ERROR; - } else { - return LIT_UNDEF; - } + return numTrue > 1 ? LIT_ERROR : LIT_UNDEF; } /**