diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java index 72014bf5..193cc0a8 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java @@ -1844,7 +1844,7 @@ protected void createInitialCandidates(final List variables, final Back final boolean modelPhase = model.get(var); if (isBothOrNegativeType(type) && !modelPhase || isBothOrPositiveType(type) && modelPhase) { final int lit = mkLit(var, !modelPhase); - if (!config.lowLevelConfig.bbInitialUBCheckForRotatableLiterals || !isRotatable(lit)) { + if (!isRotatable(lit)) { backboneCandidates.add(lit); } } @@ -1861,9 +1861,9 @@ protected void refineUpperBound() { if (isUPZeroLit(var)) { backboneCandidates.remove(lit); addBackboneLiteral(lit); - } else if (config.lowLevelConfig.bbCheckForComplementModelLiterals && model.get(var) == sign(lit)) { + } else if (model.get(var) == sign(lit)) { backboneCandidates.remove(lit); - } else if (config.lowLevelConfig.bbCheckForRotatableLiterals && isRotatable(lit)) { + } else if (isRotatable(lit)) { backboneCandidates.remove(lit); } } diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java b/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java index 1a56e879..107ed966 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/SATSolverLowLevelConfig.java @@ -29,11 +29,6 @@ public final class SATSolverLowLevelConfig { final int reduceOnSizeSize; final double maxVarDecay; - // backbone related - final boolean bbInitialUBCheckForRotatableLiterals; - final boolean bbCheckForComplementModelLiterals; - final boolean bbCheckForRotatableLiterals; - private SATSolverLowLevelConfig(final Builder builder) { varDecay = builder.varDecay; varInc = builder.varInc; @@ -55,9 +50,6 @@ private SATSolverLowLevelConfig(final Builder builder) { reduceOnSize = builder.reduceOnSize; reduceOnSizeSize = builder.reduceOnSizeSize; maxVarDecay = builder.maxVarDecay; - bbInitialUBCheckForRotatableLiterals = builder.bbInitialUBCheckForRotatableLiterals; - bbCheckForComplementModelLiterals = builder.bbCheckForComplementModelLiterals; - bbCheckForRotatableLiterals = builder.bbCheckForRotatableLiterals; } public static Builder builder() { @@ -87,9 +79,6 @@ public String toString() { sb.append("reduceOnSize=").append(reduceOnSize).append(System.lineSeparator()); sb.append("reduceOnSizeSize=").append(reduceOnSizeSize).append(System.lineSeparator()); sb.append("maxVarDecay=").append(maxVarDecay).append(System.lineSeparator()); - sb.append("bbInitialUBCheckForRotatableLiterals=").append(bbInitialUBCheckForRotatableLiterals).append(System.lineSeparator()); - sb.append("bbCheckForComplementModelLiterals=").append(bbCheckForComplementModelLiterals).append(System.lineSeparator()); - sb.append("bbCheckForRotatableLiterals=").append(bbCheckForRotatableLiterals).append(System.lineSeparator()); sb.append("}"); return sb.toString(); } @@ -115,9 +104,6 @@ public static class Builder { private boolean reduceOnSize = false; private int reduceOnSizeSize = 12; private double maxVarDecay = 0.95; - private boolean bbInitialUBCheckForRotatableLiterals = true; - private boolean bbCheckForComplementModelLiterals = true; - private boolean bbCheckForRotatableLiterals = true; private Builder() { // Initialize only via factory @@ -328,43 +314,7 @@ public Builder maxVarDecay(final double maxVarDecay) { this.maxVarDecay = maxVarDecay; return this; } - - /** - * Sets whether the backbone algorithm should check for rotatable literals. - * The default value is {@code true}. - * @param checkForRotatableLiterals the boolean value that is {@code true} if the algorithm should check for - * rotatables or {@code false} otherwise. - * @return the builder - */ - public Builder bbCheckForRotatableLiterals(final boolean checkForRotatableLiterals) { - bbCheckForRotatableLiterals = checkForRotatableLiterals; - return this; - } - - /** - * Sets whether the backbone algorithm should check for rotatable literals during initial unit propagation. - * The default value is {@code true}. - * @param initialUBCheckForRotatableLiterals the boolean value that is {@code true} if the algorithm should - * check for rotatables or {@code false} otherwise. - * @return the builder - */ - public Builder bbInitialUBCheckForRotatableLiterals(final boolean initialUBCheckForRotatableLiterals) { - bbInitialUBCheckForRotatableLiterals = initialUBCheckForRotatableLiterals; - return this; - } - - /** - * Sets whether the backbone algorithm should check for complement model literals. - * The default value is {@code true}. - * @param checkForComplementModelLiterals the boolean value that is {@code true} if the algorithm should check for - * complement literals or {@code false} otherwise. - * @return the builder - */ - public Builder bbCheckForComplementModelLiterals(final boolean checkForComplementModelLiterals) { - bbCheckForComplementModelLiterals = checkForComplementModelLiterals; - return this; - } - + /** * Builds the SAT solver configuration. * @return the configuration diff --git a/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java b/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java index fe10eeea..c7f13760 100644 --- a/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java +++ b/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java @@ -21,8 +21,6 @@ import com.booleworks.logicng.solvers.SATSolver; import com.booleworks.logicng.solvers.SolverState; import com.booleworks.logicng.solvers.functions.BackboneFunction; -import com.booleworks.logicng.solvers.sat.SATSolverConfig; -import com.booleworks.logicng.solvers.sat.SATSolverLowLevelConfig; import com.booleworks.logicng.util.FormulaHelper; import org.assertj.core.api.Assertions; import org.junit.jupiter.api.Test; @@ -268,26 +266,6 @@ public void testBackboneType() { solver.loadState(before); } - @Test - public void testDifferentConfigurations() throws IOException, ParserException { - final List configs = new ArrayList<>(); - configs.add(SATSolverConfig.builder().lowLevelConfig(SATSolverLowLevelConfig.builder().bbCheckForComplementModelLiterals(false).build()).build()); - configs.add(SATSolverConfig.builder().lowLevelConfig(SATSolverLowLevelConfig.builder().bbCheckForRotatableLiterals(false).build()).build()); - configs.add(SATSolverConfig.builder().lowLevelConfig(SATSolverLowLevelConfig.builder().bbInitialUBCheckForRotatableLiterals(false).build()).build()); - - final FormulaFactory f = FormulaFactory.caching(); - final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); - SATSolver solver = SATSolver.newSolver(f); - solver.add(formula); - final Backbone backbone = solver.execute(BackboneFunction.builder().variables(formula.variables(f)).build()); - - for (final SATSolverConfig config : configs) { - solver = SATSolver.newSolver(f, config); - solver.add(formula); - Assertions.assertThat(solver.execute(BackboneFunction.builder().variables(formula.variables(f)).build())).isEqualTo(backbone); - } - } - @Test public void testCancellationPoints() throws IOException { final List formulas = DimacsReader.readCNF(f, "src/test/resources/sat/term1_gr_rcs_w4.shuffled.cnf"); diff --git a/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java b/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java index 251f9c42..fb5ce541 100644 --- a/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java @@ -4,8 +4,8 @@ package com.booleworks.logicng.solvers.functions; -import static com.booleworks.logicng.solvers.sat.SATSolverConfig.CNFMethod.FACTORY_CNF; -import static com.booleworks.logicng.solvers.sat.SATSolverConfig.CNFMethod.PG_ON_SOLVER; +import static com.booleworks.logicng.solvers.sat.SolverTestSet.SATSolverConfigParam.CNF_METHOD; +import static com.booleworks.logicng.solvers.sat.SolverTestSet.SATSolverConfigParam.USE_AT_MOST_CLAUSES; import static org.assertj.core.api.Assertions.assertThat; import com.booleworks.logicng.LongRunningTag; @@ -19,8 +19,7 @@ import com.booleworks.logicng.solvers.SATSolver; import com.booleworks.logicng.solvers.SolverState; import com.booleworks.logicng.solvers.sat.SATSolverConfig; -import com.booleworks.logicng.solvers.sat.SATSolverLowLevelConfig; -import com.booleworks.logicng.util.Pair; +import com.booleworks.logicng.solvers.sat.SolverTestSet; import org.assertj.core.api.Assertions; import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; @@ -33,88 +32,31 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.List; +import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; -import java.util.function.Supplier; -import java.util.stream.Collectors; @SuppressWarnings("unused") public class BackboneFunctionTest { - private static final FormulaFactory f = FormulaFactory.caching(); - - private static SATSolverConfig.Builder config(final boolean useAtMostClauses, final SATSolverConfig.CNFMethod cnfMethod, - final boolean bbCheckForRotatableLiterals, final boolean bbCheckForComplementModelLiterals, - final boolean bbInitialUBCheckForRotatableLiterals) { - return SATSolverConfig.builder() - .useAtMostClauses(useAtMostClauses) - .cnfMethod(cnfMethod) - .lowLevelConfig(SATSolverLowLevelConfig.builder() - .bbCheckForRotatableLiterals(bbCheckForRotatableLiterals) - .bbCheckForComplementModelLiterals(bbCheckForComplementModelLiterals) - .bbInitialUBCheckForRotatableLiterals(bbInitialUBCheckForRotatableLiterals) - .build()); - } public static List solvers() { - final Supplier configNoAmNoPG1 = () -> config(false, FACTORY_CNF, false, false, false); - final Supplier configNoAmNoPG2 = () -> config(false, FACTORY_CNF, true, false, false); - final Supplier configNoAmNoPG3 = () -> config(false, FACTORY_CNF, false, true, false); - final Supplier configNoAmNoPG4 = () -> config(false, FACTORY_CNF, false, false, true); - final Supplier configNoAmNoPG5 = () -> config(false, FACTORY_CNF, true, true, true); - final Supplier configNoAmPG1 = () -> config(false, PG_ON_SOLVER, false, false, false); - final Supplier configNoAmPG2 = () -> config(false, PG_ON_SOLVER, true, false, false); - final Supplier configNoAmPG3 = () -> config(false, PG_ON_SOLVER, false, true, false); - final Supplier configNoAmPG4 = () -> config(false, PG_ON_SOLVER, false, false, true); - final Supplier configNoAmPG5 = () -> config(false, PG_ON_SOLVER, true, true, true); - final Supplier configNoPG1 = () -> config(true, FACTORY_CNF, false, false, false); - final Supplier configNoPG2 = () -> config(true, FACTORY_CNF, true, false, false); - final Supplier configNoPG3 = () -> config(true, FACTORY_CNF, false, true, false); - final Supplier configNoPG4 = () -> config(true, FACTORY_CNF, false, false, true); - final Supplier configNoPG5 = () -> config(true, FACTORY_CNF, true, true, true); - final Supplier configPG1 = () -> config(true, PG_ON_SOLVER, false, false, false); - final Supplier configPG2 = () -> config(true, PG_ON_SOLVER, true, false, false); - final Supplier configPG3 = () -> config(true, PG_ON_SOLVER, false, true, false); - final Supplier configPG4 = () -> config(true, PG_ON_SOLVER, false, false, true); - final Supplier configPG5 = () -> config(true, PG_ON_SOLVER, true, true, true); - final List, String>> configs = Arrays.asList( - new Pair<>(configNoAmNoPG1, "FF CNF -ATM -ROT -COMP -UB"), - new Pair<>(configNoAmNoPG2, "FF CNF -ATM +ROT -COMP -UB"), - new Pair<>(configNoAmNoPG3, "FF CNF -ATM -ROT +COMP -UB"), - new Pair<>(configNoAmNoPG4, "FF CNF -ATM -ROT -COMP +UB"), - new Pair<>(configNoAmNoPG5, "FF CNF -ATM +ROT +COMP +UB"), - new Pair<>(configNoAmPG1, "PG CNF -ATM -ROT -COMP -UB"), - new Pair<>(configNoAmPG2, "PG CNF -ATM +ROT -COMP -UB"), - new Pair<>(configNoAmPG3, "PG CNF -ATM -ROT +COMP -UB"), - new Pair<>(configNoAmPG4, "PG CNF -ATM -ROT -COMP +UB"), - new Pair<>(configNoAmPG5, "PG CNF -ATM +ROT +COMP +UB"), - new Pair<>(configNoPG1, "FF CNF +ATM -ROT -COMP -UB"), - new Pair<>(configNoPG2, "FF CNF +ATM +ROT -COMP -UB"), - new Pair<>(configNoPG3, "FF CNF +ATM -ROT +COMP -UB"), - new Pair<>(configNoPG4, "FF CNF +ATM -ROT -COMP +UB"), - new Pair<>(configNoPG5, "FF CNF +ATM +ROT +COMP +UB"), - new Pair<>(configPG1, "PG CNF +ATM -ROT -COMP -UB"), - new Pair<>(configPG2, "PG CNF +ATM +ROT -COMP -UB"), - new Pair<>(configPG3, "PG CNF +ATM -ROT +COMP -UB"), - new Pair<>(configPG4, "PG CNF +ATM -ROT -COMP +UB"), - new Pair<>(configPG5, "PG CNF +ATM +ROT +COMP +UB") - ); - return configs.stream() - .map(config -> Arguments.of(SATSolver.newSolver(f, config.first().get().build()), config.second())) - .collect(Collectors.toList()); + final FormulaFactory f = FormulaFactory.caching(); + return SolverTestSet.solverTestSetForParameterizedTests(Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD), f); } @ParameterizedTest(name = "{index} {1}") @MethodSource("solvers") public void testConstants(final SATSolver solver, final String solverDescription) { + final FormulaFactory f = solver.factory(); final SolverState state = solver.saveState(); solver.add(f.falsum()); - Backbone backbone = solver.backbone(v("a b c")); + Backbone backbone = solver.backbone(v("a b c", f)); assertThat(backbone.isSat()).isFalse(); assertThat(backbone.getCompleteBackbone(f)).isEmpty(); solver.loadState(state); solver.add(f.verum()); - backbone = solver.backbone(v("a b c")); + backbone = solver.backbone(v("a b c", f)); assertThat(backbone.isSat()).isTrue(); Assertions.assertThat(backbone.getCompleteBackbone(f)).isEmpty(); } @@ -122,14 +64,15 @@ public void testConstants(final SATSolver solver, final String solverDescription @ParameterizedTest(name = "{index} {1}") @MethodSource("solvers") public void testSimpleBackbones(final SATSolver solver, final String solverDescription) throws ParserException { + final FormulaFactory f = solver.factory(); final SolverState state = solver.saveState(); solver.add(f.parse("a & b & ~c")); - Backbone backbone = solver.backbone(v("a b c")); + Backbone backbone = solver.backbone(v("a b c", f)); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone(f)).containsExactly(f.variable("a"), f.variable("b"), f.literal("c", false)); solver.loadState(state); solver.add(f.parse("~a & ~b & c")); - backbone = solver.backbone(v("a c")); + backbone = solver.backbone(v("a c", f)); assertThat(backbone.isSat()).isTrue(); Assertions.assertThat(backbone.getCompleteBackbone(f)).containsExactly(f.literal("a", false), f.variable("c")); } @@ -137,14 +80,15 @@ public void testSimpleBackbones(final SATSolver solver, final String solverDescr @ParameterizedTest(name = "{index} {1}") @MethodSource("solvers") public void testSimpleFormulas(final SATSolver solver, final String solverDescription) throws ParserException { + final FormulaFactory f = solver.factory(); solver.add(f.parse("(a => c | d) & (b => d | ~e) & (a | b)")); - Backbone backbone = solver.backbone(v("a b c d e f")); + Backbone backbone = solver.backbone(v("a b c d e f", f)); assertThat(backbone.isSat()).isTrue(); Assertions.assertThat(backbone.getCompleteBackbone(f)).isEmpty(); solver.add(f.parse("a => b")); solver.add(f.parse("b => a")); solver.add(f.parse("~d")); - backbone = solver.backbone(v("a b c d e f g h")); + backbone = solver.backbone(v("a b c d e f g h", f)); assertThat(backbone.isSat()).isTrue(); Assertions.assertThat(backbone.getCompleteBackbone(f)).containsExactly(f.variable("a"), f.variable("b"), f.variable("c"), f.literal("d", false), f.literal("e", false)); @@ -153,6 +97,7 @@ public void testSimpleFormulas(final SATSolver solver, final String solverDescri @ParameterizedTest(name = "{index} {1}") @MethodSource("solvers") public void testSimpleFormulasWithBuilderUsage(final SATSolver solver, final String solverDescription) throws ParserException { + final FormulaFactory f = solver.factory(); solver.add(f.parse("(a => c | d) & (b => d | ~e) & (a | b)")); Backbone backbone = solver.execute(BackboneFunction.builder().variables( f.variable("a"), f.variable("b"), f.variable("c"), f.variable("d"), f.variable("e"), f.variable("f")) @@ -162,7 +107,7 @@ public void testSimpleFormulasWithBuilderUsage(final SATSolver solver, final Str solver.add(f.parse("a => b")); solver.add(f.parse("b => a")); solver.add(f.parse("~d")); - backbone = solver.backbone(v("a b c d e f g h")); + backbone = solver.backbone(v("a b c d e f g h", f)); assertThat(backbone.isSat()).isTrue(); Assertions.assertThat(backbone.getCompleteBackbone(f)).containsExactly(f.variable("a"), f.variable("b"), f.variable("c"), f.literal("d", false), f.literal("e", false)); @@ -172,6 +117,7 @@ public void testSimpleFormulasWithBuilderUsage(final SATSolver solver, final Str @MethodSource("solvers") @LongRunningTag public void testRealFormulaIncremental1(final SATSolver solver, final String solverDescription) throws IOException, ParserException { + final FormulaFactory f = solver.factory(); final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); solver.add(formula); final List expectedBackbones = new ArrayList<>(); @@ -181,26 +127,26 @@ public void testRealFormulaIncremental1(final SATSolver solver, final String sol } reader.close(); Backbone backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0), f)); solver.add(f.variable("v411")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v385")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v275")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v188")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v103")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v404")); backbone = solver.backbone(formula.variables(f)); @@ -212,6 +158,7 @@ public void testRealFormulaIncremental1(final SATSolver solver, final String sol @MethodSource("solvers") @LongRunningTag public void testRealFormulaIncremental2(final SATSolver solver, final String solverDescription) throws IOException, ParserException { + final FormulaFactory f = solver.factory(); final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); solver.add(formula); final List expectedBackbones = new ArrayList<>(); @@ -221,26 +168,26 @@ public void testRealFormulaIncremental2(final SATSolver solver, final String sol } reader.close(); Backbone backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0), f)); solver.add(f.variable("v2609")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v2416")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v2048")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v39")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v1663")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5), f)); assertThat(backbone.isSat()).isTrue(); solver.add(f.variable("v2238")); backbone = solver.backbone(formula.variables(f)); @@ -252,6 +199,7 @@ public void testRealFormulaIncremental2(final SATSolver solver, final String sol @MethodSource("solvers") @LongRunningTag public void testRealFormulaIncrementalDecremental1(final SATSolver solver, final String solverDescription) throws IOException, ParserException { + final FormulaFactory f = solver.factory(); final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); solver.add(formula); final SolverState state = solver.saveState(); @@ -262,34 +210,34 @@ public void testRealFormulaIncrementalDecremental1(final SATSolver solver, final } reader.close(); Backbone backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0), f)); solver.add(f.variable("v411")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v411 & v385")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v411 & v385 & v275")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v411 & v385 & v275 & v188")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v411 & v385 & v275 & v188 & v103")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); @@ -303,6 +251,7 @@ public void testRealFormulaIncrementalDecremental1(final SATSolver solver, final @MethodSource("solvers") @LongRunningTag public void testRealFormulaIncrementalDecremental2(final SATSolver solver, final String solverDescription) throws IOException, ParserException { + final FormulaFactory f = solver.factory(); final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); solver.add(formula); final SolverState state = solver.saveState(); @@ -313,34 +262,34 @@ public void testRealFormulaIncrementalDecremental2(final SATSolver solver, final } reader.close(); Backbone backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(0), f)); solver.add(f.variable("v2609")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(1), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v2609 & v2416")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(2), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v2609 & v2416 & v2048")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(3), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v2609 & v2416 & v2048 & v39")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(4), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); solver.add(f.parse("v2609 & v2416 & v2048 & v39 & v1663")); backbone = solver.backbone(formula.variables(f)); - Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5))); + Assertions.assertThat(backbone.getCompleteBackbone(f)).isEqualTo(parseBackbone(expectedBackbones.get(5), f)); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); @@ -362,7 +311,7 @@ public void testMiniCardSpecialCase() throws ParserException { Assertions.assertThat(backboneMC.getNegativeBackbone()).extracting(Variable::name).containsExactlyInAnyOrder("v6", "v60"); } - private SortedSet v(final String s) { + private SortedSet v(final String s, final FormulaFactory f) { final SortedSet vars = new TreeSet<>(); for (final String name : s.split(" ")) { vars.add(f.variable(name)); @@ -370,7 +319,7 @@ private SortedSet v(final String s) { return vars; } - private SortedSet parseBackbone(final String string) throws ParserException { + private SortedSet parseBackbone(final String string, final FormulaFactory f) throws ParserException { final SortedSet literals = new TreeSet<>(); for (final String lit : string.split(" ")) { literals.add((Literal) f.parse(lit)); diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java index 3bac8548..60ccd85f 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/ConfigurationsTest.java @@ -58,9 +58,6 @@ public void testSolverConfigToString() { "reduceOnSize=true%n" + "reduceOnSizeSize=10%n" + "maxVarDecay=0.99%n" + - "bbInitialUBCheckForRotatableLiterals=true%n" + - "bbCheckForComplementModelLiterals=true%n" + - "bbCheckForRotatableLiterals=true%n" + "}"); assertThat(config.toString()).isEqualTo(expected); }