fixed SATSolver#add: Ensure all variables are added to the internal s…

…olver

CHANGELOG.md

@@ -2,6 +2,12 @@
 
 LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [2.4.2] - 2023-xx-xx
+
+### Fixed
+
+- Fixed edge case in method `add(Formula formula, Proposition proposition)` in `MiniSat`. If a formula is added to the SAT solver, it can happen that a variable is not added to the solver because it was removed during the CNF transformation. A `model()` call or model enumeration will not produce models containing this variable since it was not added to the solver. The fix ensures that all variables of the original formula are added to the solver and thus, a found model includes the variable. 
+
 ## [2.4.1] - 2022-12-01
 
 ### Changed

pom.xml

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

src/main/java/org/logicng/solvers/MiniSat.java

@@ -67,7 +67,7 @@
 
 /**
  * Wrapper for the MiniSAT-style SAT solvers.
- * @version 2.4.0
+ * @version 2.4.2
  * @since 1.0
  */
 public class MiniSat extends SATSolver {
@@ -241,6 +241,18 @@ public void add(final Formula formula, final Proposition proposition) {
         } else {
             addFormulaAsCNF(formula, proposition);
         }
+        addAllOriginalVariables(formula);
+    }
+
+    /**
+     * Adds all variables of the given formula to the solver if not already present.
+     * This method can be used to ensure that the internal solver knows the given variables.
+     * @param originalFormula the original formula
+     */
+    private void addAllOriginalVariables(final Formula originalFormula) {
+        for (final Variable var : originalFormula.variables()) {
+            getOrAddIndex(var);
+        }
     }
 
     protected void addFormulaAsCNF(final Formula formula, final Proposition proposition) {

src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java

@@ -46,7 +46,7 @@
 
 /**
  * Unit tests for the at-least-k configs.
- * @version 2.0.0
+ * @version 2.4.2
  * @since 1.0
  */
 public class CCALKTest implements LogicNGTest {
@@ -66,7 +66,7 @@ public void testALK() {
         int counter = 0;
         for (final CCConfig config : this.configs) {
             f.putConfiguration(config);
-            testCC(10, 0, 1, f);
+            testCC(10, 0, 1024, f);
             testCC(10, 1, 1023, f);
             testCC(10, 2, 1013, f);
             testCC(10, 3, 968, f);

src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java

@@ -43,7 +43,7 @@
 
 /**
  * Unit tests for the at-most-k encoders.
- * @version 2.0.0
+ * @version 2.4.2
  * @since 1.0
  */
 public class CCAMKTest implements LogicNGTest {
@@ -73,8 +73,8 @@ public void testAMK() {
             testCC(10, 7, 968, f, false);
             testCC(10, 8, 1013, f, false);
             testCC(10, 9, 1023, f, false);
-            testCC(10, 10, 1, f, false);
-            testCC(10, 15, 1, f, false);
+            testCC(10, 10, 1024, f, false);
+            testCC(10, 15, 1024, f, false);
             assertThat(f.newCCVariable().name()).endsWith("_" + counter++);
         }
     }

src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java

@@ -1,19 +1,24 @@
 package org.logicng.solvers.functions;
 
 import static org.assertj.core.api.Assertions.assertThat;
+import static org.logicng.util.FormulaHelper.variables;
 
 import org.junit.jupiter.api.Test;
 import org.logicng.datastructures.Assignment;
+import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
+import org.logicng.formulas.FormulaFactoryConfig;
+import org.logicng.formulas.Variable;
 import org.logicng.io.parsers.ParserException;
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
+import org.logicng.solvers.sat.MiniSatConfig;
 
 import java.util.List;
 
 /**
  * Units tests for {@link ModelEnumerationFunction}.
- * @version 2.3.0
+ * @version 2.4.2
  * @since 2.3.0
  */
 public class ModelEnumerationFunctionTest {
@@ -47,4 +52,29 @@ public void testFastEvaluable() throws ParserException {
         models = solver.execute(ModelEnumerationFunction.builder().fastEvaluable(true).build());
         assertThat(models).extracting(Assignment::fastEvaluable).containsOnly(true);
     }
+
+    @Test
+    public void testVariableRemovedBySimplificationOccursInModels() throws ParserException {
+        final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().simplifyComplementaryOperands(true).build());
+        final SATSolver solver = MiniSat.miniSat(this.f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
+        final Variable a = f.variable("A");
+        final Variable b = f.variable("B");
+        final Formula formula = this.f.parse("A & B => A");
+        solver.add(formula); // during NNF conversion, used by the PG transformation, the formula simplifies to verum when added to the solver
+        final List<Assignment> models = solver.execute(ModelEnumerationFunction.builder().variables(formula.variables()).build());
+        assertThat(models).hasSize(4);
+        for (final Assignment model : models) {
+            assertThat(variables(model.literals())).containsExactlyInAnyOrder(a, b);
+        }
+    }
+
+    @Test
+    public void testUnknownVariableNotOccurringInModel() {
+        final SATSolver solver = MiniSat.miniSat(this.f);
+        final Variable a = this.f.variable("A");
+        solver.add(a);
+        final List<Assignment> models = solver.execute(ModelEnumerationFunction.builder().variables(this.f.variables("A", "X")).build());
+        assertThat(models).hasSize(1);
+        assertThat(models.get(0).literals()).containsExactly(a);
+    }
 }

src/test/java/org/logicng/solvers/sat/SATTest.java

@@ -33,6 +33,7 @@
 import static org.logicng.datastructures.Tristate.UNDEF;
 import static org.logicng.solvers.sat.MiniSatConfig.ClauseMinimization.BASIC;
 import static org.logicng.solvers.sat.MiniSatConfig.ClauseMinimization.NONE;
+import static org.logicng.util.FormulaHelper.variables;
 
 import org.junit.jupiter.api.Test;
 import org.logicng.LogicNGTest;
@@ -43,6 +44,7 @@
 import org.logicng.formulas.CType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
+import org.logicng.formulas.FormulaFactoryConfig;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 import org.logicng.handlers.ModelEnumerationHandler;
@@ -61,7 +63,6 @@
 import org.logicng.solvers.functions.ModelEnumerationFunction;
 import org.logicng.solvers.functions.UpZeroLiteralsFunction;
 import org.logicng.testutils.PigeonHoleGenerator;
-import org.logicng.util.FormulaHelper;
 
 import java.io.BufferedReader;
 import java.io.File;
@@ -81,7 +82,7 @@
 
 /**
  * Unit tests for the SAT solvers.
- * @version 1.6
+ * @version 2.4.1
  * @since 1.0
  */
 public class SATTest extends TestWithExampleFormulas implements LogicNGTest {
@@ -296,6 +297,28 @@ public void testPartialModel() {
         }
     }
 
+    @Test
+    public void testVariableRemovedBySimplificationOccursInModel() throws ParserException {
+        final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().simplifyComplementaryOperands(true).build());
+        final SATSolver solver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
+        final Variable a = f.variable("A");
+        final Variable b = f.variable("B");
+        final Formula formula = this.f.parse("A & B => A");
+        solver.add(formula); // during NNF conversion, used by the PG transformation, the formula simplifies to verum when added to the solver
+        assertThat(solver.sat()).isEqualTo(Tristate.TRUE);
+        assertThat(solver.knownVariables()).containsExactlyInAnyOrder(a, b);
+        assertThat(variables(solver.model().literals())).containsExactlyInAnyOrder(a, b);
+    }
+
+    @Test
+    public void testUnknownVariableNotOccurringInModel() {
+        final SATSolver solver = MiniSat.miniSat(this.f);
+        final Variable a = this.f.variable("A");
+        solver.add(a);
+        assertThat(solver.sat()).isEqualTo(Tristate.TRUE);
+        assertThat(solver.model(this.f.variables("A", "X")).literals()).containsExactly(a);
+    }
+
     @Test
     public void testModelEnumerationHandler() {
         for (final SATSolver s : this.solvers) {
@@ -341,7 +364,6 @@ public boolean foundModel(final Assignment assignment) {
     }
 
     @Test
-    @SuppressWarnings("deprecation")
     public void testWithRelaxation() throws ParserException {
         final PropositionalParser parser = new PropositionalParser(this.f);
         final Formula one = parser.parse("a & b & (c | ~d)");
@@ -822,7 +844,6 @@ public void testKnownVariables() throws ParserException {
     }
 
     @Test
-    @SuppressWarnings("deprecation")
     public void testAddWithoutUnknown() throws ParserException {
         final PropositionalParser parser = new PropositionalParser(this.f);
         final Formula phi = parser.parse("x1 & (~x2 | x3) & (x4 | ~x5)");
@@ -1086,7 +1107,7 @@ public void testDimacsFilesWithSelectionOrder() throws IOException {
                 if (fileName.endsWith(".cnf")) {
                     readCNF(solver, file);
                     final List<Literal> selectionOrder = new ArrayList<>();
-                    for (final Variable var : FormulaHelper.variables(solver.execute(FormulaOnSolverFunction.get()))) {
+                    for (final Variable var : variables(solver.execute(FormulaOnSolverFunction.get()))) {
                         if (selectionOrder.size() < 10) {
                             selectionOrder.add(var.negate());
                         }

src/test/java/org/logicng/transformations/cnf/BDDCNFTest.java

@@ -42,7 +42,7 @@
 
 /**
  * Unit Tests for {@link BDDCNFTransformation}.
- * @version 2.3.0
+ * @version 2.4.2
  * @since 1.4.0
  */
 public class BDDCNFTest extends TestWithExampleFormulas {
@@ -160,7 +160,7 @@ public void testNot() throws ParserException {
     @Test
     public void testCC() throws ParserException {
         final PseudoBooleanParser p = new PseudoBooleanParser(this.f);
-        final Formula f1 = p.parse("a <=> (1 * b <= 1)");
+        final Formula f1 = p.parse("a <=> (1 * b <= 0)");
         final Formula f2 = p.parse("~(1 * b <= 1)");
         final Formula f3 = p.parse("(1 * b + 1 * c + 1 * d <= 1)");
         final Formula f4 = p.parse("~(1 * b + 1 * c + 1 * d <= 1)");

src/test/java/org/logicng/transformations/dnf/BDDDNFTest.java

@@ -43,7 +43,7 @@
 
 /**
  * Unit Tests for {@link BDDDNFTransformation}.
- * @version 2.3.0
+ * @version 2.4.2
  * @since 2.3.0
  */
 public class BDDDNFTest extends TestWithExampleFormulas {
@@ -162,7 +162,7 @@ public void testNot() throws ParserException {
     @Test
     public void testCC() throws ParserException {
         final PseudoBooleanParser p = new PseudoBooleanParser(this.f);
-        final Formula f1 = p.parse("a <=> (1 * b <= 1)");
+        final Formula f1 = p.parse("a <=> (1 * b <= 0)");
         final Formula f2 = p.parse("~(1 * b <= 1)");
         final Formula f3 = p.parse("(1 * b + 1 * c + 1 * d <= 1)");
         final Formula f4 = p.parse("~(1 * b + 1 * c + 1 * d <= 1)");