Skip to content

Commit

Permalink
removed model and unsatCore methods from SATSolver
Browse files Browse the repository at this point in the history
  • Loading branch information
@SHildebrandt
SHildebrandt committed Apr 5, 2024
1 parent e7bd4e8 commit 6ad3802
Show file tree
Hide file tree
Showing 8 changed files with 71 additions and 107 deletions.
35 changes: 0 additions & 35 deletions src/main/java/com/booleworks/logicng/solvers/SATSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,9 @@
import com.booleworks.logicng.cardinalityconstraints.CCIncrementalData;
import com.booleworks.logicng.collections.LNGIntVector;
import com.booleworks.logicng.configurations.ConfigurationType;
import com.booleworks.logicng.datastructures.Assignment;
import com.booleworks.logicng.datastructures.EncodingResult;
import com.booleworks.logicng.datastructures.Model;
import com.booleworks.logicng.datastructures.Tristate;
import com.booleworks.logicng.explanations.UNSATCore;
import com.booleworks.logicng.formulas.CType;
import com.booleworks.logicng.formulas.CardinalityConstraint;
import com.booleworks.logicng.formulas.FType;
Expand Down Expand Up @@ -285,39 +283,6 @@ public boolean sat() {
}
}

/**
* Returns a model of the current formula on the solver wrt. a given set of variables.
* The variables must not be {@code null}.
* <p>
* If the formula is UNSAT, {@code null} will be returned.
* <p>
* This is a shortcut for {@code satCall().model()}.
* @param variables the set of variables
* @return a model of the current formula or {@code null} if the SAT call was unsatisfiable
*/
public Assignment model(final Collection<Variable> variables) {
try (final SATCall call = satCall().solve()) {
return call.model(variables);
}
}

/**
* Returns an unsat core of the current problem.
* <p>
* {@link SATSolverConfig#proofGeneration() Proof generation} must be enabled in order to use this method,
* otherwise an {@link IllegalStateException} is thrown.
* <p>
* If the formula on the solver is satisfiable, {@code null} is returned.
* <p>
* This is a shortcut for {@code satCall().unsatCore()}.
* @return the unsat core or {@code null} if the SAT call was satisfiable
*/
public UNSATCore<Proposition> unsatCore() {
try (final SATCall call = satCall().solve()) {
return call.unsatCore();
}
}

/**
* Executes a solver function on this solver.
* @param function the solver function
Expand Down
2 changes: 1 addition & 1 deletion src/test/java/com/booleworks/logicng/cardinalityconstraints/CCPerformanceTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ private void buildAMK(final FormulaFactory f, final int numLits, final boolean m
final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().useAtMostClauses(miniCard).build());
solver.add(cc);
assertSolverSat(solver);
final Assignment model = solver.model(Arrays.asList(problemLits));
final Assignment model = solver.satCall().model(Arrays.asList(problemLits));
assertThat(cc.evaluate(model)).isTrue();
}
}
Expand Down
34 changes: 17 additions & 17 deletions src/test/java/com/booleworks/logicng/explanations/drup/DRUPTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ public void testUnsatCoresFromDimacs() throws IOException {
final SATSolver solver = solverSupplier.get();
solver.add(cnf);
assertSolverUnsat(solver);
final UNSATCore<Proposition> unsatCore = solver.unsatCore();
final UNSATCore<Proposition> unsatCore = solver.satCall().unsatCore();
verifyCore(unsatCore, cnf);
}
}
Expand All @@ -69,7 +69,7 @@ public void testUnsatCoresFromLargeTestset() throws IOException {
final SATSolver solver = solverSupplier.get();
solver.add(cnf);
if (!solver.sat()) {
final UNSATCore<Proposition> unsatCore = solver.unsatCore();
final UNSATCore<Proposition> unsatCore = solver.satCall().unsatCore();
verifyCore(unsatCore, cnf);
count++;
}
Expand All @@ -91,7 +91,7 @@ public void testUnsatCoresAimTestset() throws IOException {
final SATSolver solver = solverSupplier.get();
solver.add(cnf);
assertSolverUnsat(solver);
final UNSATCore<Proposition> unsatCore = solver.unsatCore();
final UNSATCore<Proposition> unsatCore = solver.satCall().unsatCore();
verifyCore(unsatCore, cnf);
count++;
}
Expand All @@ -114,7 +114,7 @@ public void testPropositionHandling() throws ParserException {
final SATSolver solver = solverSupplier.get();
solver.addPropositions(propositions);
Assertions.assertThat(solver.sat()).isFalse();
final UNSATCore<Proposition> unsatCore = solver.unsatCore();
final UNSATCore<Proposition> unsatCore = solver.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(propositions.get(0), propositions.get(1),
propositions.get(2), propositions.get(3), propositions.get(4), propositions.get(5));
}
Expand All @@ -141,32 +141,32 @@ public void testPropositionIncDec() throws ParserException {
solver.addPropositions(p7, p8);

Assertions.assertThat(solver.sat()).isFalse();
UNSATCore<Proposition> unsatCore = solver.unsatCore();
UNSATCore<Proposition> unsatCore = solver.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p5, p6);

solver.loadState(state2);
Assertions.assertThat(solver.sat()).isFalse();
unsatCore = solver.unsatCore();
unsatCore = solver.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p5, p6);

solver.loadState(state1);
solver.add(p9);
Assertions.assertThat(solver.sat()).isFalse();
unsatCore = solver.unsatCore();
unsatCore = solver.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p9);

solver.loadState(state1);
solver.add(p5);
solver.add(p6);
Assertions.assertThat(solver.sat()).isFalse();
unsatCore = solver.unsatCore();
unsatCore = solver.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p3, p4, p5, p6);

solver.loadState(state1);
solver.add(p10);
solver.add(p11);
Assertions.assertThat(solver.sat()).isFalse();
unsatCore = solver.unsatCore();
unsatCore = solver.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p4, p11);
}

Expand All @@ -177,7 +177,7 @@ public void testTrivialCasesPropositions() throws ParserException {
final StandardProposition p1 = new StandardProposition("P1", f.parse("$false"));
solver1.add(p1);
assertSolverUnsat(solver1);
UNSATCore<Proposition> unsatCore = solver1.unsatCore();
UNSATCore<Proposition> unsatCore = solver1.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1);

final SATSolver solver2 = solverSupplier.get();
Expand All @@ -188,7 +188,7 @@ public void testTrivialCasesPropositions() throws ParserException {
final StandardProposition p3 = new StandardProposition("P3", f.parse("~a"));
solver2.add(p3);
assertSolverUnsat(solver2);
unsatCore = solver2.unsatCore();
unsatCore = solver2.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p2, p3);
}

Expand All @@ -213,7 +213,7 @@ public void testCoreAndAssumptions() throws ParserException {
solver.add(p5);
solver.add(p6);
solver.sat();
final UNSATCore<Proposition> unsatCore = solver.unsatCore();
final UNSATCore<Proposition> unsatCore = solver.satCall().unsatCore();
assertThat(unsatCore.propositions()).containsExactlyInAnyOrder(p1, p2, p5, p6);
}

Expand All @@ -230,7 +230,7 @@ public void testCoreAndAssumptions2() throws ParserException {

solver.add(f.parse("~A"));
solver.sat();
Assertions.assertThat(solver.unsatCore()).isNotNull();
Assertions.assertThat(solver.satCall().unsatCore()).isNotNull();
}

@Test
Expand All @@ -255,7 +255,7 @@ public void testCoreAndAssumptions3() throws ParserException {
solver.add(f.parse("X"));

solver.sat();
Assertions.assertThat(solver.unsatCore()).isNotNull();
Assertions.assertThat(solver.satCall().unsatCore()).isNotNull();
}

@Test
Expand All @@ -271,7 +271,7 @@ public void testCoreAndAssumptions4() throws ParserException {
solver.add(f.parse("L & A3 => A4"));
solver.add(f.parse("~A4"));
solver.add(f.parse("L | R"));
Assertions.assertThat(solver.unsatCore()).isNotNull();
Assertions.assertThat(solver.satCall().unsatCore()).isNotNull();
}

@Test
Expand All @@ -298,7 +298,7 @@ public void testWithCcPropositions() throws ParserException {
solver.add(p3);
solver.add(p4);
Assertions.assertThat(solver.sat()).isFalse();
Assertions.assertThat(solver.unsatCore().propositions()).containsExactlyInAnyOrder(p1, p2, p3);
Assertions.assertThat(solver.satCall().unsatCore().propositions()).containsExactlyInAnyOrder(p1, p2, p3);
}

@Test
Expand All @@ -320,7 +320,7 @@ public void testWithSpecialUnitCase() throws ParserException {
Assertions.assertThat(solver.sat()).isTrue();
solver.add(f.variable("a"));
Assertions.assertThat(solver.sat()).isFalse();
Assertions.assertThat(solver.unsatCore().propositions()).contains(p1, p2, p4, p5, p6, p7, p8, p9, p10, p11);
Assertions.assertThat(solver.satCall().unsatCore().propositions()).contains(p1, p2, p4, p5, p6, p7, p8, p9, p10, p11);
}

/**
Expand Down
2 changes: 1 addition & 1 deletion src/test/java/com/booleworks/logicng/pseudobooleans/PBSolvingTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -366,7 +366,7 @@ public void testLargePBs() {
final PBConstraint pbc = (PBConstraint) f.pbc(CType.GE, 5000, lits, coeffs);
solver.add(PBEncoder.encode(f, pbc, config));
assertSolverSat(solver);
assertThat(pbc.evaluate(solver.model(Arrays.asList(lits)))).isTrue();
assertThat(pbc.evaluate(solver.satCall().model(Arrays.asList(lits)))).isTrue();
}
}
}
Expand Down
5 changes: 2 additions & 3 deletions src/test/java/com/booleworks/logicng/solvers/functions/UnsatCoreFunctionTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,10 @@ public class UnsatCoreFunctionTest extends TestWithExampleFormulas {
public void testExceptionalBehavior() {
assertThatThrownBy(() -> {
final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(false).build());
solver.unsatCore();
solver.satCall().unsatCore();
}).isInstanceOf(IllegalStateException.class)
.hasMessage("Cannot generate an unsat core if proof generation is not turned on");

assertThat(SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(true).build()).unsatCore()).isNull();
// TODO test null if solver result is UNDEF because handler aborted
assertThat(SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(true).build()).satCall().unsatCore()).isNull();
}
}
24 changes: 12 additions & 12 deletions src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,21 +47,21 @@ public static Collection<Arguments> solverSuppliers() {
public void testNoModel(final Supplier<SATSolver> solverSupplier, final String solverDescription) throws ParserException {
SATSolver solver = solverSupplier.get();
solver.add(f.falsum());
assertThat(solver.model(f.variables())).isNull();
assertThat(solver.satCall().model(f.variables())).isNull();
solver = solverSupplier.get();
solver.add(f.parse("A & ~A"));
assertThat(solver.model(f.variables("A"))).isNull();
assertThat(solver.satCall().model(f.variables("A"))).isNull();
solver = solverSupplier.get();
solver.add(f.parse("(A => (B & C)) & A & C & (C <=> ~B)"));
assertThat(solver.model(f.variables("A", "B", "C"))).isNull();
assertThat(solver.satCall().model(f.variables("A", "B", "C"))).isNull();
}

@ParameterizedTest(name = "{index} {1}")
@MethodSource("solverSuppliers")
public void testEmptyModel(final Supplier<SATSolver> solverSupplier, final String solverDescription) {
final SATSolver solver = solverSupplier.get();
solver.add(f.verum());
final Assignment model = solver.model(f.variables());
final Assignment model = solver.satCall().model(f.variables());
assertThat(model.literals()).isEmpty();
assertThat(model.blockingClause(f)).isEqualTo(f.falsum());
assertThat(solver.enumerateAllModels(List.of())).hasSize(1);
Expand All @@ -72,12 +72,12 @@ public void testEmptyModel(final Supplier<SATSolver> solverSupplier, final Strin
public void testSimpleModel(final Supplier<SATSolver> solverSupplier, final String solverDescription) {
SATSolver solver = solverSupplier.get();
solver.add(f.literal("A", true));
Assignment model = solver.model(f.variables("A"));
Assignment model = solver.satCall().model(f.variables("A"));
assertThat(model.literals()).containsExactly(f.literal("A", true));
assertThat(solver.enumerateAllModels(f.variables("A"))).hasSize(1);
solver = solverSupplier.get();
solver.add(f.literal("A", false));
model = solver.model(f.variables("A"));
model = solver.satCall().model(f.variables("A"));
assertThat(model.literals()).containsExactly(f.literal("A", false));
assertThat(solver.enumerateAllModels(f.variables("A"))).hasSize(1);
}
Expand All @@ -88,7 +88,7 @@ public void testCNFFormula(final Supplier<SATSolver> solverSupplier, final Strin
final SATSolver solver = solverSupplier.get();
final Formula formula = f.parse("(A|B|C) & (~A|~B|~C) & (A|~B|~C) & (~A|~B|C)");
solver.add(formula);
final Assignment model = solver.model(f.variables("A", "B", "C"));
final Assignment model = solver.satCall().model(f.variables("A", "B", "C"));
assertThat(formula.evaluate(model)).isTrue();
assertThat(solver.enumerateAllModels(f.variables("A", "B", "C"))).hasSize(4);
for (final Model m : solver.enumerateAllModels(f.variables("A", "B", "C"))) {
Expand All @@ -103,7 +103,7 @@ public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final Supplier<SATSolve
final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F");
final Formula cnf = formula.transform(new TseitinTransformation(solver.factory(), 0));
solver.add(cnf);
final Assignment model = solver.model(formula.variables(f));
final Assignment model = solver.satCall().model(formula.variables(f));
assertThat(formula.evaluate(model)).isTrue();
final List<Model> allModels = solver.enumerateAllModels(formula.variables(f));
assertThat(allModels).hasSize(4);
Expand All @@ -120,7 +120,7 @@ public void testNonCNFAllVars(final Supplier<SATSolver> solverSupplier, final St
final SATSolver solver = solverSupplier.get();
final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F");
solver.add(formula);
final Assignment model = solver.model(formula.variables(f));
final Assignment model = solver.satCall().model(formula.variables(f));
assertThat(formula.evaluate(model)).isTrue();
final List<Model> allModels = solver.enumerateAllModels(formula.variables(f));
assertThat(allModels).hasSize(4);
Expand All @@ -136,7 +136,7 @@ public void testNonCNFOnlyFormulaVars(final Supplier<SATSolver> solverSupplier,
final SATSolver solver = solverSupplier.get();
final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F");
solver.add(formula);
final Assignment model = solver.model(formula.variables(f));
final Assignment model = solver.satCall().model(formula.variables(f));
assertThat(formula.evaluate(model)).isTrue();
assertThat(model.formula(f).variables(f)).isEqualTo(formula.variables(f));
final List<Model> allModels = solver.enumerateAllModels(formula.variables(f));
Expand All @@ -156,7 +156,7 @@ public void testNonCNFRestrictedVars(final Supplier<SATSolver> solverSupplier, f
verificationSolver.add(formula);
solverForMe.add(formula);
final SortedSet<Variable> relevantVariables = new TreeSet<>(Arrays.asList(f.variable("A"), f.variable("B"), f.variable("C")));
final Assignment model = solverForMe.model(relevantVariables);
final Assignment model = solverForMe.satCall().model(relevantVariables);
assertThat(verificationSolver.satCall().addFormulas(model.literals()).sat()).isEqualTo(Tristate.TRUE);
assertThat(model.formula(f).variables(f)).isEqualTo(relevantVariables);
final List<Model> allModels = solverForMe.enumerateAllModels(relevantVariables);
Expand All @@ -179,7 +179,7 @@ public void testNonCNFRestrictedAndAdditionalVars(final Supplier<SATSolver> solv
final SortedSet<Variable> additionalVariables = new TreeSet<>(Arrays.asList(f.variable("D"), f.variable("X"), f.variable("Y")));
final SortedSet<Variable> allVariables = new TreeSet<>(relevantVariables);
allVariables.addAll(additionalVariables);
final Assignment model = solverForMe.model(additionalVariables);
final Assignment model = solverForMe.satCall().model(additionalVariables);
assertThat(verificationSolver.satCall().addFormulas(model.literals()).sat()).isEqualTo(Tristate.TRUE);
assertThat(model.formula(f).variables(f)).containsExactlyInAnyOrder(f.variable("D"), f.variable("X"), f.variable("Y"));
final ModelEnumerationFunction me = ModelEnumerationFunction.builder(relevantVariables)
Expand Down
Loading

0 comments on commit 6ad3802

Please sign in to comment.