bugfix: added backbone literals to intermediate result in AdvancedSim…

…plifier
logic-ng · Aug 2, 2024 · b783c19 · b783c19
1 parent 09e61b0
commit b783c19
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 4 deletions.
diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
@@ -142,23 +142,26 @@ public Formula apply(final Formula formula, final boolean cache) {
         }
         final Formula simplifyMinDnf = computeMinDnf(f, simplified, config);
         if (simplifyMinDnf == null) {
-            return config.returnIntermediateResult ? simplified : null;
+            return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null;
         }
         simplified = simplifyWithRating(simplified, simplifyMinDnf, config);
         if (config.factorOut) {
             final Formula factoredOut = simplified.transform(new FactorOutSimplifier(config.ratingFunction));
             simplified = simplifyWithRating(simplified, factoredOut, config);
         }
-        if (config.restrictBackbone) {
-            simplified = f.and(f.and(backboneLiterals), simplified);
-        }
+        simplified = addLiterals(simplified, backboneLiterals);
         if (config.simplifyNegations) {
             final Formula negationSimplified = simplified.transform(NegationSimplifier.get());
             simplified = simplifyWithRating(simplified, negationSimplified, config);
         }
         return simplified;
     }
 
+    private static Formula addLiterals(final Formula formula, final SortedSet<Literal> literals) {
+        final FormulaFactory f = formula.factory();
+        return f.and(f.and(literals), formula);
+    }
+
     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);

diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java
@@ -35,6 +35,8 @@
 import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_MSU3;
 import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_OLL;
 import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_WBO;
+import static org.mockito.Mockito.mock;
+import static org.mockito.Mockito.when;
 
 import org.junit.jupiter.api.Test;
 import org.junit.jupiter.params.ParameterizedTest;
@@ -63,6 +65,7 @@
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.List;
+import java.util.concurrent.atomic.AtomicInteger;
 
 /**
  * Unit Tests for the class {@link AdvancedSimplifier}.
@@ -210,6 +213,17 @@ 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);
+        // abort simplification after successful backbone computation
+        final AtomicInteger count = new AtomicInteger(0);
+        when(optHandler.aborted()).then(invocationOnMock ->  count.addAndGet(1) > 1);
+        testHandler(optHandler, formula, true, true);
+    }
+
     private void computeAndVerify(final Formula formula, final AdvancedSimplifier simplifier) {
         final Formula simplified = formula.transform(simplifier);
         assertThat(formula.factory().equivalence(formula, simplified).holds(new TautologyPredicate(this.f)))