Skip to content

Commit

Permalink
MaxSATSolver.solve without handler can return the plain MaxSATResult
Browse files Browse the repository at this point in the history
  • Loading branch information
@SHildebrandt
SHildebrandt committed Aug 8, 2024
1 parent b333b63 commit 1e11c8b
Show file tree
Hide file tree
Showing 7 changed files with 45 additions and 51 deletions.
2 changes: 1 addition & 1 deletion src/main/java/com/booleworks/logicng/np/SetCover.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ public static <T> List<Set<T>> compute(final FormulaFactory f, final Collection<
for (final Variable setVar : setMap.keySet()) {
solver.addSoftFormula(setVar.negate(f), 1);
}
final MaxSATResult maxSATResult = solver.solve().getResult();
final MaxSATResult maxSATResult = solver.solve();
if (!maxSATResult.isSatisfiable()) {
throw new IllegalStateException("Internal optimization problem was not feasible.");
}
Expand Down
4 changes: 2 additions & 2 deletions src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -363,8 +363,8 @@ protected void addClause(final Formula formula, final int weight) {
* Solves the formula on the solver and returns the result.
* @return the result (SAT, UNSAT, Optimum found)
*/
public LNGResult<MaxSATResult> solve() {
return solve(NopHandler.get());
public MaxSATResult solve() {
return solve(NopHandler.get()).getResult();
}

/**
Expand Down
5 changes: 2 additions & 3 deletions src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -418,7 +418,7 @@ private int solveMaxSat(final List<Formula> formulas, final SortedSet<Variable>
final MaxSATSolver solver) {
formulas.forEach(solver::addHardFormula);
variables.forEach(v -> solver.addSoftFormula(v.negate(formulas.iterator().next().factory()), 1));
return solver.solve().getResult().getOptimum();
return solver.solve().getOptimum();
}

private SortedSet<Literal> satisfiedLiterals(final LNGResult<SatResult<Assignment>> assignment,
Expand Down Expand Up @@ -467,8 +467,7 @@ private void testOptimumModel(final Formula formula, final LNGResult<SatResult<A
final MaxSATSolver solver = MaxSATSolver.oll(f);
solver.addHardFormula(formula);
literals.forEach(l -> solver.addSoftFormula(maximize ? l : l.negate(f), 1));
final int numSatisfiedOll = satisfiedLiterals(
LNGResult.of(SatResult.sat(solver.solve().getResult().getModel())), literals).size();
final int numSatisfiedOll = satisfiedLiterals(LNGResult.of(SatResult.sat(solver.solve().getModel())), literals).size();
assertThat(actualNumSatisfied).isEqualTo(numSatisfiedOll);
}
} else {
Expand Down
7 changes: 1 addition & 6 deletions src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,6 @@

import com.booleworks.logicng.LongRunningTag;
import com.booleworks.logicng.formulas.FormulaFactory;
import com.booleworks.logicng.handlers.LNGResult;
import com.booleworks.logicng.solvers.MaxSATResult;
import com.booleworks.logicng.solvers.MaxSATSolver;
import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig;
import org.junit.jupiter.api.Test;
Expand All @@ -37,16 +35,13 @@ public void testWeightedMaxSat() throws IOException {
MaxSATSolver.incWBO(f, MaxSATConfig.builder().weight(MaxSATConfig.WeightStrategy.DIVERSIFY).build());
solvers[2] = MaxSATSolver.incWBO(f);
for (final MaxSATSolver solver : solvers) {
// final long start = System.currentTimeMillis();
for (final File file : Objects.requireNonNull(folder.listFiles())) {
if (file.getName().endsWith("wcnf")) {
solver.reset();
readCnfToSolver(solver, file.getAbsolutePath());
assertThat(solver.solve().getResult().getOptimum()).isEqualTo(result.get(file.getName()));
assertThat(solver.solve().getOptimum()).isEqualTo(result.get(file.getName()));
}
}
// final long stop = System.currentTimeMillis();
// System.out.printf("%-8s: %.2f sec%n", solver.getAlgorithm(), (stop - start) / 1000.0);
}
}

Expand Down
18 changes: 9 additions & 9 deletions src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ public void testWBO() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.wbo(f, config);
readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -92,7 +92,7 @@ public void testOLL() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.oll(f);
readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -107,7 +107,7 @@ public void testIncWBO() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.incWBO(f, config);
readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -129,7 +129,7 @@ public void testLinearSU() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.linearSU(f, config);
readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -153,7 +153,7 @@ public void testLinearUS() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.linearUS(f, config);
readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -176,7 +176,7 @@ public void testMSU3() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.msu3(f, config);
readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand Down Expand Up @@ -317,7 +317,7 @@ public void testNonClauselSoftConstraints() throws ParserException {
for (final MaxSATSolver solver : solvers) {
solver.addHardFormula(f.parse("a & b & c"));
solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getModel().literals()).containsExactlyInAnyOrder(
f.variable("a"), f.variable("b"), f.variable("c")
Expand All @@ -335,7 +335,7 @@ public void testSoftConstraintsCornerCaseVerum() throws ParserException {
solver.addHardFormula(f.parse("a & b & c"));
solver.addSoftFormula(f.parse("$true"), 1);
solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getModel().literals()).containsExactlyInAnyOrder(
f.variable("a"), f.variable("b"), f.variable("c")
Expand All @@ -353,7 +353,7 @@ public void testSoftConstraintsCornerCaseFalsum() throws ParserException {
solver.addHardFormula(f.parse("a & b & c"));
solver.addSoftFormula(f.parse("$false"), 1);
solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getModel().literals()).containsExactlyInAnyOrder(
f.variable("a"), f.variable("b"), f.variable("c")
Expand Down
28 changes: 14 additions & 14 deletions src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ public void testWBO() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.wbo(f, config);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -108,7 +108,7 @@ public void testIncWBO() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.incWBO(f, config);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -127,7 +127,7 @@ public void testLinearSU() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.linearSU(f, config);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -151,7 +151,7 @@ public void testWMSU3() throws IOException {
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.wmsu3(f, config);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -168,7 +168,7 @@ public void testWMSU3BMO() throws IOException {
for (int i = 0; i < bmoFiles.length; i++) {
final MaxSATSolver solver = MaxSATSolver.wmsu3(f, config);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/bmo/" + bmoFiles[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(bmoResults[i]);
}
Expand All @@ -186,7 +186,7 @@ public void testLineaerSUBMO() throws IOException {
for (int i = 0; i < bmoFiles.length; i++) {
final MaxSATSolver solver = MaxSATSolver.linearSU(f, config);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/bmo/" + bmoFiles[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(bmoResults[i]);
}
Expand All @@ -198,14 +198,14 @@ public void testOLL() throws IOException {
for (int i = 0; i < bmoFiles.length; i++) {
final MaxSATSolver solver = MaxSATSolver.oll(f);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/bmo/" + bmoFiles[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(bmoResults[i]);
}
for (int i = 0; i < files.length; i++) {
final MaxSATSolver solver = MaxSATSolver.oll(f);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(results[i]);
}
Expand All @@ -216,7 +216,7 @@ public void testOLL() throws IOException {
public void testLargeOLL1() throws IOException {
final MaxSATSolver solver = MaxSATSolver.oll(f);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/large/large_industrial.wcnf");
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(68974);
}
Expand All @@ -226,7 +226,7 @@ public void testLargeOLL1() throws IOException {
public void testLargeOLL2() throws IOException {
final MaxSATSolver solver = MaxSATSolver.oll(f);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/large/t3g3-5555.spn.wcnf");
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(1100610);
}
Expand All @@ -236,7 +236,7 @@ public void testLargeOLL2() throws IOException {
public void testOLLWithLargeWeights() throws IOException {
final MaxSATSolver solver = MaxSATSolver.oll(f);
readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/large/large_weights.wcnf");
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getOptimum()).isEqualTo(90912);
}
Expand Down Expand Up @@ -341,7 +341,7 @@ public void testWeightedNonClauseSoftConstraints() throws ParserException {
for (final MaxSATSolver solver : solvers) {
solver.addHardFormula(f.parse("a & b & c"));
solver.addSoftFormula(f.parse("~a & ~b & ~c"), 2);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getModel().literals()).containsExactlyInAnyOrder(
f.variable("a"), f.variable("b"), f.variable("c")
Expand All @@ -362,7 +362,7 @@ public void testWeightedSoftConstraintsCornerCaseVerum() throws ParserException
solver.addHardFormula(f.parse("a & b & c"));
solver.addSoftFormula(f.parse("$true"), 2);
solver.addSoftFormula(f.parse("~a & ~b & ~c"), 3);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getModel().literals()).containsExactlyInAnyOrder(
f.variable("a"), f.variable("b"), f.variable("c")
Expand All @@ -382,7 +382,7 @@ public void testWeightedSoftConstraintsCornerCaseFalsum() throws ParserException
solver.addHardFormula(f.parse("a & b & c"));
solver.addSoftFormula(f.parse("$false"), 2);
solver.addSoftFormula(f.parse("~a & ~b & ~c"), 3);
final MaxSATResult result = solver.solve().getResult();
final MaxSATResult result = solver.solve();
assertThat(result.isSatisfiable()).isTrue();
assertThat(result.getModel().literals()).containsExactlyInAnyOrder(
f.variable("a"), f.variable("b"), f.variable("c")
Expand Down
Loading

0 comments on commit 1e11c8b

Please sign in to comment.