diff --git a/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java b/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java index 726c0d4d..e27b7722 100644 --- a/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java @@ -23,6 +23,7 @@ import com.booleworks.logicng.solvers.maxsat.algorithms.MSU3; import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSAT; import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig; +import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATState; import com.booleworks.logicng.solvers.maxsat.algorithms.OLL; import com.booleworks.logicng.solvers.maxsat.algorithms.WBO; import com.booleworks.logicng.solvers.maxsat.algorithms.WMSU3; @@ -52,11 +53,11 @@ public enum Algorithm { protected final MaxSATConfig configuration; protected final Algorithm algorithm; - protected PlaistedGreenbaumTransformationMaxSATSolver pgTransformation; - protected FormulaFactory f; + protected final PlaistedGreenbaumTransformationMaxSATSolver pgTransformation; + protected final FormulaFactory f; + protected final MaxSAT solver; + protected final SortedSet selectorVariables; protected LNGResult result; - protected MaxSAT solver; - protected SortedSet selectorVariables; /** * Constructs a new MaxSAT solver with a given configuration. @@ -69,7 +70,36 @@ protected MaxSATSolver(final FormulaFactory f, final MaxSATConfig configuration, this.f = f; this.algorithm = algorithm; this.configuration = configuration; - reset(); + result = null; + selectorVariables = new TreeSet<>(); + switch (algorithm) { + case WBO: + solver = new WBO(f, configuration); + break; + case INC_WBO: + solver = new IncWBO(f, configuration); + break; + case LINEAR_SU: + solver = new LinearSU(f, configuration); + break; + case LINEAR_US: + solver = new LinearUS(f, configuration); + break; + case MSU3: + solver = new MSU3(f, configuration); + break; + case WMSU3: + solver = new WMSU3(f, configuration); + break; + case OLL: + solver = new OLL(f, configuration); + break; + default: + throw new IllegalArgumentException("Unknown MaxSAT algorithm: " + algorithm); + } + pgTransformation = configuration.getCnfMethod() == FACTORY_CNF + ? null + : new PlaistedGreenbaumTransformationMaxSATSolver(f, configuration.getCnfMethod() == FULL_PG_ON_SOLVER, solver); } /** @@ -234,43 +264,6 @@ public boolean isWeighted() { algorithm == Algorithm.OLL; } - /** - * Resets the solver. - * @throws IllegalArgumentException if the algorithm was unknown - */ - public void reset() { - result = null; - selectorVariables = new TreeSet<>(); - switch (algorithm) { - case WBO: - solver = new WBO(f, configuration); - break; - case INC_WBO: - solver = new IncWBO(f, configuration); - break; - case LINEAR_SU: - solver = new LinearSU(f, configuration); - break; - case LINEAR_US: - solver = new LinearUS(f, configuration); - break; - case MSU3: - solver = new MSU3(f, configuration); - break; - case WMSU3: - solver = new WMSU3(f, configuration); - break; - case OLL: - solver = new OLL(f, configuration); - break; - default: - throw new IllegalArgumentException("Unknown MaxSAT algorithm: " + algorithm); - } - pgTransformation = configuration.getCnfMethod() == FACTORY_CNF - ? null - : new PlaistedGreenbaumTransformationMaxSATSolver(f, configuration.getCnfMethod() == FULL_PG_ON_SOLVER, solver); - } - /** * Adds a new hard formula to the solver. Hard formulas must always be true. * @param formula the formula @@ -296,6 +289,31 @@ public void addSoftFormula(final Formula formula, final int weight) { addFormulaAsCnf(selVar, weight); } + /** + * Saves the current solver state. + * @return the current solver state + */ + public MaxSATState saveState() { + return solver.saveState(); + } + + /** + * Loads a given state in the solver. + *

+ * ATTENTION: You can only load a state which was created by this instance + * of the solver before the current state. Only the sizes of the internal + * data structures are stored, meaning you can go back in time and + * restore a solver state with fewer variables and/or fewer clauses. It is + * not possible to import a solver state from another solver or another + * solving execution. + * @param state the solver state to load + * @throws IllegalArgumentException if the solver state is not valid anymore + */ + public void loadState(final MaxSATState state) { + result = null; + solver.loadState(state); + } + private void addFormulaAsCnf(final Formula formula, final int weight) { result = null; if (configuration.getCnfMethod() == FACTORY_CNF) { 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 7eba8928..2cfb4809 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 @@ -40,7 +40,7 @@ /** * Incremental WBO solver. - * @version 2.1.0 + * @version 3.0.0 * @since 1.0 */ public class IncWBO extends WBO { @@ -387,7 +387,6 @@ protected LNGResult weightSearch(final ComputationHandler } protected int incComputeCostModel(final LNGBooleanVector currentModel) { - assert currentModel.size() != 0; int currentCost = 0; for (int i = 0; i < softClauses.size(); i++) { boolean unsatisfied = true; 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 8885e775..c7a7be2c 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 @@ -41,7 +41,7 @@ /** * Linear search solver with Boolean Multilevel Optimization (BMO) - * @version 2.1.0 + * @version 3.0.0 * @since 1.0 */ public class LinearSU extends MaxSAT { 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 dd8dcf5b..ef6509fc 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 @@ -35,7 +35,7 @@ /** * Linear search solver. - * @version 2.1.0 + * @version 3.0.0 * @since 1.0 */ public class LinearUS extends MaxSAT { 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 342ed4a3..61a24fd5 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 @@ -42,7 +42,7 @@ /** * Non-incremental MSU3 solver. - * @version 2.1.0 + * @version 3.0.0 * @since 1.0 */ public class MSU3 extends MaxSAT { 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 666a3362..f68835b2 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 @@ -53,7 +53,7 @@ /** * Super class for the MaxSAT solvers. - * @version 2.0.0 + * @version 3.0.0 * @since 1.0 */ public abstract class MaxSAT { @@ -88,6 +88,10 @@ public enum ProblemType { int currentWeight; MaxSAT.Stats lastStats; + // bookkeeping of solver states + protected LNGIntVector validStates; + protected int nextStateId; + /** * Constructor. * @param f the formula factory @@ -113,6 +117,8 @@ protected MaxSAT(final FormulaFactory f, final MaxSATConfig config) { nbSatisfiable = 0; sumSizeCores = 0; orderWeights = new LNGIntVector(); + validStates = new LNGIntVector(); + nextStateId = 0; } /** @@ -156,46 +162,75 @@ public final LNGResult search(final ComputationHandler han if (!handler.shouldResume(MAX_SAT_CALL_STARTED)) { return LNGResult.aborted(MAX_SAT_CALL_STARTED); } - final StateBeforeSolving stateBeforeSolving = saveStateBeforeSolving(); + final MaxSATState stateBeforeSolving = saveState(); final LNGResult result = internalSearch(handler); if (!handler.shouldResume(MAX_SAT_CALL_FINISHED)) { return LNGResult.aborted(MAX_SAT_CALL_FINISHED); } lastStats = new Stats(); - loadStateBeforeSolving(stateBeforeSolving); + loadState(stateBeforeSolving); return result; } - protected StateBeforeSolving saveStateBeforeSolving() { + /** + * Saves and returns the solver state. + * @return the current solver state + */ + public MaxSATState saveState() { 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, hardClauses.size(), softClauses.size(), ubCost, currentWeight, softWeights); + final int stateId = nextStateId++; + validStates.push(stateId); + return new MaxSATState(stateId, nbVars, hardClauses.size(), softClauses.size(), ubCost, currentWeight, softWeights); } - protected void loadStateBeforeSolving(final StateBeforeSolving stateBeforeSolving) { - hardClauses.shrinkTo(stateBeforeSolving.nbHard); - softClauses.shrinkTo(stateBeforeSolving.nbSoft); + /** + * Loads a given state in the solver. + *

+ * ATTENTION: You can only load a state which was created by this instance + * of the solver before the current state. Only the sizes of the internal + * data structures are stored, meaning you can go back in time and + * restore a solver state with fewer variables and/or fewer clauses. It is + * not possible to import a solver state from another solver or another + * solving execution. + * @param state the solver state to load + * @throws IllegalArgumentException if the solver state is not valid anymore + */ + public void loadState(final MaxSATState state) { + int index = -1; + for (int i = validStates.size() - 1; i >= 0 && index == -1; i--) { + if (validStates.get(i) == state.stateId) { + index = i; + } + } + if (index == -1) { + throw new IllegalArgumentException("The given solver state is not valid anymore."); + } + validStates.shrinkTo(index + 1); + + hardClauses.shrinkTo(state.nbHard); + softClauses.shrinkTo(state.nbSoft); orderWeights.clear(); - for (int i = stateBeforeSolving.nbVars; i < nbVars; i++) { + for (int i = state.nbVars; i < nbVars; i++) { final Variable var = index2var.remove(i); if (var != null) { var2index.remove(var); } } - nbVars = stateBeforeSolving.nbVars; + nbVars = state.nbVars; nbCores = 0; nbSymmetryClauses = 0; sumSizeCores = 0; nbSatisfiable = 0; - ubCost = stateBeforeSolving.ubCost; + ubCost = state.ubCost; lbCost = 0; - currentWeight = stateBeforeSolving.currentWeight; + currentWeight = state.currentWeight; for (int i = 0; i < softClauses.size(); i++) { final LNGSoftClause clause = softClauses.get(i); clause.relaxationVars().clear(); - clause.setWeight(stateBeforeSolving.softWeights[i]); + clause.setWeight(state.softWeights[i]); clause.setAssumptionVar(LIT_UNDEF); } } @@ -366,8 +401,6 @@ public LNGCoreSolver newSATSolver() { * @param currentModel the model found by the solver */ public void saveModel(final LNGBooleanVector currentModel) { - assert nbInitialVariables != 0; - assert currentModel.size() != 0; model.clear(); for (int i = 0; i < nbInitialVariables; i++) { model.push(currentModel.get(i)); @@ -384,7 +417,6 @@ public void saveModel(final LNGBooleanVector currentModel) { * @return the cost of the given model */ public int computeCostModel(final LNGBooleanVector currentModel, final int weight) { - assert currentModel.size() != 0; int currentCost = 0; for (int i = 0; i < softClauses.size(); i++) { boolean unsatisfied = true; @@ -482,24 +514,6 @@ LNGEvent foundUpperBound(final int upperBound, final ComputationHandler handler) return handler.shouldResume(event) ? null : event; } - protected static class StateBeforeSolving { - protected final int nbVars; - 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 nbHard, final int nbSoft, final int ubCost, final int currentWeight, final int[] softWeights) { - this.nbVars = nbVars; - this.nbSoft = nbSoft; - this.nbHard = nbHard; - this.ubCost = ubCost; - this.currentWeight = currentWeight; - this.softWeights = softWeights; - } - } - /** * The MaxSAT solver statistics. */ diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSATConfig.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSATConfig.java index 4189dea6..706db7e7 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSATConfig.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSATConfig.java @@ -12,7 +12,7 @@ /** * The configuration object for a MaxSAT solver. - * @version 2.0.0 + * @version 3.0.0 * @since 1.0 */ public final class MaxSATConfig extends Configuration { diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSATState.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSATState.java new file mode 100644 index 00000000..167fefa5 --- /dev/null +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSATState.java @@ -0,0 +1,130 @@ +package com.booleworks.logicng.solvers.maxsat.algorithms; + +import com.booleworks.logicng.solvers.MaxSATSolver; + +import java.util.Arrays; +import java.util.Objects; + +/** + * The state of a {@link MaxSATSolver}. + * @version 3.0.0 + * @since 3.0.0 + */ +public class MaxSATState { + protected final int stateId; + protected final int nbVars; + protected final int nbHard; + protected final int nbSoft; + protected final int ubCost; + protected final int currentWeight; + protected final int[] softWeights; + + /** + * Creates a new MaxSAT state with the given parameters. + * @param stateId the ID of the state in the solver + * @param nbVars the number of variables + * @param nbHard the number of hard clauses + * @param nbSoft the number of soft clauses + * @param ubCost the ub cost + * @param currentWeight the current weight + * @param softWeights the weights in each soft clause, + * must have length {@code nbSoft} + */ + public MaxSATState(final int stateId, final int nbVars, final int nbHard, final int nbSoft, final int ubCost, final int currentWeight, final int[] softWeights) { + this.stateId = stateId; + this.nbVars = nbVars; + this.nbHard = nbHard; + this.nbSoft = nbSoft; + this.ubCost = ubCost; + this.currentWeight = currentWeight; + this.softWeights = softWeights; + } + + /** + * Returns the ID of the state in the solver. + * @return the ID of the state in the solver + */ + public int getStateId() { + return stateId; + } + + /** + * Returns the number of variables. + * @return the number of variables + */ + public int getNbVars() { + return nbVars; + } + + /** + * Returns the number of hard clauses. + * @return the number of hard clauses + */ + public int getNbHard() { + return nbHard; + } + + /** + * Returns the number of soft clauses. + * @return the number of soft clauses + */ + public int getNbSoft() { + return nbSoft; + } + + /** + * Returns the ub cost. + * @return the ub cost + */ + public int getUbCost() { + return ubCost; + } + + /** + * Returns the current weight. + * @return the current weight + */ + public int getCurrentWeight() { + return currentWeight; + } + + /** + * Returns the weights in each soft clause, must have length {@code nbSoft}. + * @return the weights in each soft clause + */ + public int[] getSoftWeights() { + return softWeights; + } + + @Override + public boolean equals(final Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + final MaxSATState that = (MaxSATState) o; + return stateId == that.stateId && nbVars == that.nbVars && nbHard == that.nbHard && nbSoft == that.nbSoft + && ubCost == that.ubCost && currentWeight == that.currentWeight + && Objects.deepEquals(softWeights, that.softWeights); + } + + @Override + public int hashCode() { + return Objects.hash(stateId, nbVars, nbHard, nbSoft, ubCost, currentWeight, Arrays.hashCode(softWeights)); + } + + @Override + public String toString() { + return "MaxSATState{" + + "stateId=" + stateId + + ", nbVars=" + nbVars + + ", nbHard=" + nbHard + + ", nbSoft=" + nbSoft + + ", ubCost=" + ubCost + + ", currentWeight=" + currentWeight + + ", softWeights=" + Arrays.toString(softWeights) + + '}'; + } +} 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 3f0fff0b..a22cc3a9 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 @@ -24,7 +24,7 @@ *

* Based on "Unsatisfiability-based optimization in clasp*" by Andres, Kaufmann, * Matheis, and Schaub. - * @version 2.4.0 + * @version 3.0.0 * @since 2.4.0 */ public class OLL extends MaxSAT { 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 c4937b1d..bc48b699 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 @@ -45,7 +45,7 @@ /** * Weighted Boolean Optimization solver. - * @version 2.1.0 + * @version 3.0.0 * @since 1.0 */ public class WBO extends MaxSAT { 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 4628673e..73023aac 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 @@ -39,7 +39,7 @@ /** * The weighted MSU3 algorithm. - * @version 2.1.0 + * @version 3.0.0 * @since 1.0 */ public class WMSU3 extends MaxSAT { diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/encodings/ModularTotalizer.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/encodings/ModularTotalizer.java index 6db4013d..e6c07162 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/encodings/ModularTotalizer.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/encodings/ModularTotalizer.java @@ -79,7 +79,6 @@ boolean hasCreatedEncoding() { * @param rhs the right-hand side of the constraint */ public void encode(final LNGCoreSolver s, final LNGIntVector lits, final int rhs) { - assert lits.size() > 0; hasEncoding = false; cardinalityUpoutlits.clear(); cardinalityLwoutlits.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 d6b7a13f..00c3381b 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java @@ -578,8 +578,7 @@ public LNGIntVector assumptionsConflict() { } /** - * Saves and returns the solver state expressed as an integer array which - * stores the length of the internal data structures. + * Saves and returns the solver state. * @return the current solver state */ public SolverState saveState() { diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSATDecrementalTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSATDecrementalTest.java new file mode 100644 index 00000000..4b0eaf2b --- /dev/null +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSATDecrementalTest.java @@ -0,0 +1,152 @@ +package com.booleworks.logicng.solvers.maxsat; + +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; + +import com.booleworks.logicng.TestWithExampleFormulas; +import com.booleworks.logicng.io.parsers.ParserException; +import com.booleworks.logicng.solvers.MaxSATSolver; +import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig; +import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig.CardinalityEncoding; +import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig.IncrementalStrategy; +import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig.WeightStrategy; +import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATState; +import org.junit.jupiter.api.Test; + +public class MaxSATDecrementalTest extends TestWithExampleFormulas { + + @Test + public void testDecrementalityPartial() throws ParserException { + final MaxSATSolver[] solvers = new MaxSATSolver[]{ + MaxSATSolver.wbo(f), + MaxSATSolver.incWBO(f), + MaxSATSolver.oll(f), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.TOTALIZER).bmo(false).build()), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.MTOTALIZER).bmo(false).build()), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.TOTALIZER).bmo(true).build()), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.MTOTALIZER).bmo(true).build()), + MaxSATSolver.linearUS(f, MaxSATConfig.builder().incremental(IncrementalStrategy.NONE).cardinality(CardinalityEncoding.TOTALIZER).build()), + MaxSATSolver.linearUS(f, MaxSATConfig.builder().incremental(IncrementalStrategy.NONE).cardinality(CardinalityEncoding.MTOTALIZER).build()), + MaxSATSolver.linearUS(f, MaxSATConfig.builder().incremental(IncrementalStrategy.ITERATIVE).cardinality(CardinalityEncoding.TOTALIZER).build()), + MaxSATSolver.msu3(f, MaxSATConfig.builder().incremental(IncrementalStrategy.NONE).cardinality(CardinalityEncoding.TOTALIZER).build()), + MaxSATSolver.msu3(f, MaxSATConfig.builder().incremental(IncrementalStrategy.NONE).cardinality(CardinalityEncoding.MTOTALIZER).build()), + MaxSATSolver.msu3(f, MaxSATConfig.builder().incremental(IncrementalStrategy.ITERATIVE).cardinality(CardinalityEncoding.TOTALIZER).build()) + }; + for (final MaxSATSolver solver : solvers) { + assertThat(solver.solve().getOptimum()).isEqualTo(0); + final MaxSATState state0 = solver.saveState(); + assertThat(state0).isEqualTo(new MaxSATState(1, 0, 0, 0, 0, 1, new int[0])); + + solver.addHardFormula(f.parse("(~a | ~b) & (~b | ~c) & ~d")); + assertThat(solver.solve().getOptimum()).isEqualTo(0); + final MaxSATState state1 = solver.saveState(); + assertThat(state1).isEqualTo(new MaxSATState(3, 4, 3, 0, 0, 1, new int[0])); + + solver.addSoftFormula(A, 1); + solver.addSoftFormula(B, 1); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + final MaxSATState state2 = solver.saveState(); + assertThat(state2).isEqualTo(new MaxSATState(5, 6, 7, 2, 2, 1, new int[]{1, 1})); + + solver.loadState(state1); + assertThat(solver.solve().getOptimum()).isEqualTo(0); + + solver.addSoftFormula(A, 1); + solver.addSoftFormula(B, 1); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + final MaxSATState state3 = solver.saveState(); + solver.addSoftFormula(C, 1); + solver.addSoftFormula(D, 1); + //assertThat(solver.solve().getOptimum()).isEqualTo(2); + final MaxSATState state4 = solver.saveState(); + solver.addSoftFormula(NA, 1); + assertThat(solver.solve().getOptimum()).isEqualTo(3); + + solver.loadState(state4); + assertThat(solver.solve().getOptimum()).isEqualTo(2); + + solver.loadState(state3); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + + assertThatThrownBy(() -> solver.loadState(state2)).isInstanceOf(IllegalArgumentException.class) + .hasMessage("The given solver state is not valid anymore."); + + solver.loadState(state0); + assertThat(solver.solve().getOptimum()).isEqualTo(0); + + solver.addSoftFormula(A, 1); + solver.addSoftFormula(B, 1); + solver.addSoftFormula(NB, 1); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + } + } + + @Test + public void testDecrementalityWeighted() throws ParserException { + final MaxSATSolver[] solvers = new MaxSATSolver[]{ + MaxSATSolver.wbo(f, MaxSATConfig.builder().weight(WeightStrategy.NONE).build()), + MaxSATSolver.wbo(f, MaxSATConfig.builder().weight(WeightStrategy.NORMAL).build()), + MaxSATSolver.wbo(f, MaxSATConfig.builder().weight(WeightStrategy.DIVERSIFY).build()), + MaxSATSolver.incWBO(f, MaxSATConfig.builder().weight(WeightStrategy.NONE).build()), + MaxSATSolver.incWBO(f, MaxSATConfig.builder().weight(WeightStrategy.NORMAL).build()), + MaxSATSolver.incWBO(f, MaxSATConfig.builder().weight(WeightStrategy.DIVERSIFY).build()), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.TOTALIZER).bmo(false).build()), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.MTOTALIZER).bmo(false).build()), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.TOTALIZER).bmo(true).build()), + MaxSATSolver.linearSU(f, MaxSATConfig.builder().cardinality(CardinalityEncoding.MTOTALIZER).bmo(true).build()), + MaxSATSolver.wmsu3(f, MaxSATConfig.builder().incremental(IncrementalStrategy.NONE).cardinality(CardinalityEncoding.TOTALIZER).bmo(false).build()), + MaxSATSolver.wmsu3(f, MaxSATConfig.builder().incremental(IncrementalStrategy.NONE).cardinality(CardinalityEncoding.MTOTALIZER).bmo(false).build()), + MaxSATSolver.wmsu3(f, MaxSATConfig.builder().incremental(IncrementalStrategy.ITERATIVE).cardinality(CardinalityEncoding.TOTALIZER).bmo(false).build()), + MaxSATSolver.wmsu3(f, MaxSATConfig.builder().incremental(IncrementalStrategy.ITERATIVE).cardinality(CardinalityEncoding.TOTALIZER).bmo(true).build()), + MaxSATSolver.oll(f) + }; + for (final MaxSATSolver solver : solvers) { + solver.addSoftFormula(X, 2); + assertThat(solver.solve().getOptimum()).isEqualTo(0); + final MaxSATState state0 = solver.saveState(); + assertThat(state0).isEqualTo(new MaxSATState(1, 2, 2, 1, 2, 2, new int[]{2})); + + solver.addHardFormula(f.parse("(~a | ~b) & (~b | ~c) & ~d")); + assertThat(solver.solve().getOptimum()).isEqualTo(0); + final MaxSATState state1 = solver.saveState(); + assertThat(state1).isEqualTo(new MaxSATState(3, 6, 5, 1, 2, 2, new int[]{2})); + + solver.addSoftFormula(A, 1); + solver.addSoftFormula(B, 2); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + final MaxSATState state2 = solver.saveState(); + assertThat(state2).isEqualTo(new MaxSATState(5, 8, 9, 3, 5, 2, new int[]{2, 1, 2})); + + solver.loadState(state1); + assertThat(solver.solve().getOptimum()).isEqualTo(0); + + solver.addSoftFormula(A, 1); + solver.addSoftFormula(B, 2); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + final MaxSATState state3 = solver.saveState(); + solver.addSoftFormula(C, 1); + solver.addSoftFormula(D, 2); + //assertThat(solver.solve().getOptimum()).isEqualTo(4); + final MaxSATState state4 = solver.saveState(); + solver.addSoftFormula(NA, 4); + assertThat(solver.solve().getOptimum()).isEqualTo(4); + + solver.loadState(state4); + assertThat(solver.solve().getOptimum()).isEqualTo(4); + + solver.loadState(state3); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + + assertThatThrownBy(() -> solver.loadState(state2)).isInstanceOf(IllegalArgumentException.class) + .hasMessage("The given solver state is not valid anymore."); + + solver.loadState(state0); + assertThat(solver.solve().getOptimum()).isEqualTo(0); + + solver.addSoftFormula(A, 1); + solver.addSoftFormula(B, 1); + solver.addSoftFormula(NB, 1); + assertThat(solver.solve().getOptimum()).isEqualTo(1); + } + } +} diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSATIncrementalTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSATIncrementalTest.java index 0e3e362e..d8b62b50 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSATIncrementalTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSATIncrementalTest.java @@ -14,7 +14,7 @@ public class MaxSATIncrementalTest extends TestWithExampleFormulas { @Test - public void testIncrementalInterfacePartial() throws ParserException { + public void testIncrementalityPartial() throws ParserException { final MaxSATSolver[] solvers = new MaxSATSolver[]{ MaxSATSolver.wbo(f), MaxSATSolver.incWBO(f), @@ -44,7 +44,7 @@ public void testIncrementalInterfacePartial() throws ParserException { } @Test - public void testIncrementalInterfaceWeighted() throws ParserException { + public void testIncrementalityWeighted() throws ParserException { final MaxSATSolver[] solvers = new MaxSATSolver[]{ MaxSATSolver.wbo(f, MaxSATConfig.builder().weight(WeightStrategy.NONE).build()), MaxSATSolver.wbo(f, MaxSATConfig.builder().weight(WeightStrategy.NORMAL).build()), diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java index 6ad0a77a..e4845280 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java @@ -17,10 +17,12 @@ import java.io.File; import java.io.IOException; import java.nio.file.Files; +import java.util.Arrays; import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.Objects; +import java.util.function.Supplier; public class MaxSatLongRunningTest { @@ -30,15 +32,17 @@ public void testWeightedMaxSat() throws IOException { final FormulaFactory f = FormulaFactory.caching(); final File folder = new File("src/test/resources/longrunning/wms"); final Map result = readResult(new File("src/test/resources/longrunning/wms/result.txt")); - final MaxSATSolver[] solvers = new MaxSATSolver[3]; - solvers[0] = MaxSATSolver.oll(f); - solvers[1] = MaxSATSolver.incWBO(f, MaxSATConfig.builder() - .cnfMethod(SATSolverConfig.CNFMethod.FACTORY_CNF).weight(MaxSATConfig.WeightStrategy.DIVERSIFY).build()); - solvers[2] = MaxSATSolver.incWBO(f, MaxSATConfig.builder().cnfMethod(SATSolverConfig.CNFMethod.FACTORY_CNF).build()); - for (final MaxSATSolver solver : solvers) { + final List> solvers = Arrays.asList( + () -> MaxSATSolver.oll(f), + () -> MaxSATSolver.incWBO(f, MaxSATConfig.builder().cnfMethod(SATSolverConfig.CNFMethod.FACTORY_CNF) + .weight(MaxSATConfig.WeightStrategy.DIVERSIFY).build()), + () -> MaxSATSolver.incWBO(f, MaxSATConfig.builder().cnfMethod(SATSolverConfig.CNFMethod.FACTORY_CNF) + .build()) + ); + for (final Supplier solverGenerator : solvers) { for (final File file : Objects.requireNonNull(folder.listFiles())) { if (file.getName().endsWith("wcnf")) { - solver.reset(); + final MaxSATSolver solver = solverGenerator.get(); readCnfToSolver(solver, file.getAbsolutePath()); assertThat(solver.solve().getOptimum()).isEqualTo(result.get(file.getName())); } diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java index 3500b925..06af0b4a 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java @@ -28,6 +28,7 @@ import java.io.FileNotFoundException; import java.io.IOException; import java.io.PrintStream; +import java.util.function.Supplier; public class PartialMaxSATTest extends TestWithExampleFormulas { @@ -188,8 +189,7 @@ public void testTimeoutHandlerWBO() { final MaxSATConfig[] configs = new MaxSATConfig[1]; configs[0] = MaxSATConfig.builder().verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -198,8 +198,7 @@ public void testTimeoutHandlerIncWBO() { final MaxSATConfig[] configs = new MaxSATConfig[1]; configs[0] = MaxSATConfig.builder().verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -216,8 +215,7 @@ public void testTimeoutHandlerLinearSU() { configs[3] = MaxSATConfig.builder().cardinality(MaxSATConfig.CardinalityEncoding.MTOTALIZER).bmo(true) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -235,8 +233,7 @@ public void testTimeoutHandlerLinearUS() { .cardinality(MaxSATConfig.CardinalityEncoding.TOTALIZER).verbosity(MaxSATConfig.Verbosity.SOME) .output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -254,23 +251,23 @@ public void testTimeoutHandlerMSU3() { .cardinality(MaxSATConfig.CardinalityEncoding.TOTALIZER).verbosity(MaxSATConfig.Verbosity.SOME) .output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } - private void testTimeoutHandler(final MaxSATSolver solver) { + private void testTimeoutHandler(final Supplier solverGenerator) { final TimeoutHandler handler = new TimeoutHandler(1000L); final PigeonHoleGenerator pg = new PigeonHoleGenerator(f); final Formula formula = pg.generate(10); + MaxSATSolver solver = solverGenerator.get(); solver.addHardFormula(formula); solver.addSoftFormula(f.or(formula.variables(f)), 1); LNGResult result = solver.solve(handler); assertThat(result.isSuccess()).isFalse(); final TimeoutHandler handler2 = new TimeoutHandler(1000L); - solver.reset(); + solver = solverGenerator.get(); solver.addHardFormula(IMP1); solver.addSoftFormula(AND1, 1); result = solver.solve(handler2); diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java index 50191307..e4a50125 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java @@ -24,6 +24,7 @@ import java.io.FileNotFoundException; import java.io.IOException; import java.io.PrintStream; +import java.util.function.Supplier; public class PartialWeightedMaxSATTest extends TestWithExampleFormulas { @@ -257,8 +258,7 @@ public void testTimeoutHandlerWBO() { configs[2] = MaxSATConfig.builder().weight(MaxSATConfig.WeightStrategy.DIVERSIFY) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -273,8 +273,7 @@ public void testTimeoutHandlerIncWBO() { configs[2] = MaxSATConfig.builder().weight(MaxSATConfig.WeightStrategy.DIVERSIFY) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -286,8 +285,7 @@ public void testTimeoutHandlerLinearSU() { configs[1] = MaxSATConfig.builder().cardinality(MaxSATConfig.CardinalityEncoding.MTOTALIZER).bmo(false) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -305,8 +303,7 @@ public void testTimeoutHandlerWMSU3() { .cardinality(MaxSATConfig.CardinalityEncoding.TOTALIZER).bmo(false) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -318,8 +315,7 @@ public void testTimeoutHandlerWMSU3BMO() { .cardinality(MaxSATConfig.CardinalityEncoding.TOTALIZER).bmo(true) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -331,8 +327,7 @@ public void testTimeoutHandlerLinearSUBMO() { configs[1] = MaxSATConfig.builder().cardinality(MaxSATConfig.CardinalityEncoding.MTOTALIZER).bmo(true) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); for (final MaxSATConfig config : configs) { - final MaxSATSolver solver = MaxSATSolver.wbo(f, config); - testTimeoutHandler(solver); + testTimeoutHandler(() -> MaxSATSolver.wbo(f, config)); } } @@ -396,17 +391,18 @@ public void testWeightedSoftConstraintsCornerCaseFalsum() throws ParserException } } - private void testTimeoutHandler(final MaxSATSolver solver) { + private void testTimeoutHandler(final Supplier solverGenerator) { final TimeoutHandler handler = new TimeoutHandler(1000L); final PigeonHoleGenerator pg = new PigeonHoleGenerator(f); final Formula formula = pg.generate(10); + MaxSATSolver solver = solverGenerator.get(); solver.addHardFormula(formula); solver.addSoftFormula(f.or(formula.variables(f)), 10); LNGResult result = solver.solve(handler); assertThat(result.isSuccess()).isFalse(); final TimeoutHandler handler2 = new TimeoutHandler(1000L); - solver.reset(); + solver = solverGenerator.get(); solver.addHardFormula(IMP1); solver.addSoftFormula(AND1, 10); result = solver.solve(handler2);