added minimalDnfCover config flag in AdvancedSimplifierConfig

logic-ng · Aug 2, 2024 · c03d342 · c03d342
1 parent b783c19
commit c03d342
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 11 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -2,6 +2,12 @@
 
 LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [2.6.0] - 2024-08-02
+
+### Added
+
+- Added configuration flag `minimalDnfCover` in `AdvancedSimplifierConfig` to set whether the step for computing the minimal DNF cover should be performed. Default is `true`.
+
 ## [2.5.1] - 2024-07-31
 
 ### Changed

diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
@@ -135,16 +135,18 @@ public Formula apply(final Formula formula, final boolean cache) {
                 return config.returnIntermediateResult ? formula : null;
             }
             if (!backbone.isSat()) {
-               return f.falsum();
+                return f.falsum();
             }
             backboneLiterals.addAll(backbone.getCompleteBackbone());
             simplified = formula.restrict(new Assignment(backboneLiterals));
         }
-        final Formula simplifyMinDnf = computeMinDnf(f, simplified, config);
-        if (simplifyMinDnf == null) {
-            return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null;
+        if (config.minimalDnfCover) {
+            final Formula simplifyMinDnf = computeMinDnf(f, simplified, config);
+            if (simplifyMinDnf == null) {
+                return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null;
+            }
+            simplified = simplifyWithRating(simplified, simplifyMinDnf, config);
         }
-        simplified = simplifyWithRating(simplified, simplifyMinDnf, config);
         if (config.factorOut) {
             final Formula factoredOut = simplified.transform(new FactorOutSimplifier(config.ratingFunction));
             simplified = simplifyWithRating(simplified, factoredOut, config);
@@ -164,13 +166,13 @@ private static Formula addLiterals(final Formula formula, final SortedSet<Litera
 
     private Formula computeMinDnf(final FormulaFactory f, final Formula simplified, final AdvancedSimplifierConfig config) {
         final PrimeResult primeResult =
-               PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.optimizationConfig);
+                PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.optimizationConfig);
         if (primeResult == null || config.optimizationConfig.aborted()) {
             return null;
         }
         final List<SortedSet<Literal>> primeImplicants = primeResult.getPrimeImplicants();
         final List<Formula> minimizedPIs = SmusComputation.computeSmusForFormulas(negateAllLiterals(primeImplicants, f),
-               Collections.singletonList(simplified), f, config.optimizationConfig);
+                Collections.singletonList(simplified), f, config.optimizationConfig);
         if (minimizedPIs == null || config.optimizationConfig.aborted()) {
             return null;
         }

diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
@@ -42,6 +42,7 @@
 public class AdvancedSimplifierConfig extends Configuration {
 
     boolean restrictBackbone;
+    boolean minimalDnfCover;
     boolean factorOut;
     boolean simplifyNegations;
     boolean returnIntermediateResult;
@@ -52,6 +53,7 @@ public class AdvancedSimplifierConfig extends Configuration {
     public String toString() {
         return "AdvancedSimplifierConfig{" +
                 "restrictBackbone=" + this.restrictBackbone +
+                ", minimalDnfCover=" + this.minimalDnfCover +
                 ", factorOut=" + this.factorOut +
                 ", simplifyNegations=" + this.simplifyNegations +
                 ", returnIntermediateResult=" + this.returnIntermediateResult +
@@ -67,6 +69,7 @@ public String toString() {
     private AdvancedSimplifierConfig(final Builder builder) {
         super(ConfigurationType.ADVANCED_SIMPLIFIER);
         this.restrictBackbone = builder.restrictBackbone;
+        this.minimalDnfCover = builder.minimalDnfCover;
         this.factorOut = builder.factorOut;
         this.simplifyNegations = builder.simplifyNegations;
         this.returnIntermediateResult = builder.returnIntermediateResult;
@@ -88,6 +91,7 @@ public static Builder builder() {
     public static class Builder {
 
         boolean restrictBackbone = true;
+        boolean minimalDnfCover = true;
         boolean factorOut = true;
         boolean simplifyNegations = true;
         boolean returnIntermediateResult = false;
@@ -109,6 +113,17 @@ public Builder restrictBackbone(final boolean restrictBackbone) {
             return this;
         }
 
+        /**
+         * Sets the flag for whether a minimal DNF cover should be computed. The
+         * default is 'true'.
+         * @param minimalDnfCover flag for the minimal DNF cover computation
+         * @return the current builder
+         */
+        public Builder minimalDnfCover(final boolean minimalDnfCover) {
+            this.minimalDnfCover = minimalDnfCover;
+            return this;
+        }
+
         /**
          * Sets the flag for whether the formula should be factorized. The
          * default is 'true'.

diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java
@@ -191,11 +191,13 @@ public void testAdvancedSimplifierConfig() {
         final FormulaFactory f = new FormulaFactory();
         final List<AdvancedSimplifierConfig> configs = Arrays.asList(
                 AdvancedSimplifierConfig.builder().build(),
-                AdvancedSimplifierConfig.builder().restrictBackbone(false).factorOut(false).simplifyNegations(false).build(),
+                AdvancedSimplifierConfig.builder().restrictBackbone(false).minimalDnfCover(false).factorOut(false).simplifyNegations(false).build(),
                 AdvancedSimplifierConfig.builder().factorOut(false).simplifyNegations(false).build(),
                 AdvancedSimplifierConfig.builder().restrictBackbone(false).simplifyNegations(false).build(),
+                AdvancedSimplifierConfig.builder().restrictBackbone(false).minimalDnfCover(false).build(),
                 AdvancedSimplifierConfig.builder().restrictBackbone(false).factorOut(false).build(),
                 AdvancedSimplifierConfig.builder().restrictBackbone(false).build(),
+                AdvancedSimplifierConfig.builder().minimalDnfCover(false).build(),
                 AdvancedSimplifierConfig.builder().factorOut(false).build(),
                 AdvancedSimplifierConfig.builder().simplifyNegations(false).build());
 
@@ -216,11 +218,11 @@ public void testAdvancedSimplifierConfig() {
     @Test
     public void testBackboneIntermediateResult() {
         final FormulaFactory f = new FormulaFactory();
-        Formula formula = parse(f, "(a & b) | (a & c)");
-        OptimizationHandler optHandler = mock(OptimizationHandler.class);
+        final Formula formula = parse(f, "(a & b) | (a & c)");
+        final OptimizationHandler optHandler = mock(OptimizationHandler.class);
         // abort simplification after successful backbone computation
         final AtomicInteger count = new AtomicInteger(0);
-        when(optHandler.aborted()).then(invocationOnMock ->  count.addAndGet(1) > 1);
+        when(optHandler.aborted()).then(invocationOnMock -> count.addAndGet(1) > 1);
         testHandler(optHandler, formula, true, true);
     }