add decrementality with saveState and loadState to MaxSATSolver, remo…

…ve MaxSATSolver.reset

src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java

@@ -24,6 +24,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;
@@ -55,11 +56,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<Variable> selectorVariables;
     protected LNGResult<MaxSATResult> result;
-    protected MaxSAT solver;
-    protected SortedSet<Variable> selectorVariables;
 
     /**
      * Constructs a new MaxSAT solver with a given configuration.
@@ -72,7 +73,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);
     }
 
     /**
@@ -237,43 +267,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
@@ -299,6 +292,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.
+     * <p>
+     * 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) {

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<InternalMaxSATResult> 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;

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 {

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 {

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 {

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<InternalMaxSATResult> search(final ComputationHandler han
         if (!handler.shouldResume(MAX_SAT_CALL_STARTED)) {
             return LNGResult.canceled(MAX_SAT_CALL_STARTED);
         }
-        final StateBeforeSolving stateBeforeSolving = saveStateBeforeSolving();
+        final MaxSATState stateBeforeSolving = saveState();
         final LNGResult<InternalMaxSATResult> result = internalSearch(handler);
         if (!handler.shouldResume(MAX_SAT_CALL_FINISHED)) {
             return LNGResult.canceled(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.
+     * <p>
+     * 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.
      */

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 {