removed backbone configuration parameters from SATSolverConfig

booleworks · Apr 4, 2024 · 944e268 · 944e268
1 parent c85e8c6
commit 944e268
Show file tree

Hide file tree

Showing 5 changed files with 51 additions and 177 deletions.
diff --git 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<Integer> 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
@@ -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
@@ -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<SATSolverConfig> 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<Formula> formulas = DimacsReader.readCNF(f, "src/test/resources/sat/term1_gr_rcs_w4.shuffled.cnf");