Optimization config in prime compiler

pom.xml

@@ -26,7 +26,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.5.1</version>
+  <version>2.6.0-SNAPSHOT</version>
   <packaging>bundle</packaging>
 
   <name>LogicNG</name>

src/main/java/org/logicng/explanations/smus/SmusComputation.java

@@ -137,7 +137,7 @@ public static <P extends Proposition> List<P> computeSmus(
             final FormulaFactory f,
             final OptimizationConfig config) {
         if (config.getOptimizationType() == SAT_OPTIMIZATION) {
-            return computeSmusSat(propositions, additionalConstraints, f, config.getOptimizationHandler());
+            return computeSmusSAT(propositions, additionalConstraints, f, config.getOptimizationHandler());
         } else {
             return computeSmusMaxSAT(propositions, additionalConstraints, f, config);
         }
@@ -193,7 +193,7 @@ public static List<Formula> computeSmusForFormulas(
         return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList());
     }
 
-    private static <P extends Proposition> List<P> computeSmusSat(
+    private static <P extends Proposition> List<P> computeSmusSAT(
             final List<P> propositions,
             final List<Formula> additionalConstraints,
             final FormulaFactory f,
@@ -283,9 +283,6 @@ private static SortedSet<Variable> minimumHs(
             final Set<Variable> variables,
             final OptimizationConfig config,
             final FormulaFactory f) {
-        if (variables.isEmpty()) {
-            return new TreeSet<>(); // TODO workaround: MaxSAT assertion fails for corner case
-        }
         final MaxSATSolver maxSatSolver = config.genMaxSATSolver(f);
         constraints.forEach(maxSatSolver::addHardFormula);
         for (final Variable v : variables) {

src/main/java/org/logicng/primecomputation/PrimeCompiler.java

@@ -39,12 +39,14 @@
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 import org.logicng.handlers.OptimizationHandler;
+import org.logicng.handlers.SATHandler;
+import org.logicng.solvers.MaxSATSolver;
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
 import org.logicng.solvers.functions.OptimizationFunction;
 import org.logicng.solvers.maxsat.OptimizationConfig;
 import org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType;
-import org.logicng.solvers.sat.MiniSatConfig;
+import org.logicng.solvers.maxsat.algorithms.MaxSAT;
 import org.logicng.transformations.LiteralSubstitution;
 import org.logicng.util.FormulaHelper;
 import org.logicng.util.Pair;
@@ -71,24 +73,20 @@
  * {@link #getWithMaximization()} and another which searches for minimum models
  * {@link #getWithMaximization()}. From experience, the one with minimum models usually
  * outperforms the one with maximum models.
- * @version 2.1.0
+ * @version 2.6.0
  * @since 2.0.0
  */
 public final class PrimeCompiler {
 
     private static final String POS = "_POS";
     private static final String NEG = "_NEG";
-    private static final OptimizationConfig DEFAULT_CFG =
-            new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, null, null);
-    private static final PrimeCompiler INSTANCE_MIN = new PrimeCompiler(false, DEFAULT_CFG);
-    private static final PrimeCompiler INSTANCE_MAX = new PrimeCompiler(true, DEFAULT_CFG);
+    private static final PrimeCompiler INSTANCE_MIN = new PrimeCompiler(false);
+    private static final PrimeCompiler INSTANCE_MAX = new PrimeCompiler(true);
 
     private final boolean computeWithMaximization;
-    private final OptimizationConfig config;
 
-    private PrimeCompiler(final boolean computeWithMaximization, final OptimizationConfig config) {
+    private PrimeCompiler(final boolean computeWithMaximization) {
         this.computeWithMaximization = computeWithMaximization;
-        this.config = config;
     }
 
     /**
@@ -108,31 +106,36 @@ public static PrimeCompiler getWithMaximization() {
     }
 
     /**
-     * Returns a compiler which uses minimum models to compute the primes.
-     * @return a compiler which uses minimum models to compute the primes
-     */
-    public static PrimeCompiler getWithMinimization(final OptimizationConfig config) {
-        return new PrimeCompiler(false, config);
-    }
-
-    /**
-     * Returns a compiler which uses maximum models to compute the primes.
-     * @return a compiler which uses maximum models to compute the primes
+     * Computes prime implicants and prime implicates for a given formula.
+     * The coverage type specifies if the implicants or the implicates will
+     * be complete, the other one will still be a cover of the given formula.
+     * @param formula the formula
+     * @param type    the coverage type
+     * @return the prime result
      */
-    public static PrimeCompiler getWithMaximization(final OptimizationConfig config) {
-        return new PrimeCompiler(false, config);
+    public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type) {
+        return compute(formula, type, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, null, null));
     }
 
     /**
      * Computes prime implicants and prime implicates for a given formula.
      * The coverage type specifies if the implicants or the implicates will
      * be complete, the other one will still be a cover of the given formula.
+     * <p>
+     * The prime compiler can be called with an {@link OptimizationHandler}.
+     * The given handler instance will be used for every subsequent
+     * {@link org.logicng.solvers.functions.OptimizationFunction} call and
+     * the handler's SAT handler is used for every subsequent SAT call.
      * @param formula the formula
      * @param type    the coverage type
-     * @return the prime result
+     * @param handler an optimization handler, can be {@code null}
+     * @return the prime result or null if the computation was aborted by the handler
      */
-    public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type) {
-        return compute(formula, type, null);
+    public PrimeResult compute(
+            final Formula formula,
+            final PrimeResult.CoverageType type,
+            final OptimizationHandler handler) {
+        return compute(formula, type, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, handler, null));
     }
 
     /**
@@ -146,15 +149,23 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType
      * the handler's SAT handler is used for every subsequent SAT call.
      * @param formula the formula
      * @param type    the coverage type
-     * @param handler an optimization handler, can be {@code null}
+     * @param cfg     the optimization configuration
      * @return the prime result or null if the computation was aborted by the handler
      */
-    public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type, final OptimizationHandler handler) {
-        start(handler);
+    public PrimeResult compute(
+            final Formula formula,
+            final PrimeResult.CoverageType type,
+            final OptimizationConfig cfg) {
+
         final boolean completeImplicants = type == PrimeResult.CoverageType.IMPLICANTS_COMPLETE;
         final Formula formulaForComputation = completeImplicants ? formula : formula.negate();
-        final Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> result = computeGeneric(formulaForComputation, handler);
-        if (result == null || aborted(handler)) {
+        final Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> result;
+        if (cfg.getOptimizationType() == OptimizationType.SAT_OPTIMIZATION) {
+            result = computeSAT(formulaForComputation, cfg.getOptimizationHandler());
+        } else {
+            result = computeMaxSAT(formulaForComputation, cfg);
+        }
+        if (result == null) {
             return null;
         }
         return new PrimeResult(
@@ -163,12 +174,15 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType
                 type);
     }
 
-    private Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> computeGeneric(final Formula formula, final OptimizationHandler handler) {
+    private Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> computeSAT(
+            final Formula formula,
+            final OptimizationHandler handler) {
+        start(handler);
         final FormulaFactory f = formula.factory();
         final SubstitutionResult sub = createSubstitution(formula);
-        final SATSolver hSolver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
+        final SATSolver hSolver = MiniSat.miniSat(f);
         hSolver.add(sub.constraintFormula);
-        final SATSolver fSolver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
+        final SATSolver fSolver = MiniSat.miniSat(f);
         fSolver.add(formula.negate());
         final NaivePrimeReduction primeReduction = new NaivePrimeReduction(formula);
         final List<SortedSet<Literal>> primeImplicants = new ArrayList<>();
@@ -216,6 +230,66 @@ private Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> computeGeneric(
         }
     }
 
+    private Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> computeMaxSAT(
+            final Formula formula,
+            final OptimizationConfig cfg) {
+        start(cfg.getMaxSATHandler());
+        final SATHandler handler = cfg.getMaxSATHandler() == null ? null : cfg.getMaxSATHandler().satHandler();
+        final FormulaFactory f = formula.factory();
+        final SubstitutionResult sub = createSubstitution(formula);
+        final List<Formula> hSolverConstraints = new ArrayList<>();
+        hSolverConstraints.add(sub.constraintFormula);
+        final SATSolver fSolver = MiniSat.miniSat(f);
+        fSolver.add(formula.negate());
+        final NaivePrimeReduction primeReduction = new NaivePrimeReduction(formula);
+        final List<SortedSet<Literal>> primeImplicants = new ArrayList<>();
+        final List<SortedSet<Literal>> primeImplicates = new ArrayList<>();
+        while (true) {
+            final MaxSATSolver hSolver = cfg.genMaxSATSolver(f);
+            hSolverConstraints.forEach(hSolver::addHardFormula);
+            sub.newVar2oldLit.keySet().forEach(it ->
+                    hSolver.addSoftFormula(f.literal(it.name(), this.computeWithMaximization), 1));
+            final MaxSAT.MaxSATResult result = hSolver.solve(cfg.getMaxSATHandler());
+            if (result == MaxSAT.MaxSATResult.UNDEF) {
+                return null;
+            }
+            final Assignment hModel = hSolver.model();
+            if (hModel == null) {
+                return new Pair<>(primeImplicants, primeImplicates);
+            }
+            final Assignment fModel = transformModel(hModel, sub.newVar2oldLit);
+            final Tristate fSat = fSolver.sat(handler, fModel.literals());
+            if (aborted(handler)) {
+                return null;
+            }
+            if (fSat == Tristate.FALSE) {
+                final SortedSet<Literal> primeImplicant = this.computeWithMaximization
+                        ? primeReduction.reduceImplicant(fModel.literals(), handler)
+                        : fModel.literals();
+                if (primeImplicant == null || aborted(handler)) {
+                    return null;
+                }
+                primeImplicants.add(primeImplicant);
+                final List<Literal> blockingClause = new ArrayList<>();
+                for (final Literal lit : primeImplicant) {
+                    blockingClause.add(((Literal) lit.transform(sub.substitution)).negate());
+                }
+                hSolverConstraints.add(f.or(blockingClause));
+            } else {
+                final SortedSet<Literal> implicate = new TreeSet<>();
+                for (final Literal lit : (this.computeWithMaximization ? fModel : fSolver.model(formula.variables())).literals()) {
+                    implicate.add(lit.negate());
+                }
+                final SortedSet<Literal> primeImplicate = primeReduction.reduceImplicate(implicate, handler);
+                if (primeImplicate == null || aborted(handler)) {
+                    return null;
+                }
+                primeImplicates.add(primeImplicate);
+                hSolverConstraints.add(f.or(primeImplicate).transform(sub.substitution));
+            }
+        }
+    }
+
     private SubstitutionResult createSubstitution(final Formula formula) {
         final Map<Variable, Literal> newVar2oldLit = new HashMap<>();
         final LiteralSubstitution substitution = new LiteralSubstitution();

src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java

@@ -404,7 +404,6 @@ protected MaxSATResult weightSearch() {
     }
 
     protected int incComputeCostModel(final LNGBooleanVector currentModel) {
-        assert currentModel.size() != 0;
         int currentCost = 0;
         for (int i = 0; i < nSoft(); i++) {
             boolean unsatisfied = true;
@@ -413,7 +412,6 @@ protected int incComputeCostModel(final LNGBooleanVector currentModel) {
                     unsatisfied = false;
                     continue;
                 }
-                assert var(this.softClauses.get(i).clause().get(j)) < currentModel.size();
                 if ((sign(this.softClauses.get(i).clause().get(j)) && !currentModel.get(var(this.softClauses.get(i).clause().get(j)))) ||
                         (!sign(this.softClauses.get(i).clause().get(j)) && currentModel.get(var(this.softClauses.get(i).clause().get(j))))) {
                     unsatisfied = false;

src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java

@@ -329,8 +329,6 @@ public MiniSatStyleSolver newSATSolver() {
      * @param currentModel the model found by the solver
      */
     public void saveModel(final LNGBooleanVector currentModel) {
-        assert this.nbInitialVariables != 0;
-        assert currentModel.size() != 0;
         this.model.clear();
         for (int i = 0; i < this.nbInitialVariables; i++) {
             this.model.push(currentModel.get(i));
@@ -346,7 +344,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 < nSoft(); i++) {
             boolean unsatisfied = true;
@@ -355,7 +352,6 @@ public int computeCostModel(final LNGBooleanVector currentModel, final int weigh
                     unsatisfied = false;
                     continue;
                 }
-                assert var(this.softClauses.get(i).clause().get(j)) < currentModel.size();
                 if ((sign(this.softClauses.get(i).clause().get(j)) && !currentModel.get(var(this.softClauses.get(i).clause().get(j))))
                         || (!sign(this.softClauses.get(i).clause().get(j)) && currentModel.get(var(this.softClauses.get(i).clause().get(j))))) {
                     unsatisfied = false;

src/test/java/org/logicng/explanations/smus/SmusComputationTest.java

@@ -78,7 +78,6 @@ public static Collection<Object[]> configs() {
         return configs;
     }
 
-
     @ParameterizedTest
     @MethodSource("configs")
     public void testFromPaper(final OptimizationConfig cfg) {