From 5cdab69e166bb7366bf4b3c66dacdae47cf48cb1 Mon Sep 17 00:00:00 2001 From: Rouven Walter Date: Tue, 31 Jan 2023 17:36:32 +0100 Subject: [PATCH] fixed SATSolver#add: Ensure all variables are added to the internal solver --- CHANGELOG.md | 6 ++++ pom.xml | 2 +- .../java/org/logicng/solvers/MiniSat.java | 14 +++++++- .../cardinalityconstraints/CCALKTest.java | 4 +-- .../cardinalityconstraints/CCAMKTest.java | 6 ++-- .../ModelEnumerationFunctionTest.java | 32 ++++++++++++++++++- .../java/org/logicng/solvers/sat/SATTest.java | 31 +++++++++++++++--- .../transformations/cnf/BDDCNFTest.java | 4 +-- .../transformations/dnf/BDDDNFTest.java | 4 +-- 9 files changed, 86 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1e9b85fa..df47d769 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/pom.xml b/pom.xml index 66b1acb9..da4fb766 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.5.0-SNAPSHOT + 2.4.2-SNAPSHOT bundle LogicNG diff --git a/src/main/java/org/logicng/solvers/MiniSat.java b/src/main/java/org/logicng/solvers/MiniSat.java index 5b4e8f00..4428b014 100644 --- a/src/main/java/org/logicng/solvers/MiniSat.java +++ b/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) { diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java index 6270f631..fdebac98 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java +++ b/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); diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java index 984dba52..611f0e67 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java +++ b/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++); } } diff --git a/src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java b/src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java index 0e3aa04b..73fa7237 100644 --- a/src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java +++ b/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 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 models = solver.execute(ModelEnumerationFunction.builder().variables(this.f.variables("A", "X")).build()); + assertThat(models).hasSize(1); + assertThat(models.get(0).literals()).containsExactly(a); + } } diff --git a/src/test/java/org/logicng/solvers/sat/SATTest.java b/src/test/java/org/logicng/solvers/sat/SATTest.java index d2949650..079e96fa 100644 --- a/src/test/java/org/logicng/solvers/sat/SATTest.java +++ b/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 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()); } diff --git a/src/test/java/org/logicng/transformations/cnf/BDDCNFTest.java b/src/test/java/org/logicng/transformations/cnf/BDDCNFTest.java index 1ff65372..f0768f33 100644 --- a/src/test/java/org/logicng/transformations/cnf/BDDCNFTest.java +++ b/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)"); diff --git a/src/test/java/org/logicng/transformations/dnf/BDDDNFTest.java b/src/test/java/org/logicng/transformations/dnf/BDDDNFTest.java index 9ce2cff8..581b528f 100644 --- a/src/test/java/org/logicng/transformations/dnf/BDDDNFTest.java +++ b/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)");