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 7f024833..fbce4654 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 @@ -118,7 +118,7 @@ protected void incrementalBuildWeightSolver(final MaxSATConfig.WeightStrategy st for (int i = 0; i < nVars(); i++) { newSATVariable(solver); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { solver.addClause(hardClauses.get(i).clause(), null); } if (symmetryStrategy) { @@ -128,7 +128,7 @@ protected void incrementalBuildWeightSolver(final MaxSATConfig.WeightStrategy st } LNGIntVector clause; nbCurrentSoft = 0; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= currentWeight && softClauses.get(i).weight() != 0) { nbCurrentSoft++; clause = new LNGIntVector(softClauses.get(i).clause()); @@ -157,8 +157,8 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) { addSoftClause(weightCore, clause, vars); final int l = newLiteral(false); newSATVariable(solver); - softClauses.get(nSoft() - 1).setAssumptionVar(l); - coreMapping.put(l, nSoft() - 1); + softClauses.get(softClauses.size() - 1).setAssumptionVar(l); + coreMapping.put(l, softClauses.size() - 1); incSoft.set(indexSoft, true); incSoft.push(false); for (int j = 0; j < vars.size(); j++) { @@ -174,7 +174,7 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) { softMapping.get(indexSoft).clear(); relaxationMapping.push(new LNGIntVector(relaxationMapping.get(indexSoft))); relaxationMapping.get(indexSoft).clear(); - symmetryLog(nSoft() - 1); + symmetryLog(softClauses.size() - 1); } } else { assert softClauses.get(indexSoft).weight() - weightCore > 0; @@ -191,8 +191,8 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) { incSoft.set(indexSoft, true); int l = newLiteral(false); newSATVariable(solver); - softClauses.get(nSoft() - 1).setAssumptionVar(l); - coreMapping.put(l, nSoft() - 1); + softClauses.get(softClauses.size() - 1).setAssumptionVar(l); + coreMapping.put(l, softClauses.size() - 1); incSoft.push(false); for (int j = 0; j < vars.size(); j++) { clause.push(vars.get(j)); @@ -210,8 +210,8 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) { addSoftClause(weightCore, clause, vars); l = newLiteral(false); newSATVariable(solver); - softClauses.get(nSoft() - 1).setAssumptionVar(l); - coreMapping.put(l, nSoft() - 1); + softClauses.get(softClauses.size() - 1).setAssumptionVar(l); + coreMapping.put(l, softClauses.size() - 1); incSoft.push(false); for (int j = 0; j < vars.size(); j++) { clause.push(vars.get(j)); @@ -224,7 +224,7 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore) { if (symmetryStrategy) { softMapping.push(new LNGIntVector()); relaxationMapping.push(new LNGIntVector()); - symmetryLog(nSoft() - 1); + symmetryLog(softClauses.size() - 1); } } } @@ -319,7 +319,7 @@ protected LNGResult weightSearch(final ComputationHandler initAssumptions(); updateCurrentWeight(weightStrategy); incrementalBuildWeightSolver(weightStrategy); - incSoft.growTo(nSoft(), false); + incSoft.growTo(softClauses.size(), false); while (true) { assumptions.clear(); for (int i = 0; i < incSoft.size(); i++) { @@ -346,7 +346,7 @@ protected LNGResult weightSearch(final ComputationHandler incrementalBuildWeightSolver(weightStrategy); } else { nbSatisfiable++; - if (nbCurrentSoft == nSoft()) { + if (nbCurrentSoft == softClauses.size()) { assert incComputeCostModel(solver.model()) == lbCost; if (lbCost == ubCost && verbosity != MaxSATConfig.Verbosity.NONE) { output.println("c LB = UB"); @@ -389,7 +389,7 @@ protected LNGResult weightSearch(final ComputationHandler protected int incComputeCostModel(final LNGBooleanVector currentModel) { assert currentModel.size() != 0; int currentCost = 0; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { boolean unsatisfied = true; for (int j = 0; j < softClauses.get(i).clause().size(); j++) { if (incSoft.get(i)) { @@ -422,7 +422,7 @@ protected LNGResult normalSearch(final ComputationHandler } initAssumptions(); solver = rebuildSolver(); - incSoft.growTo(nSoft(), false); + incSoft.growTo(softClauses.size(), false); while (true) { assumptions.clear(); for (int i = 0; i < incSoft.size(); i++) { diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearSU.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearSU.java index c566abd4..680523e2 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearSU.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearSU.java @@ -250,10 +250,10 @@ protected LNGCoreSolver rebuildSolver(final int minWeight) { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() < minWeight) { continue; } @@ -279,7 +279,7 @@ protected LNGCoreSolver rebuildBMO(final LNGVector functions, fina final LNGCoreSolver s = rebuildSolver(currentWeight); objFunction.clear(); coeffs.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() == currentWeight) { objFunction.push(softClauses.get(i).relaxationVars().get(0)); coeffs.push(softClauses.get(i).weight()); diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearUS.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearUS.java index b886b074..8b452a45 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearUS.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearUS.java @@ -212,11 +212,11 @@ protected LNGCoreSolver rebuildSolver() { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } LNGIntVector clause; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { clause = new LNGIntVector(softClauses.get(i).clause()); for (int j = 0; j < softClauses.get(i).relaxationVars().size(); j++) { clause.push(softClauses.get(i).relaxationVars().get(j)); @@ -227,7 +227,7 @@ protected LNGCoreSolver rebuildSolver() { } protected void initRelaxation(final LNGIntVector objFunction) { - for (int i = 0; i < nbSoft; i++) { + for (int i = 0; i < softClauses.size(); i++) { final int l = newLiteral(false); softClauses.get(i).relaxationVars().push(l); softClauses.get(i).setAssumptionVar(l); 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 4a2ce5c1..12c26385 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 @@ -101,8 +101,8 @@ protected LNGResult none(final ComputationHandler handler) final LNGIntVector assumptions = new LNGIntVector(); final LNGIntVector currentObjFunction = new LNGIntVector(); encoder.setIncremental(IncrementalStrategy.NONE); - final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false); - for (int i = 0; i < nSoft(); i++) { + final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false); + for (int i = 0; i < softClauses.size(); i++) { coreMapping.put(softClauses.get(i).assumptionVar(), i); } while (true) { @@ -155,7 +155,7 @@ protected LNGResult none(final ComputationHandler handler) } currentObjFunction.clear(); assumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (activeSoft.get(i)) { currentObjFunction.push(softClauses.get(i).relaxationVars().get(0)); } else { @@ -186,8 +186,8 @@ protected LNGResult iterative(final ComputationHandler han final LNGIntVector currentObjFunction = new LNGIntVector(); final LNGIntVector encodingAssumptions = new LNGIntVector(); encoder.setIncremental(IncrementalStrategy.ITERATIVE); - final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false); - for (int i = 0; i < nSoft(); i++) { + final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false); + for (int i = 0; i < softClauses.size(); i++) { coreMapping.put(softClauses.get(i).assumptionVar(), i); } while (true) { @@ -249,7 +249,7 @@ protected LNGResult iterative(final ComputationHandler han } currentObjFunction.clear(); assumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (activeSoft.get(i)) { currentObjFunction.push(softClauses.get(i).relaxationVars().get(0)); } else { @@ -282,11 +282,11 @@ protected LNGCoreSolver rebuildSolver() { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } LNGIntVector clause; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { clause = new LNGIntVector(softClauses.get(i).clause()); for (int j = 0; j < softClauses.get(i).relaxationVars().size(); j++) { clause.push(softClauses.get(i).relaxationVars().get(j)); @@ -297,7 +297,7 @@ protected LNGCoreSolver rebuildSolver() { } protected void initRelaxation(final LNGIntVector objFunction) { - for (int i = 0; i < nbSoft; i++) { + for (int i = 0; i < softClauses.size(); i++) { final int l = newLiteral(false); softClauses.get(i).relaxationVars().push(l); softClauses.get(i).setAssumptionVar(l); diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java index dcc240db..0cc71224 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java @@ -78,8 +78,6 @@ public enum ProblemType { int hardWeight; ProblemType problemType; int nbVars; - int nbSoft; - int nbHard; int nbInitialVariables; int nbCores; int nbSymmetryClauses; @@ -105,8 +103,6 @@ protected MaxSAT(final FormulaFactory f, final MaxSATConfig config) { hardWeight = Integer.MAX_VALUE; problemType = ProblemType.UNWEIGHTED; nbVars = 0; - nbSoft = 0; - nbHard = 0; nbInitialVariables = 0; currentWeight = 1; model = new LNGBooleanVector(); @@ -171,17 +167,16 @@ public final LNGResult search(final ComputationHandler han } protected StateBeforeSolving saveStateBeforeSolving() { - assert nbSoft == softClauses.size(); - final int[] softWeights = new int[nbSoft]; - for (int i = 0; i < nbSoft; i++) { + final int[] softWeights = new int[softClauses.size()]; + for (int i = 0; i < softClauses.size(); i++) { softWeights[i] = softClauses.get(i).weight(); } - return new StateBeforeSolving(nbVars, nbSoft, nbHard, ubCost, currentWeight, softWeights); + return new StateBeforeSolving(nbVars, hardClauses.size(), softClauses.size(), ubCost, currentWeight, softWeights); } protected void loadStateBeforeSolving(final StateBeforeSolving stateBeforeSolving) { - softClauses.shrinkTo(stateBeforeSolving.nbSoft); hardClauses.shrinkTo(stateBeforeSolving.nbHard); + softClauses.shrinkTo(stateBeforeSolving.nbSoft); orderWeights.clear(); for (int i = stateBeforeSolving.nbVars; i < nbVars; i++) { final Variable var = index2var.remove(i); @@ -190,8 +185,6 @@ protected void loadStateBeforeSolving(final StateBeforeSolving stateBeforeSolvin } } nbVars = stateBeforeSolving.nbVars; - nbSoft = stateBeforeSolving.nbSoft; - nbHard = stateBeforeSolving.nbHard; nbCores = 0; nbSymmetryClauses = 0; sumSizeCores = 0; @@ -223,26 +216,12 @@ public int nVars() { } /** - * Returns the number of soft clauses in the working MaxSAT formula. - * @return the number of soft clauses in the working MaxSAT formula - */ - public int nSoft() { - return nbSoft; - } - - /** - * Returns the number of hard clauses in the working MaxSAT formula. - * @return the number of hard clauses in the working MaxSAT formula + * Returns a new variable index and increases the internal number of + * variables. + * @return a new variable index */ - public int nHard() { - return nbHard; - } - - /** - * Increases the number of variables in the working MaxSAT formula. - */ - public void newVar() { - nbVars++; + public int newVar() { + return nbVars++; } /** @@ -251,7 +230,6 @@ public void newVar() { */ public void addHardClause(final LNGIntVector lits) { hardClauses.push(new LNGHardClause(lits)); - nbHard++; } /** @@ -272,7 +250,6 @@ public void addSoftClause(final int weight, final LNGIntVector lits) { */ protected void addSoftClause(final int weight, final LNGIntVector lits, final LNGIntVector vars) { softClauses.push(new LNGSoftClause(lits, weight, LIT_UNDEF, vars)); - nbSoft++; } /** @@ -328,9 +305,7 @@ public int literal(final Literal lit) { * @return the new literal */ public int newLiteral(final boolean sign) { - final int p = LNGCoreSolver.mkLit(nVars(), sign); - newVar(); - return p; + return LNGCoreSolver.mkLit(newVar(), sign); } /** @@ -411,7 +386,7 @@ public void saveModel(final LNGBooleanVector currentModel) { public int computeCostModel(final LNGBooleanVector currentModel, final int weight) { assert currentModel.size() != 0; int currentCost = 0; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { boolean unsatisfied = true; for (int j = 0; j < softClauses.get(i).clause().size(); j++) { if (weight != Integer.MAX_VALUE && softClauses.get(i).weight() != weight) { @@ -445,7 +420,7 @@ public boolean isBMO(final boolean cache) { boolean bmo = true; final SortedSet partitionWeights = new TreeSet<>(); final SortedMap nbPartitionWeights = new TreeMap<>(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { final int weight = softClauses.get(i).weight(); partitionWeights.add(weight); nbPartitionWeights.merge(weight, 1, Integer::sum); @@ -509,13 +484,13 @@ LNGEvent foundUpperBound(final int upperBound, final ComputationHandler handler) protected static class StateBeforeSolving { protected final int nbVars; - protected final int nbSoft; protected final int nbHard; + protected final int nbSoft; protected final int ubCost; protected final int currentWeight; protected final int[] softWeights; - protected StateBeforeSolving(final int nbVars, final int nbSoft, final int nbHard, final int ubCost, final int currentWeight, final int[] softWeights) { + protected StateBeforeSolving(final int nbVars, final int nbHard, final int nbSoft, final int ubCost, final int currentWeight, final int[] softWeights) { this.nbVars = nbVars; this.nbSoft = nbSoft; this.nbHard = nbHard; 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 a660454a..fc57727b 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 @@ -67,12 +67,12 @@ private LNGCoreSolver rebuildSolver() { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } LNGIntVector clause; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { clause = new LNGIntVector(softClauses.get(i).clause()); for (int j = 0; j < softClauses.get(i).relaxationVars().size(); j++) { clause.push(softClauses.get(i).relaxationVars().get(j)); @@ -95,8 +95,8 @@ private LNGResult unweighted(final ComputationHandler hand final LNGIntVector encodingAssumptions = new LNGIntVector(); encoder.setIncremental(MaxSATConfig.IncrementalStrategy.ITERATIVE); - final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false); - for (int i = 0; i < nSoft(); i++) { + final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false); + for (int i = 0; i < softClauses.size(); i++) { coreMapping.put(softClauses.get(i).assumptionVar(), i); } @@ -118,7 +118,7 @@ private LNGResult unweighted(final ComputationHandler hand if (newCost == 0) { return LNGResult.of(InternalMaxSATResult.optimum(ubCost, model)); } - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } } else { @@ -200,7 +200,7 @@ private LNGResult unweighted(final ComputationHandler hand // reset the assumptions assumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (!activeSoft.get(i)) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -224,8 +224,8 @@ private LNGResult weighted(final ComputationHandler handle final LNGIntVector encodingAssumptions = new LNGIntVector(); encoder.setIncremental(MaxSATConfig.IncrementalStrategy.ITERATIVE); - final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false); - for (int i = 0; i < nSoft(); i++) { + final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false); + for (int i = 0; i < softClauses.size(); i++) { coreMapping.put(softClauses.get(i).assumptionVar(), i); } @@ -247,7 +247,7 @@ private LNGResult weighted(final ComputationHandler handle } if (nbSatisfiable == 1) { minWeight = findNextWeightDiversity(minWeight, cardinalityAssumptions, boundMapping); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= minWeight) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -255,7 +255,7 @@ private LNGResult weighted(final ComputationHandler handle } else { // compute min weight in soft int notConsidered = 0; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() < minWeight) { notConsidered++; } @@ -270,7 +270,7 @@ private LNGResult weighted(final ComputationHandler handle if (notConsidered != 0) { minWeight = findNextWeightDiversity(minWeight, cardinalityAssumptions, boundMapping); assumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (!activeSoft.get(i) && softClauses.get(i).weight() >= minWeight) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -350,18 +350,18 @@ private LNGResult weighted(final ComputationHandler handle clause.push(l); solver.addClause(clause, null); assert clause.size() - 1 == softClauses.get(indexSoft).clause().size(); - assert softClauses.get(nSoft() - 1).relaxationVars().size() == 1; + assert softClauses.get(softClauses.size() - 1).relaxationVars().size() == 1; // Create a new assumption literal. - softClauses.get(nSoft() - 1).setAssumptionVar(l); - assert softClauses.get(nSoft() - 1).assumptionVar() == - softClauses.get(nSoft() - 1).relaxationVars().get(0); + softClauses.get(softClauses.size() - 1).setAssumptionVar(l); + assert softClauses.get(softClauses.size() - 1).assumptionVar() == + softClauses.get(softClauses.size() - 1).relaxationVars().get(0); // Map the new soft clause to its assumption // literal. - coreMapping.put(l, nSoft() - 1); + coreMapping.put(l, softClauses.size() - 1); softRelax.push(l); assert softClauses.get(coreMapping.get(l)).weight() == minCore; - assert activeSoft.size() == nSoft(); + assert activeSoft.size() == softClauses.size(); } else { assert softClauses.get(coreMapping.get(solver.assumptionsConflict().get(i))).weight() == minCore; @@ -448,7 +448,7 @@ private LNGResult weighted(final ComputationHandler handle cardinalityAssumptions.add(out); } assumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (!activeSoft.get(i) && softClauses.get(i).weight() >= minWeight) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -465,7 +465,7 @@ private LNGResult weighted(final ComputationHandler handle } private void initRelaxation() { - for (int i = 0; i < nbSoft; i++) { + for (int i = 0; i < softClauses.size(); i++) { final int l = newLiteral(false); softClauses.get(i).relaxationVars().push(l); softClauses.get(i).setAssumptionVar(l); @@ -485,7 +485,7 @@ private int findNextWeightDiversity(final int weight, final Set cardina } nbClauses = 0; nbWeights.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= nextWeight) { nbClauses++; nbWeights.add(softClauses.get(i).weight()); @@ -499,7 +499,7 @@ private int findNextWeightDiversity(final int weight, final Set cardina nbWeights.add(softId.weight); } } - if ((float) nbClauses / nbWeights.size() > alpha || nbClauses == nSoft() + cardinalityAssumptions.size()) { + if ((float) nbClauses / nbWeights.size() > alpha || nbClauses == softClauses.size() + cardinalityAssumptions.size()) { break; } if (nbSatisfiable == 1 && !findNext) { @@ -511,7 +511,7 @@ private int findNextWeightDiversity(final int weight, final Set cardina int findNextWeight(final int weight, final Set cardinalityAssumptions, final SortedMap boundMapping) { int nextWeight = 1; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() > nextWeight && softClauses.get(i).weight() < weight) { nextWeight = softClauses.get(i).weight(); } 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 fd164e94..850abef1 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 @@ -123,7 +123,7 @@ protected LNGCoreSolver rebuildWeightSolver(final WeightStrategy strategy) { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } if (symmetryStrategy) { @@ -131,7 +131,7 @@ protected LNGCoreSolver rebuildWeightSolver(final WeightStrategy strategy) { } LNGIntVector clause = new LNGIntVector(); nbCurrentSoft = 0; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= currentWeight) { nbCurrentSoft++; clause.clear(); @@ -153,14 +153,14 @@ LNGCoreSolver rebuildSolver() { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } if (symmetryStrategy) { symmetryBreaking(); } LNGIntVector clause; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { clause = new LNGIntVector(softClauses.get(i).clause()); for (int j = 0; j < softClauses.get(i).relaxationVars().size(); j++) { clause.push(softClauses.get(i).relaxationVars().get(j)); @@ -176,24 +176,28 @@ protected LNGCoreSolver rebuildHardSolver() { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } return s; } void updateCurrentWeight(final WeightStrategy strategy) { - assert strategy == WeightStrategy.NORMAL || strategy == WeightStrategy.DIVERSIFY; - if (strategy == WeightStrategy.NORMAL) { - currentWeight = findNextWeight(currentWeight); - } else if (strategy == WeightStrategy.DIVERSIFY) { - currentWeight = findNextWeightDiversity(currentWeight); + switch (strategy) { + case NORMAL: + currentWeight = findNextWeight(currentWeight); + break; + case DIVERSIFY: + currentWeight = findNextWeightDiversity(currentWeight); + break; + default: + throw new IllegalArgumentException("Unknown strategy: " + strategy); } } protected int findNextWeight(final int weight) { int nextWeight = 1; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() > nextWeight && softClauses.get(i).weight() < weight) { nextWeight = softClauses.get(i).weight(); } @@ -215,13 +219,13 @@ protected int findNextWeightDiversity(final int weight) { } nbClauses = 0; nbWeights.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= nextWeight) { nbClauses++; nbWeights.add(softClauses.get(i).weight()); } } - if ((double) nbClauses / nbWeights.size() > alpha || nbClauses == nSoft()) { + if ((double) nbClauses / nbWeights.size() > alpha || nbClauses == softClauses.size()) { break; } if (nbSatisfiable == 1 && !findNext) { @@ -308,13 +312,13 @@ protected void relaxCore(final LNGIntVector conflict, final int weightCore, fina lits.push(p); addSoftClause(weightCore, clause, vars); final int l = newLiteral(false); - softClauses.get(nSoft() - 1).setAssumptionVar(l); + softClauses.get(softClauses.size() - 1).setAssumptionVar(l); // Map the new soft clause to its assumption literal - coreMapping.put(l, nSoft() - 1); + coreMapping.put(l, softClauses.size() - 1); // Update the assumption vector assumps.push(LNGCoreSolver.not(l)); if (symmetryStrategy) { - symmetryLog(nSoft() - 1); + symmetryLog(softClauses.size() - 1); } } } @@ -338,7 +342,7 @@ int computeCostCore(final LNGIntVector conflict) { } void initSymmetry() { - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { softMapping.push(new LNGIntVector()); relaxationMapping.push(new LNGIntVector()); } @@ -480,7 +484,7 @@ protected LNGResult weightSearch(final ComputationHandler solver = rebuildWeightSolver(weightStrategy); } else { nbSatisfiable++; - if (nbCurrentSoft == nSoft()) { + if (nbCurrentSoft == softClauses.size()) { assert computeCostModel(solver.model(), Integer.MAX_VALUE) == lbCost; if (lbCost == ubCost && verbosity != Verbosity.NONE) { output.println("c LB = UB"); @@ -568,7 +572,7 @@ protected LNGResult normalSearch(final ComputationHandler } void initAssumptions() { - for (int i = 0; i < nbSoft; i++) { + for (int i = 0; i < softClauses.size(); i++) { final int l = newLiteral(false); softClauses.get(i).setAssumptionVar(l); coreMapping.put(l, i); 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 c849ffb3..1615aafd 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 @@ -129,8 +129,8 @@ protected LNGResult iterative(final ComputationHandler han initRelaxation(); final LNGCoreSolver solver = rebuildSolver(); encoder.setIncremental(MaxSATConfig.IncrementalStrategy.ITERATIVE); - final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false); - for (int i = 0; i < nSoft(); i++) { + final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false); + for (int i = 0; i < softClauses.size(); i++) { coreMapping.put(softClauses.get(i).assumptionVar(), i); } final LNGIntVector assumptions = new LNGIntVector(); @@ -161,7 +161,7 @@ protected LNGResult iterative(final ComputationHandler han return LNGResult.canceled(upperBoundEvent); } } - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= currentWeight && !activeSoft.get(i)) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -197,7 +197,7 @@ protected LNGResult iterative(final ComputationHandler han coeffs.push(softClauses.get(indexSoft).weight()); } } - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (!activeSoft.get(i) && softClauses.get(i).weight() >= currentWeight) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -207,7 +207,7 @@ protected LNGResult iterative(final ComputationHandler han fullObjFunction.push(objFunction.get(i)); } if (verbosity != MaxSATConfig.Verbosity.NONE) { - output.printf("c Relaxed soft clauses %d / %d%n", fullCoeffsFunction.size(), nSoft()); + output.printf("c Relaxed soft clauses %d / %d%n", fullCoeffsFunction.size(), softClauses.size()); } lbCost++; while (!subsetSum(fullCoeffsFunction, lbCost)) { @@ -217,7 +217,7 @@ protected LNGResult iterative(final ComputationHandler han output.println("c LB : " + lbCost); } if (!encoder.hasPBEncoding()) { - encoder.incEncodePB(solver, objFunction, coeffs, lbCost, assumptions, nSoft()); + encoder.incEncodePB(solver, objFunction, coeffs, lbCost, assumptions, softClauses.size()); } else { encoder.incUpdatePB(solver, objFunction, coeffs, lbCost); encoder.incUpdatePBAssumptions(assumptions); @@ -232,8 +232,8 @@ protected LNGResult none(final ComputationHandler handler) initRelaxation(); LNGCoreSolver solver = rebuildSolver(); encoder.setIncremental(MaxSATConfig.IncrementalStrategy.NONE); - final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false); - for (int i = 0; i < nSoft(); i++) { + final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false); + for (int i = 0; i < softClauses.size(); i++) { coreMapping.put(softClauses.get(i).assumptionVar(), i); } final LNGIntVector assumptions = new LNGIntVector(); @@ -261,7 +261,7 @@ protected LNGResult none(final ComputationHandler handler) return LNGResult.canceled(upperBoundEvent); } } - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= currentWeight && !activeSoft.get(i)) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -291,7 +291,7 @@ protected LNGResult none(final ComputationHandler handler) final LNGIntVector objFunction = new LNGIntVector(); coeffs.clear(); assumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (activeSoft.get(i)) { objFunction.push(softClauses.get(i).relaxationVars().get(0)); coeffs.push(softClauses.get(i).weight()); @@ -300,7 +300,7 @@ protected LNGResult none(final ComputationHandler handler) } } if (verbosity != MaxSATConfig.Verbosity.NONE) { - output.printf("c Relaxed soft clauses %d / %d%n", objFunction.size(), nSoft()); + output.printf("c Relaxed soft clauses %d / %d%n", objFunction.size(), softClauses.size()); } solver = rebuildSolver(); lbCost++; @@ -324,8 +324,8 @@ protected LNGResult iterativeBmo(final ComputationHandler final LNGIntVector joinObjFunction = new LNGIntVector(); final LNGIntVector encodingAssumptions = new LNGIntVector(); final LNGIntVector joinCoeffs = new LNGIntVector(); - final LNGBooleanVector activeSoft = new LNGBooleanVector(nSoft(), false); - for (int i = 0; i < nSoft(); i++) { + final LNGBooleanVector activeSoft = new LNGBooleanVector(softClauses.size(), false); + for (int i = 0; i < softClauses.size(); i++) { coreMapping.put(softClauses.get(i).assumptionVar(), i); } int minWeight = 0; @@ -371,7 +371,7 @@ protected LNGResult iterativeBmo(final ComputationHandler assert orderWeights.get(0) > 1; minWeight = orderWeights.get(orderWeights.size() - 1); currentWeight = orderWeights.get(0); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (softClauses.get(i).weight() >= currentWeight) { assumptions.push(LNGCoreSolver.not(softClauses.get(i).assumptionVar())); } @@ -403,7 +403,7 @@ protected LNGResult iterativeBmo(final ComputationHandler solver.addClause(encodingAssumptions.get(i), null); } encodingAssumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (!activeSoft.get(i) && previousWeight == softClauses.get(i).weight()) { solver.addClause(LNGCoreSolver.not(softClauses.get(i).assumptionVar()), null); } @@ -457,7 +457,7 @@ protected LNGResult iterativeBmo(final ComputationHandler objFunction.clear(); coeffs.clear(); assumptions.clear(); - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { if (activeSoft.get(i)) { assert softClauses.get(i).weight() == currentWeight; objFunction.push(softClauses.get(i).relaxationVars().get(0)); @@ -467,7 +467,7 @@ protected LNGResult iterativeBmo(final ComputationHandler } } if (verbosity != MaxSATConfig.Verbosity.NONE) { - output.printf("c Relaxed soft clauses %d / %d%n", objFunction.size(), nSoft()); + output.printf("c Relaxed soft clauses %d / %d%n", objFunction.size(), softClauses.size()); } assert posWeight < functions.size(); functions.set(posWeight, new LNGIntVector(objFunction)); @@ -496,11 +496,11 @@ protected LNGCoreSolver rebuildSolver() { for (int i = 0; i < nVars(); i++) { newSATVariable(s); } - for (int i = 0; i < nHard(); i++) { + for (int i = 0; i < hardClauses.size(); i++) { s.addClause(hardClauses.get(i).clause(), null); } LNGIntVector clause; - for (int i = 0; i < nSoft(); i++) { + for (int i = 0; i < softClauses.size(); i++) { clause = new LNGIntVector(softClauses.get(i).clause()); for (int j = 0; j < softClauses.get(i).relaxationVars().size(); j++) { clause.push(softClauses.get(i).relaxationVars().get(j)); @@ -511,7 +511,7 @@ protected LNGCoreSolver rebuildSolver() { } protected void initRelaxation() { - for (int i = 0; i < nbSoft; i++) { + for (int i = 0; i < softClauses.size(); i++) { final int l = newLiteral(false); softClauses.get(i).relaxationVars().push(l); softClauses.get(i).setAssumptionVar(l); diff --git a/src/main/java/com/booleworks/logicng/transformations/cnf/PlaistedGreenbaumTransformationMaxSATSolver.java b/src/main/java/com/booleworks/logicng/transformations/cnf/PlaistedGreenbaumTransformationMaxSATSolver.java index d86fec10..de41f0d0 100644 --- a/src/main/java/com/booleworks/logicng/transformations/cnf/PlaistedGreenbaumTransformationMaxSATSolver.java +++ b/src/main/java/com/booleworks/logicng/transformations/cnf/PlaistedGreenbaumTransformationMaxSATSolver.java @@ -282,11 +282,7 @@ private Pair getPgVar(final Formula formula, final boolean pol } private int newSolverVariable() { - final int index = solver.nVars(); - solver.newVar(); -// final String name = InternalAuxVarType.CNF.prefix() + "MAX_SAT_SOLVER_" + index; -// solver.addName(name, index); - return index * 2; + return solver.newVar() * 2; } private static LNGIntVector vector(final int... elts) {