From e7bd4e835a72c2422d02be5df3a82ab0f7b0960c Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Fri, 5 Apr 2024 10:14:00 +0200 Subject: [PATCH] some refactoring --- .../dnnf/DnnfCoreSolver.java | 19 ++----- .../datastructures/LNGBoundedLongQueue.java | 42 ++------------- .../solvers/maxsat/algorithms/IncWBO.java | 16 +++--- .../solvers/maxsat/algorithms/MSU3.java | 22 ++++---- .../solvers/maxsat/algorithms/OLL.java | 32 +++++------ .../solvers/maxsat/algorithms/WBO.java | 16 +++--- .../solvers/maxsat/algorithms/WMSU3.java | 30 +++++------ .../logicng/solvers/sat/LNGCoreSolver.java | 54 +++++++++---------- .../solvers/sat/SATSolverLowLevelConfig.java | 32 +---------- .../logicng/LogicNGVersionTest.java | 12 +++++ .../solvers/sat/ConfigurationsTest.java | 4 -- .../solvers/sat/LNGCoreSolverTest.java | 2 +- 12 files changed, 105 insertions(+), 176 deletions(-) diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCoreSolver.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCoreSolver.java index c84bb0bf..7f2038be 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCoreSolver.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCoreSolver.java @@ -10,7 +10,6 @@ import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.solvers.datastructures.LNGClause; -import com.booleworks.logicng.solvers.datastructures.LNGVariable; import com.booleworks.logicng.solvers.sat.LNGCoreSolver; import com.booleworks.logicng.solvers.sat.SATSolverConfig; @@ -143,7 +142,9 @@ public boolean assertCdLiteral() { uncheckedEnqueue(lastLearnt.get(0), null); unitClauses.push(lastLearnt.get(0)); } else { - final LNGClause cr = new LNGClause(lastLearnt, stateId); + final LNGClause cr = new LNGClause(lastLearnt, nextStateId); + cr.setLBD(analyzeLBD); + cr.setOneWatched(false); learnts.push(cr); attachClause(cr); claBumpActivity(cr); @@ -151,11 +152,6 @@ public boolean assertCdLiteral() { } varDecayActivity(); claDecayActivity(); - if (--learntsizeAdjustCnt == 0) { - learntsizeAdjustConfl *= learntsizeAdjustInc; - learntsizeAdjustCnt = (int) learntsizeAdjustConfl; - maxLearnts *= llConfig.learntsizeInc; - } return propagateAfterDecide(); } @@ -203,15 +199,8 @@ protected void cancelUntil(final int level) { final int l = trail.get(c); assignment[l] = Tristate.UNDEF; assignment[l ^ 1] = Tristate.UNDEF; - final int x = var(l); - final LNGVariable v = vars.get(x); - v.assign(Tristate.UNDEF); - v.setPolarity(sign(trail.get(c))); - insertVarOrder(x); } - qhead = trailLim.get(level); - trail.removeElements(trail.size() - trailLim.get(level)); - trailLim.removeElements(trailLim.size() - level); + super.cancelUntil(level); } } diff --git a/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGBoundedLongQueue.java b/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGBoundedLongQueue.java index a72f7ee2..abb1b5b4 100644 --- a/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGBoundedLongQueue.java +++ b/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGBoundedLongQueue.java @@ -94,7 +94,11 @@ public LNGBoundedLongQueue() { * @param size the size */ public void initSize(final int size) { - growTo(size); + elems.growTo(size, 0); + first = 0; + maxSize = size; + queueSize = 0; + last = 0; } /** @@ -135,18 +139,6 @@ public boolean valid() { return queueSize == maxSize; } - /** - * Grows this queue to a given size. - * @param size the size - */ - private void growTo(final int size) { - elems.growTo(size, 0); - first = 0; - maxSize = size; - queueSize = 0; - last = 0; - } - /** * Performs a fast clear of this queue (the elements are left untouched). */ @@ -157,30 +149,6 @@ public void fastClear() { sumOfQueue = 0; } - LNGLongVector getElems() { - return elems; - } - - int getFirst() { - return first; - } - - int getLast() { - return last; - } - - long getSumOfQueue() { - return sumOfQueue; - } - - int getMaxSize() { - return maxSize; - } - - int getQueueSize() { - return queueSize; - } - @Override public String toString() { return String.format("LNGBoundedLongQueue{first=%d, last=%d, sumOfQueue=%d, maxSize=%d, queueSize=%d, elems=%s}", diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/IncWBO.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/IncWBO.java index 06ebe8df..2851b155 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/IncWBO.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/IncWBO.java @@ -323,16 +323,16 @@ protected MaxSATResult weightSearch() { return MaxSATResult.UNDEF; } else if (res == FALSE) { nbCores++; - assert solver.conflict().size() > 0; - final int coreCost = computeCostCore(solver.conflict()); + assert solver.assumptionsConflict().size() > 0; + final int coreCost = computeCostCore(solver.assumptionsConflict()); lbCost += coreCost; if (verbosity != MaxSATConfig.Verbosity.NONE) { - output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost); + output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost); } if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - relaxCore(solver.conflict(), coreCost); + relaxCore(solver.assumptionsConflict(), coreCost); incrementalBuildWeightSolver(weightStrategy); } else { nbSatisfiable++; @@ -421,11 +421,11 @@ protected MaxSATResult normalSearch() { return MaxSATResult.UNDEF; } else if (res == FALSE) { nbCores++; - assert solver.conflict().size() > 0; - final int coreCost = computeCostCore(solver.conflict()); + assert solver.assumptionsConflict().size() > 0; + final int coreCost = computeCostCore(solver.assumptionsConflict()); lbCost += coreCost; if (verbosity != MaxSATConfig.Verbosity.NONE) { - output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost); + output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost); } if (lbCost == ubCost) { if (verbosity != MaxSATConfig.Verbosity.NONE) { @@ -436,7 +436,7 @@ protected MaxSATResult normalSearch() { if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - relaxCore(solver.conflict(), coreCost); + relaxCore(solver.assumptionsConflict(), coreCost); } else { nbSatisfiable++; ubCost = incComputeCostModel(solver.model()); diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java index 20e91c44..90654f6d 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java @@ -152,10 +152,10 @@ protected MaxSATResult none() { } else if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - sumSizeCores += solver.conflict().size(); - for (int i = 0; i < solver.conflict().size(); i++) { - assert !activeSoft.get(coreMapping.get(solver.conflict().get(i))); - activeSoft.set(coreMapping.get(solver.conflict().get(i)), true); + sumSizeCores += solver.assumptionsConflict().size(); + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + assert !activeSoft.get(coreMapping.get(solver.assumptionsConflict().get(i))); + activeSoft.set(coreMapping.get(solver.assumptionsConflict().get(i)), true); } currentObjFunction.clear(); assumptions.clear(); @@ -232,19 +232,19 @@ protected MaxSATResult iterative() { } return MaxSATResult.OPTIMUM; } - sumSizeCores += solver.conflict().size(); - if (solver.conflict().size() == 0) { + sumSizeCores += solver.assumptionsConflict().size(); + if (solver.assumptionsConflict().size() == 0) { return MaxSATResult.UNSATISFIABLE; } if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } joinObjFunction.clear(); - for (int i = 0; i < solver.conflict().size(); i++) { - if (coreMapping.containsKey(solver.conflict().get(i))) { - assert !activeSoft.get(coreMapping.get(solver.conflict().get(i))); - activeSoft.set(coreMapping.get(solver.conflict().get(i)), true); - joinObjFunction.push(softClauses.get(coreMapping.get(solver.conflict().get(i))).relaxationVars().get(0)); + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + if (coreMapping.containsKey(solver.assumptionsConflict().get(i))) { + assert !activeSoft.get(coreMapping.get(solver.assumptionsConflict().get(i))); + activeSoft.set(coreMapping.get(solver.assumptionsConflict().get(i)), true); + joinObjFunction.push(softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).relaxationVars().get(0)); } } currentObjFunction.clear(); diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/OLL.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/OLL.java index fef53d12..2ad268ed 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/OLL.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/OLL.java @@ -146,16 +146,16 @@ private MaxSATResult unweighted() { assert nbSatisfiable > 0; return MaxSATResult.OPTIMUM; } - sumSizeCores += solver.conflict().size(); + sumSizeCores += solver.assumptionsConflict().size(); final LNGIntVector softRelax = new LNGIntVector(); final LNGIntVector cardinalityRelax = new LNGIntVector(); - for (int i = 0; i < solver.conflict().size(); i++) { - final int p = solver.conflict().get(i); + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + final int p = solver.assumptionsConflict().get(i); if (coreMapping.containsKey(p)) { assert !activeSoft.get(coreMapping.get(p)); - activeSoft.set(coreMapping.get(solver.conflict().get(i)), true); - assert p == softClauses.get(coreMapping.get(solver.conflict().get(i))).relaxationVars().get(0); + activeSoft.set(coreMapping.get(solver.assumptionsConflict().get(i)), true); + assert p == softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).relaxationVars().get(0); softRelax.push(p); } @@ -165,7 +165,7 @@ private MaxSATResult unweighted() { cardinalityRelax.push(p); // this is a soft cardinality -- bound must be increased - final IntTriple softId = boundMapping.get(solver.conflict().get(i)); + final IntTriple softId = boundMapping.get(solver.assumptionsConflict().get(i)); // // increase the bound assert softId.id < softCardinality.size(); assert softCardinality.get(softId.id).hasCardEncoding(); @@ -298,16 +298,16 @@ private MaxSATResult weighted() { } else if (res == Tristate.FALSE) { // reduce the weighted to the unweighted case int minCore = Integer.MAX_VALUE; - for (int i = 0; i < solver.conflict().size(); i++) { - final int p = solver.conflict().get(i); + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + final int p = solver.assumptionsConflict().get(i); if (coreMapping.containsKey(p)) { assert !activeSoft.get(coreMapping.get(p)); - if (softClauses.get(coreMapping.get(solver.conflict().get(i))).weight() < minCore) { - minCore = softClauses.get(coreMapping.get(solver.conflict().get(i))).weight(); + if (softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight() < minCore) { + minCore = softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight(); } } if (boundMapping.containsKey(p)) { - final IntTriple softId = boundMapping.get(solver.conflict().get(i)); + final IntTriple softId = boundMapping.get(solver.assumptionsConflict().get(i)); if (softId.weight < minCore) { minCore = softId.weight; } @@ -322,12 +322,12 @@ private MaxSATResult weighted() { assert nbSatisfiable > 0; return MaxSATResult.OPTIMUM; } - sumSizeCores += solver.conflict().size(); + sumSizeCores += solver.assumptionsConflict().size(); final LNGIntVector softRelax = new LNGIntVector(); final LNGIntVector cardinalityRelax = new LNGIntVector(); - for (int i = 0; i < solver.conflict().size(); i++) { - final int p = solver.conflict().get(i); + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + final int p = solver.assumptionsConflict().get(i); if (coreMapping.containsKey(p)) { if (softClauses.get(coreMapping.get(p)).weight() > minCore) { assert !activeSoft.get(coreMapping.get(p)); @@ -366,7 +366,7 @@ private MaxSATResult weighted() { assert softClauses.get(coreMapping.get(l)).weight() == minCore; assert activeSoft.size() == nSoft(); } else { - assert softClauses.get(coreMapping.get(solver.conflict().get(i))).weight() == minCore; + assert softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight() == minCore; softRelax.push(p); assert !activeSoft.get(coreMapping.get(p)); activeSoft.set(coreMapping.get(p), true); @@ -375,7 +375,7 @@ private MaxSATResult weighted() { if (boundMapping.containsKey(p)) { assert cardinalityAssumptions.contains(p); // this is a soft cardinality -- bound must be increased - final IntTriple softId = boundMapping.get(solver.conflict().get(i)); + final IntTriple softId = boundMapping.get(solver.assumptionsConflict().get(i)); // increase the bound assert softId.id < softCardinality.size(); diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WBO.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WBO.java index ff47a6c1..3db0e4bc 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WBO.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WBO.java @@ -460,16 +460,16 @@ protected MaxSATResult weightSearch() { return MaxSATResult.UNDEF; } else if (res == FALSE) { nbCores++; - assert solver.conflict().size() > 0; - final int coreCost = computeCostCore(solver.conflict()); + assert solver.assumptionsConflict().size() > 0; + final int coreCost = computeCostCore(solver.assumptionsConflict()); lbCost += coreCost; if (verbosity != Verbosity.NONE) { - output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost); + output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost); } if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - relaxCore(solver.conflict(), coreCost, assumptions); + relaxCore(solver.assumptionsConflict(), coreCost, assumptions); solver = rebuildWeightSolver(weightStrategy); } else { nbSatisfiable++; @@ -526,11 +526,11 @@ protected MaxSATResult normalSearch() { return MaxSATResult.UNDEF; } else if (res == FALSE) { nbCores++; - assert solver.conflict().size() > 0; - final int coreCost = computeCostCore(solver.conflict()); + assert solver.assumptionsConflict().size() > 0; + final int coreCost = computeCostCore(solver.assumptionsConflict()); lbCost += coreCost; if (verbosity != Verbosity.NONE) { - output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.conflict().size(), coreCost); + output.printf("c LB : %d CS : %d W : %d%n", lbCost, solver.assumptionsConflict().size(), coreCost); } if (lbCost == ubCost) { if (verbosity != Verbosity.NONE) { @@ -540,7 +540,7 @@ protected MaxSATResult normalSearch() { } else if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - relaxCore(solver.conflict(), coreCost, assumptions); + relaxCore(solver.assumptionsConflict(), coreCost, assumptions); solver = rebuildSolver(); } else { nbSatisfiable++; diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WMSU3.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WMSU3.java index 740630a8..e36d7614 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WMSU3.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/WMSU3.java @@ -194,15 +194,15 @@ protected MaxSATResult iterative() { } else if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - sumSizeCores += solver.conflict().size(); + sumSizeCores += solver.assumptionsConflict().size(); objFunction.clear(); coeffs.clear(); assumptions.clear(); - for (int i = 0; i < solver.conflict().size(); i++) { - if (!coreMapping.containsKey(solver.conflict().get(i))) { + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + if (!coreMapping.containsKey(solver.assumptionsConflict().get(i))) { continue; } - final int indexSoft = coreMapping.get(solver.conflict().get(i)); + final int indexSoft = coreMapping.get(solver.assumptionsConflict().get(i)); if (!activeSoft.get(indexSoft)) { activeSoft.set(indexSoft, true); objFunction.push(softClauses.get(indexSoft).relaxationVars().get(0)); @@ -288,9 +288,9 @@ protected MaxSATResult none() { } else if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - sumSizeCores += solver.conflict().size(); - for (int i = 0; i < solver.conflict().size(); i++) { - final int indexSoft = coreMapping.get(solver.conflict().get(i)); + sumSizeCores += solver.assumptionsConflict().size(); + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + final int indexSoft = coreMapping.get(solver.assumptionsConflict().get(i)); assert !activeSoft.get(indexSoft); activeSoft.set(indexSoft, true); } @@ -437,18 +437,18 @@ protected MaxSATResult iterativeBmo() { } else if (!foundLowerBound(lbCost, null)) { return MaxSATResult.UNDEF; } - sumSizeCores += solver.conflict().size(); + sumSizeCores += solver.assumptionsConflict().size(); joinObjFunction.clear(); joinCoeffs.clear(); - for (int i = 0; i < solver.conflict().size(); i++) { - if (coreMapping.containsKey(solver.conflict().get(i))) { - if (activeSoft.get(coreMapping.get(solver.conflict().get(i)))) { + for (int i = 0; i < solver.assumptionsConflict().size(); i++) { + if (coreMapping.containsKey(solver.assumptionsConflict().get(i))) { + if (activeSoft.get(coreMapping.get(solver.assumptionsConflict().get(i)))) { continue; } - assert softClauses.get(coreMapping.get(solver.conflict().get(i))).weight() == currentWeight; - activeSoft.set(coreMapping.get(solver.conflict().get(i)), true); - joinObjFunction.push(softClauses.get(coreMapping.get(solver.conflict().get(i))).relaxationVars().get(0)); - joinCoeffs.push(softClauses.get(coreMapping.get(solver.conflict().get(i))).weight()); + assert softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight() == currentWeight; + activeSoft.set(coreMapping.get(solver.assumptionsConflict().get(i)), true); + joinObjFunction.push(softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).relaxationVars().get(0)); + joinCoeffs.push(softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight()); } } objFunction.clear(); 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 193cc0a8..5c00c8b2 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java @@ -92,13 +92,14 @@ public class LNGCoreSolver { protected SATSolverLowLevelConfig llConfig; protected boolean inSatCall; - protected LNGIntVector validStates = new LNGIntVector(); - protected int stateId = 0; - // mapping of variable names to variable indices protected Map name2idx = new TreeMap<>(); protected Map idx2name = new TreeMap<>(); + // bookkeeping of solver states + protected LNGIntVector validStates = new LNGIntVector(); + protected int nextStateId = 0; + // internal solver state protected boolean ok = true; protected int qhead = 0; @@ -111,12 +112,14 @@ public class LNGCoreSolver { protected LNGIntVector trail = new LNGIntVector(); protected LNGIntVector trailLim = new LNGIntVector(); protected LNGBooleanVector model = new LNGBooleanVector(); - protected LNGIntVector conflict = new LNGIntVector(); + protected LNGIntVector assumptionsConflict = new LNGIntVector(); protected LNGIntVector assumptions = new LNGIntVector(); protected LNGVector assumptionPropositions = new LNGVector<>(); protected LNGBooleanVector seen = new LNGBooleanVector(); protected int analyzeBtLevel = 0; protected double claInc = 1; + protected double varInc; + protected double varDecay; protected int clausesLiterals = 0; protected int learntsLiterals = 0; @@ -129,23 +132,15 @@ public class LNGCoreSolver { protected LNGVector pgProof = new LNGVector<>(); // backbone computation + protected boolean computingBackbone = false; protected Stack backboneCandidates; protected LNGIntVector backboneAssumptions; protected HashMap backboneMap; - protected boolean computingBackbone = false; // Selection order protected LNGIntVector selectionOrder = new LNGIntVector(); protected int selectionOrderIdx = 0; - protected double varDecay; - protected double varInc; - protected double learntsizeAdjustConfl = 0; - protected int learntsizeAdjustCnt = 0; - protected int learntsizeAdjustStartConfl = 100; - protected double learntsizeAdjustInc = 1.5; - protected double maxLearnts = 0; - // internal glucose-related state protected LNGVector> watchesBin = new LNGVector<>(); protected LNGIntVector permDiff = new LNGIntVector(); @@ -487,7 +482,7 @@ public Tristate internalSolve(final SATHandler handler) { public Tristate internalSolve() { start(handler); model.clear(); - conflict.clear(); + assumptionsConflict.clear(); if (!ok) { return Tristate.FALSE; } @@ -507,7 +502,7 @@ public Tristate internalSolve() { for (final LNGVariable v : vars) { model.push(v.assignment() == Tristate.TRUE); } - } else if (status == Tristate.FALSE && conflict.empty()) { + } else if (status == Tristate.FALSE && assumptionsConflict.empty()) { ok = false; } finishSolving(handler); @@ -558,11 +553,11 @@ public boolean ok() { } /** - * Returns the current conflict of the solver or an empty vector if there is none. - * @return the current conflict of the solver + * Returns the conflict of the solver or an empty vector if there is none. + * @return the conflict of the solver */ - public LNGIntVector conflict() { - return conflict; + public LNGIntVector assumptionsConflict() { + return assumptionsConflict; } /** @@ -581,7 +576,7 @@ public SolverState saveState() { state[4] = pgOriginalClauses.size(); state[5] = pgProof.size(); } - final int id = stateId++; + final int id = nextStateId++; validStates.push(id); return new SolverState(id, state); } @@ -1036,13 +1031,12 @@ protected boolean litRedundant(final int p, final int abstractLevels, final LNGI } /** - * Analysis the final conflict if there were assumptions. - * @param p the conflicting literal - * @param outConflict the vector to store the final conflict + * Analyses the final conflict if there were assumptions. + * @param p the conflicting literal */ - protected void analyzeFinal(final int p, final LNGIntVector outConflict) { - outConflict.clear(); - outConflict.push(p); + protected void analyzeAssumptionConflict(final int p) { + assumptionsConflict.clear(); + assumptionsConflict.push(p); if (decisionLevel() == 0) { return; } @@ -1055,7 +1049,7 @@ protected void analyzeFinal(final int p, final LNGIntVector outConflict) { v = vars.get(x); if (v.reason() == null) { assert v.level() > 0; - outConflict.push(not(trail.get(i))); + assumptionsConflict.push(not(trail.get(i))); } else { final LNGClause c = v.reason(); if (!c.isAtMost()) { @@ -1204,7 +1198,7 @@ protected Tristate search() { uncheckedEnqueue(learntClause.get(0), null); unitClauses.push(learntClause.get(0)); } else { - final LNGClause cr = new LNGClause(learntClause, stateId); + final LNGClause cr = new LNGClause(learntClause, nextStateId); cr.setLBD(analyzeLBD); cr.setOneWatched(false); learnts.push(cr); @@ -1235,7 +1229,7 @@ protected Tristate search() { final int drupLit = (var(p) + 1) * (-2 * (sign(p) ? 1 : 0) + 1); pgOriginalClauses.push(new ProofInformation(new LNGIntVector(1, drupLit), assumptionPropositions.get(decisionLevel()))); } - analyzeFinal(not(p), conflict); + analyzeAssumptionConflict(not(p)); return Tristate.FALSE; } else { if (config.proofGeneration) { @@ -1668,7 +1662,7 @@ public String toString() { sb.append("#trailLim ").append(trailLim.size()).append(System.lineSeparator()); sb.append("model ").append(model).append(System.lineSeparator()); - sb.append("conflict ").append(conflict).append(System.lineSeparator()); + sb.append("conflict ").append(assumptionsConflict).append(System.lineSeparator()); sb.append("assumptions ").append(assumptions).append(System.lineSeparator()); sb.append("#seen ").append(seen.size()).append(System.lineSeparator()); diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java b/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java index 107ed966..e67e3caf 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java @@ -11,8 +11,6 @@ public final class SATSolverLowLevelConfig { final int restartFirst; final double restartInc; final double clauseDecay; - final double learntsizeFactor; - public final double learntsizeInc; // Glucose-related configuration final int lbLBDMinimizingClause; @@ -35,8 +33,6 @@ private SATSolverLowLevelConfig(final Builder builder) { restartFirst = builder.restartFirst; restartInc = builder.restartInc; clauseDecay = builder.clauseDecay; - learntsizeFactor = builder.learntsizeFactor; - learntsizeInc = builder.learntsizeInc; lbLBDMinimizingClause = builder.lbLBDMinimizingClause; lbLBDFrozenClause = builder.lbLBDFrozenClause; lbSizeMinimizingClause = builder.lbSizeMinimizingClause; @@ -64,8 +60,6 @@ public String toString() { sb.append("restartFirst=").append(restartFirst).append(System.lineSeparator()); sb.append("restartInc=").append(restartInc).append(System.lineSeparator()); sb.append("clauseDecay=").append(clauseDecay).append(System.lineSeparator()); - sb.append("learntsizeFactor=").append(learntsizeFactor).append(System.lineSeparator()); - sb.append("learntsizeInc=").append(learntsizeInc).append(System.lineSeparator()); sb.append("lbLBDMinimizingClause=").append(lbLBDMinimizingClause).append(System.lineSeparator()); sb.append("lbLBDFrozenClause=").append(lbLBDFrozenClause).append(System.lineSeparator()); sb.append("lbSizeMinimizingClause=").append(lbSizeMinimizingClause).append(System.lineSeparator()); @@ -89,8 +83,6 @@ public static class Builder { private int restartFirst = 100; private double restartInc = 2.0; private double clauseDecay = 0.999; - private double learntsizeFactor = 1.0 / 3.0; - private double learntsizeInc = 1.1; private int lbLBDMinimizingClause = 6; private int lbLBDFrozenClause = 30; private int lbSizeMinimizingClause = 30; @@ -160,28 +152,6 @@ public Builder clauseDecay(final double clauseDecay) { return this; } - /** - * Sets the initial limit for learnt clauses as a factor of the original clauses to the given value. The default - * value is 1/3. - * @param learntsizeFactor the value - * @return the builder - */ - public Builder lsFactor(final double learntsizeFactor) { - this.learntsizeFactor = learntsizeFactor; - return this; - } - - /** - * Sets the factor by which the limit for learnt clauses is multiplied every restart to a given value. The default - * value is 1.1. - * @param learntsizeInc the value - * @return the builder - */ - public Builder lsInc(final double learntsizeInc) { - this.learntsizeInc = learntsizeInc; - return this; - } - /** * Sets the minimal LBD required to minimize a clause to a given value. The default value is 6. * @param lbLBDMinimizingClause the value (should be at least 3) @@ -314,7 +284,7 @@ public Builder maxVarDecay(final double maxVarDecay) { this.maxVarDecay = maxVarDecay; return this; } - + /** * Builds the SAT solver configuration. * @return the configuration diff --git a/src/test/java/com/booleworks/logicng/LogicNGVersionTest.java b/src/test/java/com/booleworks/logicng/LogicNGVersionTest.java index 143aad1e..7a741125 100644 --- a/src/test/java/com/booleworks/logicng/LogicNGVersionTest.java +++ b/src/test/java/com/booleworks/logicng/LogicNGVersionTest.java @@ -8,6 +8,9 @@ import static org.mockito.Mockito.anyString; import static org.mockito.Mockito.mockStatic; +import com.booleworks.logicng.formulas.FormulaFactory; +import com.booleworks.logicng.io.parsers.ParserException; +import com.booleworks.logicng.solvers.SATSolver; import org.junit.jupiter.api.Test; import org.junit.jupiter.api.extension.ExtendWith; import org.mockito.MockedStatic; @@ -16,6 +19,15 @@ @ExtendWith(MockitoExtension.class) public class LogicNGVersionTest { + @Test + public void test() throws ParserException { + final FormulaFactory f = FormulaFactory.caching(); + final SATSolver solver = SATSolver.newSolver(f); + solver.add(f.parse("(A | ~B) & (B | C)")); + solver.satCall().addFormulas(f.parse("~A"), f.parse("~C")).sat(); + System.out.println(solver); + } + @Test public void testMajor() { try (final MockedStatic versionMock = mockStatic(LogicNGVersion.class)) { diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java index 60ccd85f..2e7c749c 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java @@ -21,8 +21,6 @@ public void testSolverConfigToString() { .restartFirst(200) .restartInc(0.8) .clauseDecay(0.92) - .lsFactor(1.4) - .lsInc(1.5) .lbLBDMinimizingClause(3) .lbLBDFrozenClause(25) .lbSizeMinimizingClause(24) @@ -43,8 +41,6 @@ public void testSolverConfigToString() { "restartFirst=200%n" + "restartInc=0.8%n" + "clauseDecay=0.92%n" + - "learntsizeFactor=1.4%n" + - "learntsizeInc=1.5%n" + "lbLBDMinimizingClause=3%n" + "lbLBDFrozenClause=25%n" + "lbSizeMinimizingClause=24%n" + diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/LNGCoreSolverTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/LNGCoreSolverTest.java index 15b2ff41..99a11c69 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/LNGCoreSolverTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/LNGCoreSolverTest.java @@ -19,7 +19,7 @@ public class LNGCoreSolverTest { @Test - public void testAnalyzeFinal() { + public void testAnalyzeAssumptionConflict() { final LNGCoreSolver solver = new LNGCoreSolver(FormulaFactory.caching(), SATSolverConfig.builder().build()); solver.newVar(true, true); solver.newVar(true, true);