diff --git a/org.sat4j.core/src/main/java/org/sat4j/core/VecInt.java b/org.sat4j.core/src/main/java/org/sat4j/core/VecInt.java index b4f9da8228114b3569e8c026a6ba03c215cfa96f..08bf2c6b9fcfb3c2505a90b82721f4cf64f83edf 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/core/VecInt.java +++ b/org.sat4j.core/src/main/java/org/sat4j/core/VecInt.java @@ -540,6 +540,8 @@ public final class VecInt implements IVecInt { } /** + * Grants access to the internal array of this container. Note that this may contain + * removed entries, so this function should not be used as a converter. * @since 2.1 */ public int[] toArray() { diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java index 072f04b4d8705aee32c3854781f743df6fdd9a1c..6e814f82082bdfd19b6cb9b4808794f6ca9a40f0 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java @@ -49,6 +49,8 @@ import java.util.Timer; import java.util.TimerTask; import java.util.logging.Level; import java.util.logging.Logger; +import java.util.BitSet; +import java.util.Arrays; import org.sat4j.core.ConstrGroup; import org.sat4j.core.LiteralsUtils; @@ -1472,6 +1474,93 @@ public class Solver return this.prime[Math.abs(p)] == p; } + /** + * The method computes the intersection of all implicants that are in the current model, + * also known as unrotatable literals. This is valuable for the computation of backbones + * Note that this set of literals alone does not satisfy the formula. Literals are + * returned in DIMACS format. + */ + public int[] getImplicantIntersection() { + /* Algorithmic note: + The intersection of all implicants in the model is exactly the set of literals for + which there exists a clause that is only satisfied by that literal. Otherwise the + literal would be rotatable, i.e. for literal 'a' and model m, (m\a) would also + satisfy the formula + */ + + //special case: all literals are unit propagated, then none of them are optional and + // no tests have to be done. + if(this.implied.size() == this.nVars()) { + return Arrays.copyOf(this.model, this.model.length); + } + + //the model needs to be stored in a bitset to quickly determine whether a clause + // literal is satisfied + BitSet literalFulfilled = new BitSet(2 * this.nVars() + 1); + //The unrotatable literals have to stored in a bitset to prevent duplicates + BitSet requiredLits = new BitSet(2 * this.nVars() + 1); + for (int lit : this.model) { + literalFulfilled.set(LiteralsUtils.toInternal(lit)); + } + + //unit implied literals must be in the implicant intersection + for (int ui = 0; ui < implied.size(); ui++) { + int unitLit = LiteralsUtils.toInternal(implied.get(ui)); + requiredLits.set(unitLit); + } + + for (int constrIdx = 0; constrIdx < this.constrs.size(); constrIdx++) { + Constr curConstr = this.constrs.get(constrIdx); + // This value takes the value of the first satisfying literal, but becomes 0 + // again when another satisfying literal is found. + int uniqueSatisfyingLiteral = 0;//in internal representation + + //This loop usually stops after very few iterations, because + // watched literal clauses are implemented in a way that the watched literals + // are moved to the start of the clause. If watched literals are implemented in + // an explicit way with index variables, then these should be checked first. + for (int li = 0; li < curConstr.size(); li++) { + int curLitInternal = curConstr.get(li); + if (requiredLits.get(curLitInternal)) { + //already identified as unrotatable, therefore the literal is satisfied + // and already stored. Nothing more to do in this clause + uniqueSatisfyingLiteral = 0; + break; + } + boolean satisfies = literalFulfilled.get(curLitInternal); + if (satisfies) { + if (uniqueSatisfyingLiteral == 0) { + uniqueSatisfyingLiteral = curLitInternal; + } else { + //found another satisfying literal, abort + uniqueSatisfyingLiteral = 0; + break; + } + } + } + if (uniqueSatisfyingLiteral != 0) { + requiredLits.set(uniqueSatisfyingLiteral); + } + } + + //convert the bitset to an int[] + int[] retu = new int[requiredLits.cardinality()]; + int retuIdx = 0; + int prevSetBit = 0; + do { + int nextBit = requiredLits.nextSetBit(prevSetBit); + if (nextBit == -1) { + break; + } + retu[retuIdx] = LiteralsUtils.toDimacs(nextBit); + retuIdx++; + prevSetBit = nextBit + 1; + + } while (true); + assert retuIdx == retu.length; + return retu; + } + public boolean model(int var) { if (var <= 0 || var > realNumberOfVariables()) { throw new IllegalArgumentException( diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/orders/ExplicitPhaseSelectionStrategy.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/orders/ExplicitPhaseSelectionStrategy.java new file mode 100644 index 0000000000000000000000000000000000000000..79c3d632cdbdaee883078a4632fd6345746a00d8 --- /dev/null +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/orders/ExplicitPhaseSelectionStrategy.java @@ -0,0 +1,84 @@ +package org.sat4j.minisat.orders; + +import org.sat4j.minisat.core.IPhaseSelectionStrategy; + +import java.util.BitSet; + +import static org.sat4j.core.LiteralsUtils.*; + +/** + * This phase selection can be configured so that during a decision the same literal is + * always assigned the same boolean value. This value must be set before the sat call. + * Unconfigured variables are given a value through a fallback strategy, which must be given + * with the constructor. + */ +public class ExplicitPhaseSelectionStrategy implements IPhaseSelectionStrategy { + /** + * Is consulted when the queried variable is not configured + */ + private IPhaseSelectionStrategy fallbackStrat; + /** + * Contains marks for preferred literal assignments. + */ + private BitSet explicits; + + /** + * @param myDefault the phase strategy that decides on unconfigured variables + * @param nVars how many variables are in the solver + */ + public ExplicitPhaseSelectionStrategy( + IPhaseSelectionStrategy myDefault, int nVars) { + this.fallbackStrat = myDefault; + this.explicits = new BitSet(nVars * 2 + 1); + } + + /** + * Configures this phase selector to always return the literal given here, when + * being asked for the phase for this literals variable + * + * @param l expected in internal format + */ + public void setPreference(int l) { + assert l > 0; //expected in internal format + this.explicits.set(l); + } + + @Override + public void updateVar(int p) { + fallbackStrat.updateVar(p); + } + + @Override + public void init(int nlength) { + fallbackStrat.init(nlength); + } + + @Override + public void init(int var, int p) { + fallbackStrat.init(var, p); + } + + @Override + public void assignLiteral(int p) { + fallbackStrat.assignLiteral(p); + } + + @Override + public int select(int var) { + int lit = posLit(var); + if (this.explicits.get(lit)) { + return lit; + } + lit = negLit(var); + if (this.explicits.get(lit)) { + return lit; + } + //variable was not conigured so let the default strategy decide + return this.fallbackStrat.select(var); + } + + @Override + public void updateVarAtDecisionLevel(int q) { + this.fallbackStrat.updateVarAtDecisionLevel(q); + } +} diff --git a/org.sat4j.core/src/main/java/org/sat4j/tools/Backbone.java b/org.sat4j.core/src/main/java/org/sat4j/tools/Backbone.java index 67a3249ef30ddd98c6c74c0ad89a7c6f5857e907..5e12fffcfb83f309891e1b69396a888b71e6f106 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/tools/Backbone.java +++ b/org.sat4j.core/src/main/java/org/sat4j/tools/Backbone.java @@ -32,6 +32,11 @@ package org.sat4j.tools; import java.util.BitSet; import org.sat4j.core.VecInt; +import org.sat4j.minisat.core.IOrder; +import org.sat4j.minisat.core.Solver; +import org.sat4j.minisat.orders.ExplicitPhaseSelectionStrategy; +import org.sat4j.minisat.orders.LevelBasedVarOrderHeap; +import org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy; import org.sat4j.specs.ContradictionException; import org.sat4j.specs.IConstr; import org.sat4j.specs.ISolver; @@ -39,6 +44,9 @@ import org.sat4j.specs.IVecInt; import org.sat4j.specs.IteratorInt; import org.sat4j.specs.TimeoutException; +import static org.sat4j.core.LiteralsUtils.toDimacs; +import static org.sat4j.core.LiteralsUtils.toInternal; + /** * The aim of this class is to compute efficiently the literals implied by the * set of constraints (also called backbone or unit implicates). @@ -60,15 +68,31 @@ public final class Backbone { this.listener = listener; } + /** + * If the backbone algorithm is configured to use implicant simplification, then the + * found models are reduced either to a prime implicant or the intersection of all + * implicants in the model (if available) + * + * The first found model is always reduced regardless of this flag + */ public void setImplicantSimplification(boolean b) { this.implicant = b; } public int[] simplifiedModel(ISolver solver) { if (implicant) { - return solver.primeImplicant(); + if (solver instanceof Solver) + { + return ((Solver) solver).getImplicantIntersection(); + }else + { + return solver.primeImplicant(); + } + } + else { + return solver.model(); } - return solver.model(); + } public IVecInt compute(ISolver solver, int[] implicant, @@ -120,8 +144,8 @@ public final class Backbone { IVecInt litsToTest) throws TimeoutException; static void removeVarNotPresentAndSatisfiedLits(int[] implicant, - IVecInt litsToTest, int n) { - int[] marks = new int[n + 1]; + IVecInt litsToTest, int nVars) { + int[] marks = new int[nVars + 1]; for (int p : implicant) { marks[p > 0 ? p : -p] = p; } @@ -227,6 +251,147 @@ public final class Backbone { } }; + /** + * Similar to the IBB algorithm, this one refines a backbone estimate, which however + * converges much faster, because a modified decision heuristic is applied, selecting + * literals greedily to disprove as many backbone literals in a single SAT call as + * possible. The drawback is, that this algorithm can perform much worse for + * difficult formulas that benefit heavily from normal decision heuristics. + * + * This algorithm only works with instances of the 'Solver' class. + * + * This algorithm does not need to modify the formula, therefore the learned clauses are + * still valid after the backbone calculation. + * + * This algorithm is taken from 'A Preference-Based Approach to Backbone Computation + * with Application to Argumentation' by Alessandro Previti and Matti Jaervisalo + */ + private static final Backboner PBB = new Backboner() + { + /** + * Configures the solver to have preferences, i.e. that certain variables are always + * assigned the same preconfigured value, if the variable is assigned through a + * decision. Preferred assignments are always done first. Remember to reset the + * variable order system to the previous state once the backbone is computed. + * @param solver This solver will get a changed decision strategy + * @param literalsToTest the literals to be preferred in dimacs format. These should + * be all literals that were not yet encountered. + */ + void setupPreferences(Solver solver, IVecInt literalsToTest) + { + //literalsToTest is always given in dimacs format and contains the literals + // that were not yet seen in a model or optional in an implicant(-intersection) + ExplicitPhaseSelectionStrategy pStrat = new ExplicitPhaseSelectionStrategy( + new PhaseInLastLearnedClauseSelectionStrategy(),solver.nVars()); + for(int pidx = 0; pidx < literalsToTest.size();pidx++) + { + int curLitInternal = toInternal(literalsToTest.get(pidx)); + pStrat.setPreference(curLitInternal); + } + + LevelBasedVarOrderHeap newOrder = new LevelBasedVarOrderHeap(pStrat); + VecInt prefVars = new VecInt(literalsToTest.size()); + for (int pidx = 0; pidx < literalsToTest.size(); pidx++) + { + int pVar = literalsToTest.get(pidx); + pVar = Math.abs(pVar); + prefVars.push(pVar); + } + newOrder.addLevel(prefVars); + + solver.setOrder(newOrder); + } + + + @Override + IVecInt compute(ISolver solver, IVecInt assumptions, IVecInt litsToTest) + throws TimeoutException { + /* + This algorithm keeps finding new models purely through the preferences and stops + the loop once a model did not reduce the backbone estimate any further. This is + sufficient to guarantee convergence, because at that point all preferences are + inhibited by the fact that they are the negation of a backbone and the first + decision will not be from a preference. + */ + //need access to certain variables that are only available in the basic solver + // class + assert solver instanceof Solver; + Solver sol = (Solver) solver; + //the variable order is replaced regularly, keep a backup to restore later. + IOrder preOrder = sol.getOrder(); + int initLitsToTestSize = litsToTest.size(); + listener.start(initLitsToTestSize); + + //keep the intersection of found models in a bitset to efficiently calculate new + // intersections. + BitSet implicantIntersection = new BitSet(2 * solver.nVars() + 1); + for (int lidx = 0; lidx < litsToTest.size(); lidx++) { + int internalLit = toInternal(-litsToTest.get(lidx)); + implicantIntersection.set(internalLit); + } + + while (true) { + setupPreferences(sol, litsToTest); + solver.findModel(assumptions); + this.incSatTests(); + + //some superset of the backbone + int[] modelReduction = simplifiedModel(sol); + + //apply the new model reduction to the intersection + //remove all flags in implicantIntersection where the literal does not occur + // in modelReduction + BitSet curModelReductionBitset = new BitSet(2 * solver.nVars() + 1); + for (int mLit : modelReduction) { + int internalLit = toInternal(mLit); + curModelReductionBitset.set(internalLit); + } + assert curModelReductionBitset.cardinality() == modelReduction.length; + int preCardinality = implicantIntersection.cardinality(); + implicantIntersection.and(curModelReductionBitset); + + if (implicantIntersection.cardinality() == preCardinality) { + //backbone approximation can not further be reduced, therefore it is the + // backbone + break; + } + + litsToTest.clear(); + int prevLit = 0; + int curLit = implicantIntersection.nextSetBit(prevLit); + while(curLit != -1) { + litsToTest.push(-toDimacs(curLit)); + prevLit = curLit + 1; + curLit = implicantIntersection.nextSetBit(prevLit); + } + listener.inProgress(initLitsToTestSize - litsToTest.size(), + initLitsToTestSize); + } + + //convert the bitset to a VecInt with Dimacs literals + VecInt retu = new VecInt(implicantIntersection.cardinality()); + int prevLit = 0; + do { + int curLit = implicantIntersection.nextSetBit(prevLit); + if (curLit == -1) + { + break; + } + retu.push(toDimacs(curLit)); + + prevLit = curLit+1; + } while (prevLit != -1); + + sol.setOrder(preOrder); //remove the preferring decision heuristic + listener.end(nbSatTests); + return retu; + } + }; + + + /** + * Holds an object that implements the actual backbone algorithm, either BB,IBB or PBB + */ private final Backboner bb; private final static Backbone instance = bb(); @@ -254,6 +419,13 @@ public final class Backbone { return new Backbone(IBB); } + public static Backbone pbb() + { + return new Backbone(PBB); + } + + + public IVecInt compute(ISolver solver) throws TimeoutException { return compute(solver, VecInt.EMPTY); } @@ -278,8 +450,23 @@ public final class Backbone { if (!result) { throw new IllegalArgumentException("Formula is UNSAT!"); } - return bb.compute(solver, solver.primeImplicant(), assumptions); + //dont take the implicant flag into account, because reducing the first model yields + // the most discarded literals + return bb.compute(solver, strongestAvailableReduction(solver), assumptions); + } + /** + * Chooses a model reduction for the first found model. + * @param sol + * @return + */ + private int[] strongestAvailableReduction(ISolver sol){ + if (sol instanceof Solver){ + return ((Solver) sol).getImplicantIntersection(); + } + else{ + return sol.primeImplicant(); + } } /** @@ -305,7 +492,7 @@ public final class Backbone { if (!result) { throw new IllegalArgumentException("Formula is UNSAT!"); } - return bb.compute(solver, solver.primeImplicant(), assumptions, filter); + return bb.compute(solver, strongestAvailableReduction(solver), assumptions, filter); } diff --git a/org.sat4j.core/src/test/java/org/sat4j/tools/BackboneTest.java b/org.sat4j.core/src/test/java/org/sat4j/tools/BackboneTest.java index 8a83d5124f28ddc60ea29f652a6e2a23a706ba1d..4612d8d66afcdd78c1504c9f86bf669e29218f3f 100644 --- a/org.sat4j.core/src/test/java/org/sat4j/tools/BackboneTest.java +++ b/org.sat4j.core/src/test/java/org/sat4j/tools/BackboneTest.java @@ -36,11 +36,14 @@ import static org.junit.Assert.assertTrue; import org.junit.Test; import org.sat4j.core.VecInt; import org.sat4j.minisat.SolverFactory; +import org.sat4j.minisat.core.Solver; import org.sat4j.specs.ContradictionException; import org.sat4j.specs.IGroupSolver; import org.sat4j.specs.ISolver; import org.sat4j.specs.IVecInt; import org.sat4j.specs.TimeoutException; +import java.util.Arrays; + public class BackboneTest { @@ -105,6 +108,36 @@ public class BackboneTest { IVecInt backbone = Backbone.instance().compute(solver); } + + @Test + public void pureUnitReduction() throws ContradictionException,TimeoutException { + //exists to cover the special case in implicant intersection computation + // if the number of unit implied assignments is equal to the number of literals, + // then no reduction is possible. + Solver sol = (Solver) SolverFactory.newDefault(); + //a simple formula where only one model exists + sol.addClause(new VecInt(new int[]{1})); + sol.addClause(new VecInt(new int[]{-1,2})); + sol.addClause(new VecInt(new int[]{-1,-2,3})); + sol.addClause(new VecInt(new int[]{-1,-2,-3,4})); + sol.addClause(new VecInt(new int[]{-1,-2,-3,-4,5})); + + int[] mdl = sol.findModel(); + assertEquals(sol.nVars(), mdl.length); + int[] implInters = sol.getImplicantIntersection(); + assertEquals(sol.nVars(), implInters.length); + + Arrays.sort(mdl); + Arrays.sort(implInters); + + //Expectation: all 5 literals are in both the model and the reduction + for(int l = 1; l <= 5; l++) { + assertEquals(l, mdl[l - 1]); + assertEquals(l, implInters[l - 1]); + } + } + + /** * Testcase to check that the problem with unit clauses does no longer * occurs. @@ -287,5 +320,4 @@ public class BackboneTest { assertEquals(4, iterator.realNumberOfVariables()); assertEquals(4, iterator.numberOfModelsFoundSoFar()); } - } \ No newline at end of file diff --git a/org.sat4j.core/src/test/java/org/sat4j/tools/PrefboneTest.java b/org.sat4j.core/src/test/java/org/sat4j/tools/PrefboneTest.java new file mode 100644 index 0000000000000000000000000000000000000000..f381b8f95f8410c51288dd3932a346133b44bdab --- /dev/null +++ b/org.sat4j.core/src/test/java/org/sat4j/tools/PrefboneTest.java @@ -0,0 +1,134 @@ +package org.sat4j.tools; + +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sat4j.minisat.SolverFactory; +import org.sat4j.minisat.core.Solver; +import org.sat4j.reader.DimacsReader; +import org.sat4j.reader.ParseFormatException; +import org.sat4j.reader.Reader; +import org.sat4j.specs.ContradictionException; +import org.sat4j.specs.IVecInt; +import org.sat4j.specs.TimeoutException; + +import java.io.IOException; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashSet; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; +import static org.junit.Assert.assertNotEquals; + +@RunWith(Parameterized.class) +public class PrefboneTest +{ + @Parameterized.Parameters + public static Collection testFiles() { + return Arrays.asList("src/test/testfiles/jnh/jnh218.cnf", + "src/test/testfiles/jnh/jnh209.cnf", + "src/test/testfiles/aim/aim-50-1_6-yes1-3.cnf", + "src/test/testfiles/aim/aim-50-1_6-yes1-2.cnf", + "src/test/testfiles/Eshop-fm.dimacs"); + } + + private final String myTestFile; + + public PrefboneTest(String file) + { + this.myTestFile = file; + } + + /** + * This test verifies that the implicantIntersection is always a subset + * of (or equal to) the prime implicant and the model for any SAT instance + */ + @Test + public void implicantIntersectionTest(){ + Solver sol = (Solver) SolverFactory.newDefault(); + Reader ried = new DimacsReader(sol); + try { + ried.parseInstance(this.myTestFile); + } catch (ParseFormatException | IOException | ContradictionException e) { + assertTrue("Failed to load file for implicant intersection test", + false); + } + //make sure the test doesnt take too long + sol.setTimeout(1); + + int[] mdl = null; + try { + mdl = sol.findModel(); + } catch (TimeoutException e) { + System.out.println("Skipped test for time constraints after 1 second"); + return; + } + assertNotEquals("Tested implicant intersection on unsatisfiable instance", + mdl,null); + int[] pi = sol.primeImplicant(); + + HashSet mdlhs = new HashSet<>(); + for (int ms : mdl) { + mdlhs.add(ms); + } + HashSet pihs = new HashSet<>(); + for (int p : pi) { + pihs.add(p); + } + + int[] implInters = sol.getImplicantIntersection(); + for (int ii : implInters) { + assertTrue(mdlhs.contains(ii)); + assertTrue(pihs.contains(ii)); + } + } + + + /** + * Verifies that the three available Backbone algorithms (BB,IBB and PBB) + * all calculate the same backbone for the same problem instance + */ + @Test + public void prefboneTest(){ + Backbone[] algorithmsToTest = new Backbone[]{ + Backbone.bb(), + Backbone.ibb(), + Backbone.pbb() + }; + HashSet knownBB = null; + for (Backbone bb : algorithmsToTest) { + Solver sol = (Solver) SolverFactory.newDefault(); + Reader ried = new DimacsReader(sol); + try { + ried.parseInstance(myTestFile); + } catch (ParseFormatException | IOException | ContradictionException e) { + assertTrue("Failed to load file for backbone test", + false); + } + IVecInt curBB; + try { + curBB = bb.compute(sol); + } catch (TimeoutException e) { + System.out.println("Skipped test for time constraints after 1 second"); + return; + } + //the result of the first algorithm (BB) is stored and later compared + // with the results of the other algorithms + if (knownBB == null) { + knownBB = new HashSet<>(); + for (int idx = 0; idx < curBB.size(); idx++) { + int curBBLit = curBB.get(idx); + knownBB.add(curBBLit); + } + } else { + //make sure that curBB matches knownBB + assertEquals(knownBB.size(), curBB.size()); + for (int idx = 0; idx < curBB.size(); idx++) { + int curBBLit = curBB.get(idx); + assertTrue(knownBB.contains(curBBLit)); + } + } + } + } +}