From b783c194805ea74420c6df6c03c1f04ab462a909 Mon Sep 17 00:00:00 2001
From: Rouven Walter <rouven.walter@booleworks.com>
Date: Fri, 2 Aug 2024 21:04:38 +0200
Subject: [PATCH] bugfix: added backbone literals to intermediate result in
 AdvancedSimplifier

---
 .../simplification/AdvancedSimplifier.java         | 11 +++++++----
 .../simplification/AdvancedSimplifierTest.java     | 14 ++++++++++++++
 2 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
index 594e2e70..c5fe33a3 100644
--- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
+++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
@@ -142,16 +142,14 @@ 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);
@@ -159,6 +157,11 @@ public Formula apply(final Formula formula, final boolean cache) {
         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
index ec902ca3..64a87dee 100644
--- 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)))