Merge pull request #55 from logic-ng/development

Development
logic-ng · Sep 10, 2024 · 47d1db3 · 47d1db3
2 parents 42ece18 + 6fb3568
commit 47d1db3
Show file tree

Hide file tree

Showing 14 changed files with 951 additions and 219 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -2,6 +2,20 @@
 
 LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [2.6.0] - 2024-09-10
+
+### Added
+
+- New class `OptimizationConfig` used to configure optimization computations in various algorithms. It allows to configure the following aspects:
+  - the `optimizationType` (either SAT-based optimization or a MaxSAT algorithm)
+  - the `maxSATConfig` to further configure the MaxSAT algorithm
+  - the `optimizationHandler` to use
+  - the `maxSATHandler` to use
+- Added three new configuration options to `AdvancedSimplifierConfig`:
+  - `minimalDnfCover` determines whether the step for computing the minimal DNF cover should be performed. Default is `true`.
+  - `returnIntermediateResult` allows to return an intermediate result from the `AdvancedSimplifier` if the computation was aborted by a handler. Default is `false`.
+  - `optimizationConfig` can be used to configure the algorithms in the simplifier which perform optimizations, also the `OptimizationHandler handler` moved into this config
+
 ## [2.5.1] - 2024-07-31
 
 ### Changed

diff --git a/README.md b/README.md
@@ -34,7 +34,7 @@ LogicNG is released in the Maven Central Repository. To include it just add
 <dependency>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.5.1</version>
+  <version>2.6.0</version>
 </dependency>
 ```
 

diff --git a/pom.xml b/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</version>
   <packaging>bundle</packaging>
 
   <name>LogicNG</name>

diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java
diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java
@@ -39,10 +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.sat.MiniSatConfig;
+import org.logicng.solvers.maxsat.OptimizationConfig;
+import org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType;
+import org.logicng.solvers.maxsat.algorithms.MaxSAT;
 import org.logicng.transformations.LiteralSubstitution;
 import org.logicng.util.FormulaHelper;
 import org.logicng.util.Pair;
@@ -69,7 +73,7 @@
  * {@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 {
@@ -110,7 +114,7 @@ public static PrimeCompiler getWithMaximization() {
      * @return the prime result
      */
     public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type) {
-        return compute(formula, type, null);
+        return compute(formula, type, OptimizationConfig.sat(null));
     }
 
     /**
@@ -127,12 +131,41 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType
      * @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, final OptimizationHandler handler) {
-        start(handler);
+    public PrimeResult compute(
+            final Formula formula,
+            final PrimeResult.CoverageType type,
+            final OptimizationHandler handler) {
+        return compute(formula, type, OptimizationConfig.sat(handler));
+    }
+
+    /**
+     * 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
+     * @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 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(
@@ -141,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<>();
@@ -167,7 +203,9 @@ private Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> computeGeneric(
                 return null;
             }
             if (fSat == Tristate.FALSE) {
-                final SortedSet<Literal> primeImplicant = this.computeWithMaximization ? primeReduction.reduceImplicant(fModel.literals(), satHandler(handler)) : fModel.literals();
+                final SortedSet<Literal> primeImplicant = this.computeWithMaximization
+                        ? primeReduction.reduceImplicant(fModel.literals(), satHandler(handler))
+                        : fModel.literals();
                 if (primeImplicant == null || aborted(handler)) {
                     return null;
                 }
@@ -192,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 || aborted(cfg.getMaxSATHandler())) {
+                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();