plain inserstion based MUS algorithm

src/main/java/org/logicng/explanations/unsatcores/MUSConfig.java

@@ -42,7 +42,7 @@ public final class MUSConfig extends Configuration {
    * The algorithm for the MUS generation.
    */
   public enum Algorithm {
-    DELETION
+    DELETION, PLAIN_INSERTION
   }
 
   final Algorithm algorithm;

src/main/java/org/logicng/explanations/unsatcores/MUSGeneration.java

@@ -29,6 +29,7 @@
 package org.logicng.explanations.unsatcores;
 
 import org.logicng.explanations.unsatcores.algorithms.DeletionBasedMUS;
+import org.logicng.explanations.unsatcores.algorithms.PlainInsertionBasedMUS;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.propositions.Proposition;
 
@@ -42,12 +43,14 @@
 public final class MUSGeneration {
 
   private final DeletionBasedMUS deletion;
+  private final PlainInsertionBasedMUS insertion;
 
   /**
    * Constructs a new MUS generator.
    */
   public MUSGeneration() {
     this.deletion = new DeletionBasedMUS();
+    this.insertion = new PlainInsertionBasedMUS();
   }
 
   /**
@@ -71,6 +74,8 @@ public UNSATCore computeMUS(final List<Proposition> propositions, final FormulaF
     if (propositions.isEmpty())
       throw new IllegalArgumentException("Cannot generate a MUS for an empty list of propositions");
     switch (config.algorithm) {
+      case PLAIN_INSERTION:
+        return insertion.computeMUS(propositions, f, config);
       case DELETION:
       default:
         return deletion.computeMUS(propositions, f, config);

src/main/java/org/logicng/explanations/unsatcores/algorithms/PlainInsertionBasedMUS.java

@@ -0,0 +1,78 @@
+///////////////////////////////////////////////////////////////////////////
+//                   __                _      _   ________               //
+//                  / /   ____  ____ _(_)____/ | / / ____/               //
+//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
+//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
+//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
+//                           /____/                                      //
+//                                                                       //
+//               The Next Generation Logic Library                       //
+//                                                                       //
+///////////////////////////////////////////////////////////////////////////
+//                                                                       //
+//  Copyright 2015-2016 Christoph Zengler                                //
+//                                                                       //
+//  Licensed under the Apache License, Version 2.0 (the "License");      //
+//  you may not use this file except in compliance with the License.     //
+//  You may obtain a copy of the License at                              //
+//                                                                       //
+//  http://www.apache.org/licenses/LICENSE-2.0                           //
+//                                                                       //
+//  Unless required by applicable law or agreed to in writing, software  //
+//  distributed under the License is distributed on an "AS IS" BASIS,    //
+//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or      //
+//  implied.  See the License for the specific language governing        //
+//  permissions and limitations under the License.                       //
+//                                                                       //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.explanations.unsatcores.algorithms;
+
+import org.logicng.datastructures.Tristate;
+import org.logicng.explanations.unsatcores.MUSConfig;
+import org.logicng.explanations.unsatcores.UNSATCore;
+import org.logicng.formulas.FormulaFactory;
+import org.logicng.propositions.Proposition;
+import org.logicng.solvers.MiniSat;
+
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * A naive plain insertion-based MUS algorithm.
+ * @version 1.1
+ * @since 1.1
+ */
+public class PlainInsertionBasedMUS extends MUSAlgorithm {
+
+  @Override
+  public UNSATCore computeMUS(List<Proposition> propositions, FormulaFactory f, MUSConfig config) {
+    List<Proposition> currentFormula = new ArrayList<>(propositions.size());
+    currentFormula.addAll(propositions);
+    final List<Proposition> mus = new ArrayList<>(propositions.size());
+    final MiniSat solver = MiniSat.miniSat(f);
+    while (!currentFormula.isEmpty()) {
+      final List<Proposition> currentSubset = new ArrayList<>(propositions.size());
+      Proposition transitionProposition = null;
+      solver.reset();
+      for (final Proposition p : mus)
+        solver.add(p);
+      int count = currentFormula.size();
+      while (solver.sat() == Tristate.TRUE) {
+        if (count < 0)
+          throw new IllegalArgumentException("Cannot compute a MUS for a satisfiable formula set.");
+        final Proposition removeProposition = currentFormula.get(--count);
+        currentSubset.add(removeProposition);
+        transitionProposition = removeProposition;
+        solver.add(removeProposition);
+      }
+      currentFormula.clear();
+      currentFormula.addAll(currentSubset);
+      if (transitionProposition != null) {
+        currentFormula.remove(transitionProposition);
+        mus.add(transitionProposition);
+      }
+    }
+    return new UNSATCore(mus, true);
+  }
+}

src/test/java/org/logicng/explanations/unsatcores/MUSGenerationTest.java

@@ -80,7 +80,6 @@ public MUSGenerationTest() throws IOException {
   @Test
   public void testDeletionBasedMUS() throws IOException {
     final MUSGeneration mus = new MUSGeneration();
-    final long start = System.currentTimeMillis();
     final UNSATCore mus1 = mus.computeMUS(this.pg3, this.f);
     final UNSATCore mus2 = mus.computeMUS(this.pg4, this.f);
     final UNSATCore mus3 = mus.computeMUS(this.pg5, this.f);
@@ -90,8 +89,6 @@ public void testDeletionBasedMUS() throws IOException {
     final UNSATCore mus7 = mus.computeMUS(this.file2, this.f);
     final UNSATCore mus8 = mus.computeMUS(this.file3, this.f);
     final UNSATCore mus9 = mus.computeMUS(this.file4, this.f);
-    final long stop = System.currentTimeMillis();
-    System.out.println("Deletion Based MUS: " + (stop - start) + " ms.");
     testMUS(pg3, mus1);
     testMUS(pg4, mus2);
     testMUS(pg5, mus3);
@@ -103,6 +100,22 @@ public void testDeletionBasedMUS() throws IOException {
     testMUS(file4, mus9);
   }
 
+  @Test
+  public void testPlainInsertionBasedMUS() throws IOException {
+    final MUSGeneration mus = new MUSGeneration();
+    final MUSConfig config = new MUSConfig.Builder().algorithm(MUSConfig.Algorithm.PLAIN_INSERTION).build();
+    final UNSATCore mus1 = mus.computeMUS(this.pg3, this.f, config);
+    final UNSATCore mus2 = mus.computeMUS(this.pg4, this.f, config);
+    final UNSATCore mus3 = mus.computeMUS(this.pg5, this.f, config);
+    final UNSATCore mus6 = mus.computeMUS(this.file1, this.f, config);
+    final UNSATCore mus7 = mus.computeMUS(this.file2, this.f, config);
+    testMUS(pg3, mus1);
+    testMUS(pg4, mus2);
+    testMUS(pg5, mus3);
+    testMUS(file1, mus6);
+    testMUS(file2, mus7);
+  }
+
   private List<Proposition> generatePGPropositions(int n) {
     final List<Proposition> result = new ArrayList<>();
     final Formula pgf = pg.generate(n);