From 1c4033428e6e8ec08d9f28af11490b107f2826f5 Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Thu, 29 Aug 2024 09:35:39 +0200 Subject: [PATCH] replace Assignment with Model in several places --- .../logicng/datastructures/Assignment.java | 44 ----- .../logicng/datastructures/Model.java | 40 ++++ .../explanations/smus/SmusComputation.java | 6 +- .../MinimumPrimeImplicantFunction.java | 4 +- .../OptimizationFoundBetterBoundEvent.java | 8 +- .../knowledgecompilation/bdds/BDD.java | 51 +++-- .../primecomputation/NaivePrimeReduction.java | 3 +- .../primecomputation/PrimeCompiler.java | 24 +-- .../logicng/solvers/MaxSATResult.java | 10 +- .../logicng/solvers/MaxSATSolver.java | 22 +-- .../functions/OptimizationFunction.java | 14 +- .../solvers/maxsat/InternalMaxSATResult.java | 4 +- .../logicng/solvers/sat/SATCall.java | 5 +- .../logicng/solvers/sat/SATCallBuilder.java | 4 +- .../datastructures/AssignmentTest.java | 20 -- .../logicng/datastructures/ModelTest.java | 19 ++ .../logicng/encodings/CcPerformanceTest.java | 5 +- .../logicng/encodings/PbSolvingTest.java | 174 ++++++++--------- .../TimeoutModelEnumerationHandlerTest.java | 4 +- .../TimeoutOptimizationHandlerTest.java | 10 +- .../bdds/BDDOperationsTest.java | 104 +++++----- .../bdds/LargeBDDTest.java | 1 - .../PrimeImplicantReductionTest.java | 2 +- .../PrimeImplicateReductionTest.java | 3 +- .../functions/OptimizationFunctionTest.java | 179 +++++++++--------- .../solvers/maxsat/PartialMaxSATTest.java | 6 +- .../maxsat/PartialWeightedMaxSATTest.java | 6 +- .../solvers/maxsat/PureMaxSATTest.java | 6 +- .../logicng/solvers/sat/ModelTest.java | 88 +++++---- .../logicng/solvers/sat/SATCallTest.java | 21 +- .../logicng/solvers/sat/SATTest.java | 147 +++++++------- .../logicng/solvers/sat/SolverTestSet.java | 19 +- 32 files changed, 538 insertions(+), 515 deletions(-) diff --git a/src/main/java/com/booleworks/logicng/datastructures/Assignment.java b/src/main/java/com/booleworks/logicng/datastructures/Assignment.java index 006b475f..ea90117a 100644 --- a/src/main/java/com/booleworks/logicng/datastructures/Assignment.java +++ b/src/main/java/com/booleworks/logicng/datastructures/Assignment.java @@ -9,10 +9,8 @@ import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.Variable; -import java.util.ArrayList; import java.util.Collection; import java.util.Collections; -import java.util.List; import java.util.Objects; import java.util.SortedSet; import java.util.TreeSet; @@ -31,7 +29,6 @@ * @version 3.0.0 * @since 1.0 */ - public final class Assignment { private final SortedSet pos = new TreeSet<>(); @@ -187,47 +184,6 @@ public Model model() { return new Model(this); } - /** - * Creates the blocking clause for this assignment. - * @param f the formula factory - * @return the blocking clause for this assignment - */ - public Formula blockingClause(final FormulaFactory f) { - final List ops = new ArrayList<>(); - for (final Literal lit : pos) { - ops.add(lit.negate(f)); - } - for (final Literal lit : neg) { - ops.add(lit.negate(f)); - } - return f.or(ops); - } - - /** - * Creates the blocking clause for this assignment wrt. a given set of - * literals. If the set is {@code null}, all literals are considered - * relevant. - * @param f the formula factory - * @param literals the set of literals - * @return the blocking clause for this assignment - */ - public Formula blockingClause(final FormulaFactory f, final Collection literals) { - if (literals == null) { - return blockingClause(f); - } - final List ops = new ArrayList<>(); - for (final Literal lit : literals) { - final Variable var = lit.variable(); - final Literal negatedVar = var.negate(f); - if (pos.contains(var)) { - ops.add(negatedVar); - } else if (neg.contains(negatedVar)) { - ops.add(var); - } - } - return f.or(ops); - } - @Override public int hashCode() { return Objects.hash(pos, neg); diff --git a/src/main/java/com/booleworks/logicng/datastructures/Model.java b/src/main/java/com/booleworks/logicng/datastructures/Model.java index 9e8c08bc..427b8263 100644 --- a/src/main/java/com/booleworks/logicng/datastructures/Model.java +++ b/src/main/java/com/booleworks/logicng/datastructures/Model.java @@ -11,9 +11,12 @@ import java.util.ArrayList; import java.util.Arrays; +import java.util.Collection; import java.util.Collections; +import java.util.HashSet; import java.util.List; import java.util.Objects; +import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; @@ -136,6 +139,43 @@ public SortedSet negativeVariables() { return set; } + /** + * Creates the blocking clause for this model. + * @param f the formula factory + * @return the blocking clause for this model + */ + public Formula blockingClause(final FormulaFactory f) { + final List ops = new ArrayList<>(); + for (final Literal lit : literals) { + ops.add(lit.negate(f)); + } + return f.or(ops); + } + + /** + * Creates the blocking clause for this model wrt. a given set of + * literals. If the set is {@code null}, all literals are considered + * relevant. + * @param f the formula factory + * @param literals the set of literals + * @return the blocking clause for this model + */ + public Formula blockingClause(final FormulaFactory f, final Collection literals) { + if (literals == null) { + return blockingClause(f); + } + final Set myLiterals = new HashSet<>(this.literals); + final List ops = new ArrayList<>(); + for (final Literal lit : literals) { + if (myLiterals.contains(lit)) { + ops.add(lit.negate(f)); + } else if (myLiterals.contains(lit.negate(f))) { + ops.add(lit); + } + } + return f.or(ops); + } + @Override public boolean equals(final Object o) { if (this == o) { diff --git a/src/main/java/com/booleworks/logicng/explanations/smus/SmusComputation.java b/src/main/java/com/booleworks/logicng/explanations/smus/SmusComputation.java index e99f683e..1aadf4a7 100644 --- a/src/main/java/com/booleworks/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/com/booleworks/logicng/explanations/smus/SmusComputation.java @@ -6,7 +6,7 @@ import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.SMUS_COMPUTATION_STARTED; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Variable; @@ -158,7 +158,7 @@ public static LNGResult> computeSmusForFormulas( private static LNGResult> minimumHs(final SATSolver hSolver, final Set variables, final ComputationHandler handler) { - final LNGResult minimumHsModel = hSolver.execute(OptimizationFunction.builder() + final LNGResult minimumHsModel = hSolver.execute(OptimizationFunction.builder() .literals(variables) .minimize().build(), handler); if (!minimumHsModel.isSuccess()) { @@ -176,7 +176,7 @@ private static LNGResult> grow(final SATSolver growSolver, f if (!growSolver.sat()) { return null; } - final LNGResult maxModel = growSolver.execute(OptimizationFunction.builder() + final LNGResult maxModel = growSolver.execute(OptimizationFunction.builder() .literals(variables) .maximize().build(), handler); if (!maxModel.isSuccess()) { diff --git a/src/main/java/com/booleworks/logicng/functions/MinimumPrimeImplicantFunction.java b/src/main/java/com/booleworks/logicng/functions/MinimumPrimeImplicantFunction.java index 4c7a02b6..a7cacfb1 100644 --- a/src/main/java/com/booleworks/logicng/functions/MinimumPrimeImplicantFunction.java +++ b/src/main/java/com/booleworks/logicng/functions/MinimumPrimeImplicantFunction.java @@ -4,7 +4,7 @@ package com.booleworks.logicng.functions; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.FormulaFunction; @@ -62,7 +62,7 @@ public LNGResult> apply(final Formula formula, final Computat throw new IllegalArgumentException("The given formula must be satisfiable"); } - final LNGResult minimumModel = + final LNGResult minimumModel = solver.execute(OptimizationFunction.minimize(newVar2oldLit.keySet()), handler); if (!minimumModel.isSuccess()) { return LNGResult.canceled(minimumModel.getCancelCause()); diff --git a/src/main/java/com/booleworks/logicng/handlers/events/OptimizationFoundBetterBoundEvent.java b/src/main/java/com/booleworks/logicng/handlers/events/OptimizationFoundBetterBoundEvent.java index b7e3f264..153da898 100644 --- a/src/main/java/com/booleworks/logicng/handlers/events/OptimizationFoundBetterBoundEvent.java +++ b/src/main/java/com/booleworks/logicng/handlers/events/OptimizationFoundBetterBoundEvent.java @@ -1,6 +1,6 @@ package com.booleworks.logicng.handlers.events; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.solvers.functions.OptimizationFunction; import java.util.function.Supplier; @@ -13,13 +13,13 @@ */ public class OptimizationFoundBetterBoundEvent implements LNGEvent { - private final Supplier model; + private final Supplier model; /** * Creates a new event including a supplier to get the latest model. * @param model the latest model */ - public OptimizationFoundBetterBoundEvent(final Supplier model) { + public OptimizationFoundBetterBoundEvent(final Supplier model) { this.model = model; } @@ -27,7 +27,7 @@ public OptimizationFoundBetterBoundEvent(final Supplier model) { * Returns the supplier for the latest model. * @return the supplier for the latest model */ - public Supplier getModel() { + public Supplier getModel() { return model; } diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDD.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDD.java index 412d33ae..d28cc5f4 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDD.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDD.java @@ -4,7 +4,6 @@ package com.booleworks.logicng.knowledgecompilation.bdds; -import com.booleworks.logicng.datastructures.Assignment; import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; @@ -114,7 +113,7 @@ public Formula toFormula(final FormulaFactory f) { * formula. If {@code followPathsToTrue} is deactivated, the paths leading * to the {@code false} terminal are followed to generate the formula and * the resulting formula is negated. Depending on the formula and the number - * of satisfying assignments, the generated formula can be more compact + * of satisfying models, the generated formula can be more compact * using the {@code true} paths or {@code false} paths, respectively. * @param followPathsToTrue the extraction style * @return the formula for this BDD @@ -130,7 +129,7 @@ public Formula toFormula(final boolean followPathsToTrue) { * formula. If {@code followPathsToTrue} is deactivated, the paths leading * to the {@code false} terminal are followed to generate the formula and * the resulting formula is negated. Depending on the formula and the number - * of satisfying assignments, the generated formula can be more compact + * of satisfying models, the generated formula can be more compact * using the {@code true} paths or {@code false} paths, respectively. * @param f the formula factory to generate new formulas * @param followPathsToTrue the extraction style @@ -407,8 +406,8 @@ public BDD forall(final Variable... variables) { * Returns an arbitrary model of this BDD or {@code null} if there is none. * @return an arbitrary model of this BDD */ - public Assignment model() { - return createAssignment(kernel.factory(), operations.satOne(index)); + public Model model() { + return createModel(kernel.factory(), operations.satOne(index)); } /** @@ -416,8 +415,8 @@ public Assignment model() { * @param f the formula factory to generate new formulas * @return an arbitrary model of this BDD */ - public Assignment model(final FormulaFactory f) { - return createAssignment(f, operations.satOne(index)); + public Model model(final FormulaFactory f) { + return createModel(f, operations.satOne(index)); } /** @@ -429,7 +428,7 @@ public Assignment model(final FormulaFactory f) { * model * @return an arbitrary model of this BDD */ - public Assignment model(final boolean defaultValue, final Collection variables) { + public Model model(final boolean defaultValue, final Collection variables) { return model(kernel.factory(), defaultValue, variables); } @@ -443,11 +442,11 @@ public Assignment model(final boolean defaultValue, final Collection v * model * @return an arbitrary model of this BDD */ - public Assignment model(final FormulaFactory f, final boolean defaultValue, final Collection variables) { + public Model model(final FormulaFactory f, final boolean defaultValue, final Collection variables) { final int varBDD = BDDFactory.build(variables, kernel).index; final int pol = defaultValue ? BDDKernel.BDD_TRUE : BDDKernel.BDD_FALSE; final int modelBDD = operations.satOneSet(index, varBDD, pol); - return createAssignment(f, modelBDD); + return createModel(f, modelBDD); } /** @@ -459,7 +458,7 @@ public Assignment model(final FormulaFactory f, final boolean defaultValue, fina * model * @return an arbitrary model of this BDD */ - public Assignment model(final boolean defaultValue, final Variable... variables) { + public Model model(final boolean defaultValue, final Variable... variables) { return model(kernel.factory(), defaultValue, Arrays.asList(variables)); } @@ -473,7 +472,7 @@ public Assignment model(final boolean defaultValue, final Variable... variables) * model * @return an arbitrary model of this BDD */ - public Assignment model(final FormulaFactory f, final boolean defaultValue, final Variable... variables) { + public Model model(final FormulaFactory f, final boolean defaultValue, final Variable... variables) { return model(f, defaultValue, Arrays.asList(variables)); } @@ -481,7 +480,7 @@ public Assignment model(final FormulaFactory f, final boolean defaultValue, fina * Returns a full model of this BDD or {@code null} if there is none. * @return a full model of this BDD */ - public Assignment fullModel() { + public Model fullModel() { return fullModel(kernel.factory()); } @@ -490,8 +489,8 @@ public Assignment fullModel() { * @param f the formula factory to generate new formulas * @return a full model of this BDD */ - public Assignment fullModel(final FormulaFactory f) { - return createAssignment(f, operations.fullSatOne(index)); + public Model fullModel(final FormulaFactory f) { + return createModel(f, operations.fullSatOne(index)); } /** @@ -517,9 +516,9 @@ public BigInteger pathCountZero() { public SortedSet support() { final int supportBDD = operations.support(index); // only variables, cannot create new literals - final Assignment assignment = createAssignment(kernel.factory(), supportBDD); - assert assignment == null || assignment.negativeLiterals().isEmpty(); - return assignment == null ? Collections.emptySortedSet() : new TreeSet<>(assignment.positiveVariables()); + final Model model = createModel(kernel.factory(), supportBDD); + assert model == null || model.negativeLiterals().isEmpty(); + return model == null ? Collections.emptySortedSet() : new TreeSet<>(model.positiveVariables()); } /** @@ -590,33 +589,33 @@ public BDDNode toLngBdd() { } /** - * Creates an assignment from a BDD. + * Creates an model from a BDD. * @param f the formula factory to generate new formulas * @param modelBDD the BDD - * @return the assignment + * @return the model * @throws IllegalStateException if the BDD does not represent a unique * model */ - private Assignment createAssignment(final FormulaFactory f, final int modelBDD) { + private Model createModel(final FormulaFactory f, final int modelBDD) { if (modelBDD == BDDKernel.BDD_FALSE) { return null; } if (modelBDD == BDDKernel.BDD_TRUE) { - return new Assignment(); + return new Model(); } final List nodes = operations.allNodes(modelBDD); - final Assignment assignment = new Assignment(); + final List model = new ArrayList<>(); for (final int[] node : nodes) { final Variable variable = kernel.getVariableForIndex(node[1]); if (node[2] == BDDKernel.BDD_FALSE) { - assignment.addLiteral(variable); + model.add(variable); } else if (node[3] == BDDKernel.BDD_FALSE) { - assignment.addLiteral(variable.negate(f)); + model.add(variable.negate(f)); } else { throw new IllegalStateException("Expected that the model BDD has one unique path through the BDD."); } } - return assignment; + return new Model(model); } @Override diff --git a/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java b/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java index c38c4021..6c1d92fd 100644 --- a/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java +++ b/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java @@ -16,6 +16,7 @@ import com.booleworks.logicng.util.FormulaHelper; import java.util.ArrayList; +import java.util.Collection; import java.util.List; import java.util.SortedSet; import java.util.TreeSet; @@ -67,7 +68,7 @@ public SortedSet reduceImplicant(final SortedSet implicant) { * @return a prime implicant or null if the computation was canceled by the * handler */ - public LNGResult> reduceImplicant(final SortedSet implicant, + public LNGResult> reduceImplicant(final Collection implicant, final ComputationHandler handler) { handler.shouldResume(ComputationStartedEvent.IMPLICATE_REDUCTION_STARTED); final SortedSet primeImplicant = new TreeSet<>(implicant); diff --git a/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java b/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java index df57d3e5..09b5425b 100644 --- a/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java @@ -4,7 +4,7 @@ package com.booleworks.logicng.primecomputation; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Literal; @@ -138,22 +138,22 @@ private LNGResult>, List>>> comp if (!hSolver.sat()) { return LNGResult.of(new Pair<>(primeImplicants, primeImplicates)); } - final LNGResult hModelResult = hSolver.execute(computeWithMaximization + final LNGResult hModelResult = hSolver.execute(computeWithMaximization ? OptimizationFunction.builder().literals(sub.newVar2oldLit.keySet()).maximize().build() : OptimizationFunction.builder().literals(sub.newVar2oldLit.keySet()).minimize().build(), handler); if (!hModelResult.isSuccess()) { return LNGResult.canceled(hModelResult.getCancelCause()); } - final Assignment hModel = hModelResult.getResult(); - final Assignment fModel = transformModel(hModel, sub.newVar2oldLit); - try (final SATCall fCall = fSolver.satCall().handler(handler).addFormulas(fModel.literals()).solve()) { + final Model hModel = hModelResult.getResult(); + final Model fModel = transformModel(hModel, sub.newVar2oldLit); + try (final SATCall fCall = fSolver.satCall().handler(handler).addFormulas(fModel.getLiterals()).solve()) { if (!fCall.getSatResult().isSuccess()) { return LNGResult.canceled(fCall.getSatResult().getCancelCause()); } if (!fCall.getSatResult().getResult()) { final LNGResult> primeImplicantResult = computeWithMaximization - ? primeReduction.reduceImplicant(fModel.literals(), handler) - : LNGResult.of(fModel.literals()); + ? primeReduction.reduceImplicant(fModel.getLiterals(), handler) + : LNGResult.of(new TreeSet<>(fModel.getLiterals())); if (!primeImplicantResult.isSuccess()) { return LNGResult.canceled(primeImplicantResult.getCancelCause()); } @@ -167,7 +167,7 @@ private LNGResult>, List>>> comp } else { final SortedSet implicate = new TreeSet<>(); for (final Literal lit : - (computeWithMaximization ? fModel : fCall.model(formula.variables(f))).literals()) { + (computeWithMaximization ? fModel : fCall.model(formula.variables(f))).getLiterals()) { implicate.add(lit.negate(f)); } final LNGResult> primeImplicateResult = @@ -200,12 +200,12 @@ private SubstitutionResult createSubstitution(final FormulaFactory f, final Form return new SubstitutionResult(newVar2oldLit, substTransformation, f.and(constraintOps)); } - private Assignment transformModel(final Assignment model, final Map mapping) { - final Assignment mapped = new Assignment(); + private Model transformModel(final Model model, final Map mapping) { + final List mapped = new ArrayList<>(); for (final Variable var : model.positiveVariables()) { - mapped.addLiteral(mapping.get(var)); + mapped.add(mapping.get(var)); } - return mapped; + return new Model(mapped); } private List> negateAll(final FormulaFactory f, diff --git a/src/main/java/com/booleworks/logicng/solvers/MaxSATResult.java b/src/main/java/com/booleworks/logicng/solvers/MaxSATResult.java index 74ef354a..8915cdd0 100644 --- a/src/main/java/com/booleworks/logicng/solvers/MaxSATResult.java +++ b/src/main/java/com/booleworks/logicng/solvers/MaxSATResult.java @@ -1,6 +1,6 @@ package com.booleworks.logicng.solvers; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import java.util.Objects; @@ -18,7 +18,7 @@ public class MaxSATResult { private final boolean satisfiable; private final int optimum; - private final Assignment model; + private final Model model; /** * Creates a new MaxSATResult with the given parameters. @@ -26,7 +26,7 @@ public class MaxSATResult { * @param optimum the optimum value * @param model the model for optimum solution */ - private MaxSATResult(final boolean satisfiable, final int optimum, final Assignment model) { + private MaxSATResult(final boolean satisfiable, final int optimum, final Model model) { this.satisfiable = satisfiable; this.optimum = optimum; this.model = model; @@ -47,7 +47,7 @@ public static MaxSATResult unsatisfiable() { * @param model the model for the optimum solution * @return the result */ - public static MaxSATResult optimum(final int optimum, final Assignment model) { + public static MaxSATResult optimum(final int optimum, final Model model) { return new MaxSATResult(true, optimum, model); } @@ -74,7 +74,7 @@ public int getOptimum() { * not satisfiable. * @return the optimum model */ - public Assignment getModel() { + public Model getModel() { return model; } diff --git a/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java b/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java index 1bba35b8..15d54bab 100644 --- a/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java @@ -7,7 +7,7 @@ import com.booleworks.logicng.collections.LNGBooleanVector; import com.booleworks.logicng.collections.LNGIntVector; import com.booleworks.logicng.configurations.ConfigurationType; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Literal; @@ -26,6 +26,8 @@ import com.booleworks.logicng.solvers.maxsat.algorithms.WBO; import com.booleworks.logicng.solvers.maxsat.algorithms.WMSU3; +import java.util.ArrayList; +import java.util.List; import java.util.SortedMap; import java.util.SortedSet; import java.util.TreeMap; @@ -383,28 +385,24 @@ public LNGResult solve(final ComputationHandler handler) { solver.setProblemType(MaxSAT.ProblemType.WEIGHTED); } final LNGResult internalResult = solver.search(handler); - result = internalResult.map(res -> res.toMaxSATResult(this::createAssignment)); + result = internalResult.map(res -> res.toMaxSATResult(this::createModel)); return result; } /** - * Creates an assignment from a Boolean vector of the solver. + * Creates a model from a Boolean vector of the solver. * @param vec the vector of the solver - * @return the assignment + * @return the model */ - protected Assignment createAssignment(final LNGBooleanVector vec) { - final Assignment model = new Assignment(); + protected Model createModel(final LNGBooleanVector vec) { + final List model = new ArrayList<>(); for (int i = 0; i < vec.size(); i++) { final Literal lit = index2var.get(i); if (lit != null && !selectorVariables.contains(lit.variable())) { - if (vec.get(i)) { - model.addLiteral(lit); - } else { - model.addLiteral(lit.negate(f)); - } + model.add(vec.get(i) ? lit : lit.negate(f)); } } - return model; + return new Model(model); } /** diff --git a/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java b/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java index fea18365..509d1555 100644 --- a/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java +++ b/src/main/java/com/booleworks/logicng/solvers/functions/OptimizationFunction.java @@ -6,7 +6,7 @@ import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.OPTIMIZATION_FUNCTION_STARTED; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.encodings.CcIncrementalData; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.CardinalityConstraint; @@ -40,7 +40,7 @@ * @version 2.1.0 * @since 2.0.0 */ -public final class OptimizationFunction implements SolverFunction { +public final class OptimizationFunction implements SolverFunction { private static final String SEL_PREFIX = "@SEL_OPT_"; @@ -87,15 +87,15 @@ public static OptimizationFunction minimize(final Collection } @Override - public LNGResult apply( + public LNGResult apply( final SATSolver solver, final ComputationHandler handler) { final SolverState initialState = solver.saveState(); - final LNGResult model = maximize(solver, handler); + final LNGResult model = maximize(solver, handler); solver.loadState(initialState); return model; } - private LNGResult maximize( + private LNGResult maximize( final SATSolver solver, final ComputationHandler handler) { if (!handler.shouldResume(OPTIMIZATION_FUNCTION_STARTED)) { return LNGResult.canceled(OPTIMIZATION_FUNCTION_STARTED); @@ -114,8 +114,8 @@ private LNGResult maximize( selectorMap.forEach((selVar, lit) -> solver.add(f.or(selVar.negate(f), lit.negate(f)))); selectorMap.forEach((selVar, lit) -> solver.add(f.or(lit, selVar))); } - Assignment lastResultModel; - Assignment currentSelectorModel; + Model lastResultModel; + Model currentSelectorModel; try (final SATCall satCall = solver.satCall().handler(handler).solve()) { if (!satCall.getSatResult().isSuccess()) { return LNGResult.canceled(satCall.getSatResult().getCancelCause()); diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/InternalMaxSATResult.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/InternalMaxSATResult.java index 6f5c5ccf..3daf6e91 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/InternalMaxSATResult.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/InternalMaxSATResult.java @@ -1,7 +1,7 @@ package com.booleworks.logicng.solvers.maxsat; import com.booleworks.logicng.collections.LNGBooleanVector; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.solvers.MaxSATResult; import java.util.Objects; @@ -51,7 +51,7 @@ public static InternalMaxSATResult optimum(final int optimum, final LNGBooleanVe * assignment * @return the converted result */ - public MaxSATResult toMaxSATResult(final Function modelConversion) { + public MaxSATResult toMaxSATResult(final Function modelConversion) { return satisfiable ? MaxSATResult.optimum(optimum, modelConversion.apply(model)) : MaxSATResult.unsatisfiable(); } diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java b/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java index 1094967a..edec44cf 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java @@ -5,6 +5,7 @@ import com.booleworks.logicng.collections.LNGIntVector; import com.booleworks.logicng.collections.LNGVector; import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.explanations.UNSATCore; import com.booleworks.logicng.formulas.FType; import com.booleworks.logicng.formulas.Literal; @@ -119,7 +120,7 @@ public LNGResult getSatResult() { * was unsatisfiable * @throws IllegalArgumentException if the given variables are {@code null} */ - public Assignment model(final Collection variables) { + public Model model(final Collection variables) { if (variables == null) { throw new IllegalArgumentException("The given variables must not be null."); } @@ -138,7 +139,7 @@ public Assignment model(final Collection variables) { } final List finalModel = solver.convertInternalModel(solver.model(), relevantIndices); finalModel.addAll(unknowns); - return new Assignment(finalModel); + return new Model(finalModel); } } diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/SATCallBuilder.java b/src/main/java/com/booleworks/logicng/solvers/sat/SATCallBuilder.java index e2db914f..b1aae2d0 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/SATCallBuilder.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/SATCallBuilder.java @@ -1,6 +1,6 @@ package com.booleworks.logicng.solvers.sat; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.explanations.UNSATCore; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.Literal; @@ -156,7 +156,7 @@ public LNGResult sat() { * was unsatisfiable * @throws IllegalArgumentException if the given variables are {@code null} */ - public Assignment model(final Collection variables) { + public Model model(final Collection variables) { try (final SATCall call = solve()) { return call.model(variables); } diff --git a/src/test/java/com/booleworks/logicng/datastructures/AssignmentTest.java b/src/test/java/com/booleworks/logicng/datastructures/AssignmentTest.java index daf79fc0..54c4aee4 100644 --- a/src/test/java/com/booleworks/logicng/datastructures/AssignmentTest.java +++ b/src/test/java/com/booleworks/logicng/datastructures/AssignmentTest.java @@ -59,26 +59,6 @@ public void testFormula(final FormulaContext _c) throws ParserException { .isEqualTo(_c.p.parse("a & b & ~x & ~y")); } - @ParameterizedTest - @MethodSource("contexts") - public void testBlockingClause(final FormulaContext _c) throws ParserException { - final Assignment ass = new Assignment(); - ass.addLiteral(_c.a); - ass.addLiteral(_c.b); - ass.addLiteral(_c.nx); - ass.addLiteral(_c.ny); - final Formula bc01 = ass.blockingClause(_c.f); - assertThat(bc01.containsVariable(_c.c)).isFalse(); - assertThat(bc01).isEqualTo(_c.f.parse("~a | ~b | x | y")); - final Formula bc02 = ass.blockingClause(_c.f, null); - assertThat(bc02.containsVariable(_c.c)).isFalse(); - assertThat(bc02).isEqualTo(_c.f.parse("~a | ~b | x | y")); - final List lits = Arrays.asList(_c.a, _c.x, _c.c); - final Formula bcProjected = ass.blockingClause(_c.f, lits); - assertThat(bcProjected.containsVariable(_c.c)).isFalse(); - assertThat(bcProjected).isEqualTo(_c.f.parse("~a | x")); - } - @Test public void testCreators() { assertThat(new Assignment(Arrays.asList(c.a, c.b, c.x, c.y))).isNotNull(); diff --git a/src/test/java/com/booleworks/logicng/datastructures/ModelTest.java b/src/test/java/com/booleworks/logicng/datastructures/ModelTest.java index 02e677d9..b2afd3e3 100644 --- a/src/test/java/com/booleworks/logicng/datastructures/ModelTest.java +++ b/src/test/java/com/booleworks/logicng/datastructures/ModelTest.java @@ -6,7 +6,9 @@ import static org.assertj.core.api.Assertions.assertThat; +import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaContext; +import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.TestWithFormulaContext; import com.booleworks.logicng.io.parsers.ParserException; import com.booleworks.logicng.io.parsers.PropositionalParser; @@ -15,6 +17,7 @@ import java.util.Arrays; import java.util.Collections; +import java.util.List; /** * Unit tests for the class {@link Model}. @@ -64,6 +67,22 @@ public void testFormula(final FormulaContext _c) throws ParserException { .isEqualTo(p.parse("a & b & ~x & ~y")); } + @ParameterizedTest + @MethodSource("contexts") + public void testBlockingClause(final FormulaContext _c) throws ParserException { + final Model ass = new Model(_c.a, _c.b, _c.nx, _c.ny); + final Formula bc01 = ass.blockingClause(_c.f); + assertThat(bc01.containsVariable(_c.c)).isFalse(); + assertThat(bc01).isEqualTo(_c.f.parse("~a | ~b | x | y")); + final Formula bc02 = ass.blockingClause(_c.f, null); + assertThat(bc02.containsVariable(_c.c)).isFalse(); + assertThat(bc02).isEqualTo(_c.f.parse("~a | ~b | x | y")); + final List lits = Arrays.asList(_c.a, _c.x, _c.c); + final Formula bcProjected = ass.blockingClause(_c.f, lits); + assertThat(bcProjected.containsVariable(_c.c)).isFalse(); + assertThat(bcProjected).isEqualTo(_c.f.parse("~a | x")); + } + @ParameterizedTest @MethodSource("contexts") public void testHashCode(final FormulaContext _c) { diff --git a/src/test/java/com/booleworks/logicng/encodings/CcPerformanceTest.java b/src/test/java/com/booleworks/logicng/encodings/CcPerformanceTest.java index 34d04a29..77a530d0 100644 --- a/src/test/java/com/booleworks/logicng/encodings/CcPerformanceTest.java +++ b/src/test/java/com/booleworks/logicng/encodings/CcPerformanceTest.java @@ -9,6 +9,7 @@ import com.booleworks.logicng.LogicNGTest; import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.CardinalityConstraint; import com.booleworks.logicng.formulas.FormulaFactory; @@ -59,8 +60,8 @@ private void buildAMK(final FormulaFactory f, final int numLits, final boolean m SATSolver.newSolver(f, SATSolverConfig.builder().useAtMostClauses(miniCard).build()); solver.add(cc); assertSolverSat(solver); - final Assignment model = solver.satCall().model(Arrays.asList(problemLits)); - assertThat(cc.evaluate(model)).isTrue(); + final Model model = solver.satCall().model(Arrays.asList(problemLits)); + assertThat(cc.evaluate(model.assignment())).isTrue(); } } } diff --git a/src/test/java/com/booleworks/logicng/encodings/PbSolvingTest.java b/src/test/java/com/booleworks/logicng/encodings/PbSolvingTest.java index 3cb28d89..a09d703a 100644 --- a/src/test/java/com/booleworks/logicng/encodings/PbSolvingTest.java +++ b/src/test/java/com/booleworks/logicng/encodings/PbSolvingTest.java @@ -21,7 +21,7 @@ import java.util.Arrays; import java.util.List; import java.util.Set; -import java.util.function.Supplier; +import java.util.function.Function; public class PbSolvingTest implements LogicNGTest { @@ -29,7 +29,7 @@ public class PbSolvingTest implements LogicNGTest { private final Variable[] literals100; private final Variable[] literals10; private final List solvers; - private final List> solverSuppliers; + private final List> solverSuppliers; private final EncoderConfig[] configs; @@ -44,7 +44,7 @@ public PbSolvingTest() { literals10[i] = f.variable("v" + i); } solvers = SolverTestSet.solverTestSet(Set.of(USE_AT_MOST_CLAUSES), f); - solverSuppliers = SolverTestSet.solverSupplierTestSet(Set.of(USE_AT_MOST_CLAUSES), f); + solverSuppliers = SolverTestSet.solverSupplierTestSet(Set.of(USE_AT_MOST_CLAUSES)); configs = new EncoderConfig[]{ EncoderConfig.builder().pbEncoding(EncoderConfig.PB_ENCODER.SWC).build(), EncoderConfig.builder().pbEncoding(EncoderConfig.PB_ENCODER.BINARY_MERGE).binaryMergeUseGAC(true) @@ -93,82 +93,82 @@ public void testCCEXO() { @Test public void testCCAMK() { - for (final Supplier solver : solverSuppliers) { - testCCAMK(solver.get(), 0, 1); - testCCAMK(solver.get(), 1, 11); - testCCAMK(solver.get(), 2, 56); - testCCAMK(solver.get(), 3, 176); - testCCAMK(solver.get(), 4, 386); - testCCAMK(solver.get(), 5, 638); - testCCAMK(solver.get(), 6, 848); - testCCAMK(solver.get(), 7, 968); - testCCAMK(solver.get(), 8, 1013); - testCCAMK(solver.get(), 9, 1023); + for (final Function solver : solverSuppliers) { + testCCAMK(solver.apply(f), 0, 1); + testCCAMK(solver.apply(f), 1, 11); + testCCAMK(solver.apply(f), 2, 56); + testCCAMK(solver.apply(f), 3, 176); + testCCAMK(solver.apply(f), 4, 386); + testCCAMK(solver.apply(f), 5, 638); + testCCAMK(solver.apply(f), 6, 848); + testCCAMK(solver.apply(f), 7, 968); + testCCAMK(solver.apply(f), 8, 1013); + testCCAMK(solver.apply(f), 9, 1023); } } @Test public void testCCLT() { - for (final Supplier solver : solverSuppliers) { - testCCLT(solver.get(), 1, 1); - testCCLT(solver.get(), 2, 11); - testCCLT(solver.get(), 3, 56); - testCCLT(solver.get(), 4, 176); - testCCLT(solver.get(), 5, 386); - testCCLT(solver.get(), 6, 638); - testCCLT(solver.get(), 7, 848); - testCCLT(solver.get(), 8, 968); - testCCLT(solver.get(), 9, 1013); - testCCLT(solver.get(), 10, 1023); + for (final Function solver : solverSuppliers) { + testCCLT(solver.apply(f), 1, 1); + testCCLT(solver.apply(f), 2, 11); + testCCLT(solver.apply(f), 3, 56); + testCCLT(solver.apply(f), 4, 176); + testCCLT(solver.apply(f), 5, 386); + testCCLT(solver.apply(f), 6, 638); + testCCLT(solver.apply(f), 7, 848); + testCCLT(solver.apply(f), 8, 968); + testCCLT(solver.apply(f), 9, 1013); + testCCLT(solver.apply(f), 10, 1023); } } @Test public void testCCALK() { - for (final Supplier solver : solverSuppliers) { - testCCALK(solver.get(), 1, 1023); - testCCALK(solver.get(), 2, 1013); - testCCALK(solver.get(), 3, 968); - testCCALK(solver.get(), 4, 848); - testCCALK(solver.get(), 5, 638); - testCCALK(solver.get(), 6, 386); - testCCALK(solver.get(), 7, 176); - testCCALK(solver.get(), 8, 56); - testCCALK(solver.get(), 9, 11); - testCCALK(solver.get(), 10, 1); + for (final Function solver : solverSuppliers) { + testCCALK(solver.apply(f), 1, 1023); + testCCALK(solver.apply(f), 2, 1013); + testCCALK(solver.apply(f), 3, 968); + testCCALK(solver.apply(f), 4, 848); + testCCALK(solver.apply(f), 5, 638); + testCCALK(solver.apply(f), 6, 386); + testCCALK(solver.apply(f), 7, 176); + testCCALK(solver.apply(f), 8, 56); + testCCALK(solver.apply(f), 9, 11); + testCCALK(solver.apply(f), 10, 1); } } @Test public void testCCGT() { - for (final Supplier solver : solverSuppliers) { - testCCGT(solver.get(), 0, 1023); - testCCGT(solver.get(), 1, 1013); - testCCGT(solver.get(), 2, 968); - testCCGT(solver.get(), 3, 848); - testCCGT(solver.get(), 4, 638); - testCCGT(solver.get(), 5, 386); - testCCGT(solver.get(), 6, 176); - testCCGT(solver.get(), 7, 56); - testCCGT(solver.get(), 8, 11); - testCCGT(solver.get(), 9, 1); + for (final Function solver : solverSuppliers) { + testCCGT(solver.apply(f), 0, 1023); + testCCGT(solver.apply(f), 1, 1013); + testCCGT(solver.apply(f), 2, 968); + testCCGT(solver.apply(f), 3, 848); + testCCGT(solver.apply(f), 4, 638); + testCCGT(solver.apply(f), 5, 386); + testCCGT(solver.apply(f), 6, 176); + testCCGT(solver.apply(f), 7, 56); + testCCGT(solver.apply(f), 8, 11); + testCCGT(solver.apply(f), 9, 1); } } @Test public void testCCEQ() { - for (final Supplier solver : solverSuppliers) { - testCCEQ(solver.get(), 0, 1); - testCCEQ(solver.get(), 1, 10); - testCCEQ(solver.get(), 2, 45); - testCCEQ(solver.get(), 3, 120); - testCCEQ(solver.get(), 4, 210); - testCCEQ(solver.get(), 5, 252); - testCCEQ(solver.get(), 6, 210); - testCCEQ(solver.get(), 7, 120); - testCCEQ(solver.get(), 8, 45); - testCCEQ(solver.get(), 9, 10); - testCCEQ(solver.get(), 10, 1); + for (final Function solver : solverSuppliers) { + testCCEQ(solver.apply(f), 0, 1); + testCCEQ(solver.apply(f), 1, 10); + testCCEQ(solver.apply(f), 2, 45); + testCCEQ(solver.apply(f), 3, 120); + testCCEQ(solver.apply(f), 4, 210); + testCCEQ(solver.apply(f), 5, 252); + testCCEQ(solver.apply(f), 6, 210); + testCCEQ(solver.apply(f), 7, 120); + testCCEQ(solver.apply(f), 8, 45); + testCCEQ(solver.apply(f), 9, 10); + testCCEQ(solver.apply(f), 10, 1); } } @@ -215,8 +215,8 @@ private void testCCEQ(final SATSolver solver, final int rhs, final int expected) @Test public void testPBEQ() { for (final EncoderConfig config : configs) { - for (final Supplier solverSupplier : solverSuppliers) { - SATSolver solver = solverSupplier.get(); + for (final Function solverSupplier : solverSuppliers) { + SATSolver solver = solverSupplier.apply(f); final int[] coeffs10 = new int[]{3, 2, 2, 2, 2, 2, 2, 2, 2, 2}; solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.EQ, 5, literals10, coeffs10), config)); assertSolverSat(solver); @@ -224,7 +224,7 @@ public void testPBEQ() { .hasSize(9) .allMatch(model -> model.positiveVariables().size() == 2) .allMatch(model -> model.positiveVariables().contains(f.variable("v" + 0))); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.EQ, 7, literals10, coeffs10), config)); assertSolverSat(solver); @@ -232,14 +232,14 @@ public void testPBEQ() { .hasSize(36) .allMatch(model -> model.positiveVariables().size() == 3) .allMatch(model -> model.positiveVariables().contains(f.variable("v" + 0))); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.EQ, 0, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(1); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.EQ, 1, literals10, coeffs10), config)); assertSolverUnsat(solver); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.EQ, 22, literals10, coeffs10), config)); assertSolverUnsat(solver); } @@ -249,33 +249,33 @@ public void testPBEQ() { @Test public void testPBLess() { for (final EncoderConfig config : configs) { - for (final Supplier solverSupplier : solverSuppliers) { - SATSolver solver = solverSupplier.get(); + for (final Function solverSupplier : solverSuppliers) { + SATSolver solver = solverSupplier.apply(f); final int[] coeffs10 = new int[]{3, 2, 2, 2, 2, 2, 2, 2, 2, 2}; solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.LE, 6, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)) .hasSize(140) .allMatch(model -> model.positiveVariables().size() <= 3); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.LT, 7, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)) .hasSize(140) .allMatch(model -> model.positiveVariables().size() <= 3); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.LE, 0, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(1); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.LE, 1, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(1); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.LT, 2, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(1); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.LT, 1, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(1); @@ -286,8 +286,8 @@ public void testPBLess() { @Test public void testPBGreater() { for (final EncoderConfig config : configs) { - for (final Supplier solverSupplier : solverSuppliers) { - SATSolver solver = solverSupplier.get(); + for (final Function solverSupplier : solverSuppliers) { + SATSolver solver = solverSupplier.apply(f); final int[] coeffs10 = new int[]{3, 2, 2, 2, 2, 2, 2, 2, 2, 2}; solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.GE, 17, literals10, coeffs10), config)); assertSolverSat(solver); @@ -295,20 +295,20 @@ public void testPBGreater() { assertThat(solver.enumerateAllModels(literals10)) .hasSize(47) .allMatch(model -> model.positiveVariables().size() >= 8); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.GT, 16, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)) .hasSize(47) .allMatch(model -> model.positiveVariables().size() >= 8); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.GE, 21, literals10, coeffs10), config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(1); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.GE, 22, literals10, coeffs10), config)); assertSolverUnsat(solver); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(PbEncoder.encode(f, (PBConstraint) f.pbc(CType.GT, 42, literals10, coeffs10), config)); assertSolverUnsat(solver); } @@ -318,15 +318,15 @@ public void testPBGreater() { @Test public void testPBNegative() { for (final EncoderConfig config : configs) { - for (final Supplier solverSupplier : solverSuppliers) { - SATSolver solver = solverSupplier.get(); + for (final Function solverSupplier : solverSuppliers) { + SATSolver solver = solverSupplier.apply(f); int[] coeffs10 = new int[]{2, 2, 2, 2, 2, 2, 2, 2, 2, -2}; final PBConstraint pbc = (PBConstraint) f.pbc(CType.EQ, 2, literals10, coeffs10); solver.add(PbEncoder.encode(f, pbc, config)); assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(45) .allMatch(m -> pbc.evaluate(m.assignment())); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); coeffs10 = new int[]{2, 2, 2, 2, 2, 2, 2, 2, 2, -2}; final PBConstraint pbc2 = (PBConstraint) f.pbc(CType.EQ, 4, literals10, coeffs10); @@ -334,7 +334,7 @@ public void testPBNegative() { assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(120) .allMatch(m -> pbc2.evaluate(m.assignment())); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); coeffs10 = new int[]{2, 2, -3, 2, -7, 2, 2, 2, 2, -2}; final PBConstraint pbc3 = (PBConstraint) f.pbc(CType.EQ, 4, literals10, coeffs10); @@ -342,7 +342,7 @@ public void testPBNegative() { assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(57) .allMatch(m -> pbc3.evaluate(m.assignment())); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); coeffs10 = new int[]{2, 2, -3, 2, -7, 2, 2, 2, 2, -2}; final PBConstraint pbc4 = (PBConstraint) f.pbc(CType.EQ, -10, literals10, coeffs10); @@ -350,7 +350,7 @@ public void testPBNegative() { assertSolverSat(solver); assertThat(solver.enumerateAllModels(literals10)).hasSize(8) .allMatch(m -> pbc4.evaluate(m.assignment())); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); coeffs10 = new int[]{2, 2, -4, 2, -6, 2, 2, 2, 2, -2}; final PBConstraint pbc5 = (PBConstraint) f.pbc(CType.EQ, -12, literals10, coeffs10); @@ -366,8 +366,8 @@ public void testPBNegative() { @LongRunningTag public void testLargePBs() { for (final EncoderConfig config : configs) { - for (final Supplier solverSupplier : solverSuppliers) { - final SATSolver solver = solverSupplier.get(); + for (final Function solverSupplier : solverSuppliers) { + final SATSolver solver = solverSupplier.apply(f); final int numLits = 100; final Variable[] lits = new Variable[numLits]; final int[] coeffs = new int[numLits]; @@ -378,7 +378,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.satCall().model(Arrays.asList(lits)))).isTrue(); + assertThat(pbc.evaluate(solver.satCall().model(Arrays.asList(lits)).assignment())).isTrue(); } } } diff --git a/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java b/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java index 6de3da34..01ffdd9c 100644 --- a/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java +++ b/src/test/java/com/booleworks/logicng/handlers/TimeoutModelEnumerationHandlerTest.java @@ -98,7 +98,7 @@ public void testTimeoutHandlerSingleTimeout() { final Formula formula = pg.generate(10).negate(f); for (final SATSolver solver : solvers) { solver.add(formula); - final TimeoutHandler handler = new TimeoutHandler(100L); + final TimeoutHandler handler = new TimeoutHandler(20L); final ModelEnumerationFunction me = ModelEnumerationFunction.builder(formula.variables(f)).build(); final LNGResult> result = me.apply(solver, handler); @@ -123,5 +123,5 @@ public void testTimeoutHandlerFixedEnd() { } } - // TODO test partial results (does not seem to work well with negated Pigeon Hole + // TODO test partial results (does not seem to work well with negated Pigeon Hole) } diff --git a/src/test/java/com/booleworks/logicng/handlers/TimeoutOptimizationHandlerTest.java b/src/test/java/com/booleworks/logicng/handlers/TimeoutOptimizationHandlerTest.java index 4d48ebaa..9d4d9b36 100644 --- a/src/test/java/com/booleworks/logicng/handlers/TimeoutOptimizationHandlerTest.java +++ b/src/test/java/com/booleworks/logicng/handlers/TimeoutOptimizationHandlerTest.java @@ -19,7 +19,7 @@ import static org.mockito.Mockito.verify; import static org.mockito.Mockito.when; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.handlers.events.OptimizationFoundBetterBoundEvent; @@ -56,9 +56,9 @@ public void testTimeoutFoundBetterBound() throws InterruptedException { final TimeoutHandler handler = new TimeoutHandler(100, SINGLE_TIMEOUT); handler.shouldResume(MODEL_ENUMERATION_STARTED); - assertThat(handler.shouldResume(new OptimizationFoundBetterBoundEvent(Assignment::new))).isTrue(); + assertThat(handler.shouldResume(new OptimizationFoundBetterBoundEvent(Model::new))).isTrue(); Thread.sleep(200); - assertThat(handler.shouldResume(new OptimizationFoundBetterBoundEvent(Assignment::new))).isFalse(); + assertThat(handler.shouldResume(new OptimizationFoundBetterBoundEvent(Model::new))).isFalse(); } @Test @@ -82,7 +82,7 @@ public void testTimeoutHandlerSingleTimeout() throws IOException { solver.add(formulas); final TimeoutHandler handler = new TimeoutHandler(10L); - final LNGResult result = solver.execute(OptimizationFunction.builder() + final LNGResult result = solver.execute(OptimizationFunction.builder() .literals(FormulaHelper.variables(f, formulas)) .maximize().build(), handler); assertThat(result.isSuccess()).isFalse(); @@ -96,7 +96,7 @@ public void testTimeoutHandlerFixedEnd() throws IOException { for (final SATSolver solver : solvers) { solver.add(formulas); final TimeoutHandler handler = new TimeoutHandler(100L, FIXED_END); - final LNGResult result = solver.execute(OptimizationFunction.builder() + final LNGResult result = solver.execute(OptimizationFunction.builder() .literals(FormulaHelper.variables(f, formulas)) .maximize().build(), handler); assertThat(result.isSuccess()).isFalse(); diff --git a/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDOperationsTest.java b/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDOperationsTest.java index 35522006..6bf151d2 100644 --- a/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDOperationsTest.java +++ b/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDOperationsTest.java @@ -8,6 +8,7 @@ import com.booleworks.logicng.RandomTag; import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Literal; @@ -17,7 +18,6 @@ import com.booleworks.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel; import com.booleworks.logicng.util.FormulaRandomizer; import com.booleworks.logicng.util.FormulaRandomizerConfig; -import org.assertj.core.api.Assertions; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; @@ -176,15 +176,15 @@ public void testUniversalQuantification() throws ParserException { @Test public void testModel() { - assertThat(bddVerum.model()).isEqualTo(new Assignment()); + assertThat(bddVerum.model()).isEqualTo(new Model()); assertThat(bddFalsum.model()).isEqualTo(null); - assertThat(bddPosLit.model()).isEqualTo(new Assignment(f.literal("A", true))); - assertThat(bddNegLit.model()).isEqualTo(new Assignment(f.literal("A", false))); - assertThat(bddImpl.model()).isEqualTo(new Assignment(f.literal("A", false))); - assertThat(bddEquiv.model()).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); - assertThat(bddOr.model()) + assertThat(bddPosLit.model()).isEqualTo(new Model(f.literal("A", true))); + assertThat(bddNegLit.model()).isEqualTo(new Model(f.literal("A", false))); + assertThat(bddImpl.model()).isEqualTo(new Model(f.literal("A", false))); + assertThat(bddEquiv.model().assignment()).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); + assertThat(bddOr.model().assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddAnd.model()) + assertThat(bddAnd.model().assignment()) .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true), f.literal("C", false))); } @@ -192,64 +192,82 @@ public void testModel() { public void testModelWithGivenVars() { final Variable a = f.variable("A"); final List ab = Arrays.asList(f.variable("A"), f.variable("B")); - assertThat(bddVerum.model(true, a)).isEqualTo(new Assignment(f.literal("A", true))); - assertThat(bddVerum.model(true, ab)).isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true))); - assertThat(bddVerum.model(false, a)).isEqualTo(new Assignment(f.literal("A", false))); - assertThat(bddVerum.model(false, ab)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false))); + assertThat(bddVerum.model(true, a)).isEqualTo(new Model(f.literal("A", true))); + assertThat(bddVerum.model(true, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true))); + assertThat(bddVerum.model(false, a)).isEqualTo(new Model(f.literal("A", false))); + assertThat(bddVerum.model(false, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false))); assertThat(bddFalsum.model(true, a)).isEqualTo(null); assertThat(bddFalsum.model(true, ab)).isEqualTo(null); assertThat(bddFalsum.model(false, a)).isEqualTo(null); assertThat(bddFalsum.model(false, ab)).isEqualTo(null); - assertThat(bddPosLit.model(true, a)).isEqualTo(new Assignment(f.literal("A", true))); - assertThat(bddPosLit.model(true, ab)).isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true))); - assertThat(bddPosLit.model(false, a)).isEqualTo(new Assignment(f.literal("A", true))); - assertThat(bddPosLit.model(false, ab)).isEqualTo(new Assignment(f.literal("A", true), f.literal("B", false))); - assertThat(bddNegLit.model(true, a)).isEqualTo(new Assignment(f.literal("A", false))); - assertThat(bddNegLit.model(true, ab)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); - assertThat(bddNegLit.model(false, a)).isEqualTo(new Assignment(f.literal("A", false))); - assertThat(bddNegLit.model(false, ab)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false))); - assertThat(bddImpl.model(true, a)).isEqualTo(new Assignment(f.literal("A", false))); - assertThat(bddImpl.model(true, ab)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); - assertThat(bddImpl.model(false, a)).isEqualTo(new Assignment(f.literal("A", false))); - assertThat(bddImpl.model(false, ab)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false))); - assertThat(bddEquiv.model(true, a)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); - assertThat(bddEquiv.model(true, ab)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); - assertThat(bddEquiv.model(false, a)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); - assertThat(bddEquiv.model(false, ab)).isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); - assertThat(bddOr.model(true, a)) + assertThat(bddPosLit.model(true, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", true))); + assertThat(bddPosLit.model(true, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true))); + assertThat(bddPosLit.model(false, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", true))); + assertThat(bddPosLit.model(false, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", false))); + assertThat(bddNegLit.model(true, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", false))); + assertThat(bddNegLit.model(true, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); + assertThat(bddNegLit.model(false, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", false))); + assertThat(bddNegLit.model(false, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false))); + assertThat(bddImpl.model(true, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", false))); + assertThat(bddImpl.model(true, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); + assertThat(bddImpl.model(false, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", false))); + assertThat(bddImpl.model(false, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false))); + assertThat(bddEquiv.model(true, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); + assertThat(bddEquiv.model(true, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); + assertThat(bddEquiv.model(false, a).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); + assertThat(bddEquiv.model(false, ab).assignment()) + .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true))); + assertThat(bddOr.model(true, a).assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddOr.model(true, ab)) + assertThat(bddOr.model(true, ab).assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddOr.model(false, a)) + assertThat(bddOr.model(false, a).assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddOr.model(false, ab)) + assertThat(bddOr.model(false, ab).assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddAnd.model(true, a)) + assertThat(bddAnd.model(true, a).assignment()) .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true), f.literal("C", false))); - assertThat(bddAnd.model(true, ab)) + assertThat(bddAnd.model(true, ab).assignment()) .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true), f.literal("C", false))); - assertThat(bddAnd.model(false, a)) + assertThat(bddAnd.model(false, a).assignment()) .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true), f.literal("C", false))); - assertThat(bddAnd.model(false, ab)) + assertThat(bddAnd.model(false, ab).assignment()) .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true), f.literal("C", false))); } @Test public void testFullModel() { - assertThat(bddVerum.fullModel()) + assertThat(bddVerum.fullModel().assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); assertThat(bddFalsum.fullModel()).isEqualTo(null); - assertThat(bddPosLit.fullModel()) + assertThat(bddPosLit.fullModel().assignment()) .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", false), f.literal("C", false))); - assertThat(bddNegLit.fullModel()) + assertThat(bddNegLit.fullModel().assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddImpl.fullModel()) + assertThat(bddImpl.fullModel().assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddEquiv.fullModel()) + assertThat(bddEquiv.fullModel().assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", true), f.literal("C", false))); - assertThat(bddOr.fullModel()) + assertThat(bddOr.fullModel().assignment()) .isEqualTo(new Assignment(f.literal("A", false), f.literal("B", false), f.literal("C", false))); - assertThat(bddAnd.fullModel()) + assertThat(bddAnd.fullModel().assignment()) .isEqualTo(new Assignment(f.literal("A", true), f.literal("B", true), f.literal("C", false))); } diff --git a/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/LargeBDDTest.java b/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/LargeBDDTest.java index 517eab40..efc4ad9d 100644 --- a/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/LargeBDDTest.java +++ b/src/test/java/com/booleworks/logicng/knowledgecompilation/bdds/LargeBDDTest.java @@ -89,7 +89,6 @@ public void testTimeoutHandlerNgLarge() { final TimeoutHandler handler = new TimeoutHandler(1000L); final LNGResult bdd = BDDFactory.build(f, queens, kernel, handler); assertThat(bdd.isSuccess()).isFalse(); - assertThat(bdd.getResult()).isNull(); } @Test diff --git a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java index 65c09ca1..392d05e3 100644 --- a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java +++ b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java @@ -139,7 +139,7 @@ private void testFormula(final Formula formula, final ComputationHandler handler if (!call.getSatResult().getResult()) { return; } - final SortedSet model = call.model(formula.variables(f)).literals(); + final List model = call.model(formula.variables(f)).getLiterals(); final NaivePrimeReduction naive = new NaivePrimeReduction(f, formula); final LNGResult> primeImplicant = naive.reduceImplicant(model, handler); if (expCanceled) { diff --git a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java index 48380788..ec2e46e8 100644 --- a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java +++ b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java @@ -24,7 +24,6 @@ import com.booleworks.logicng.util.FormulaHelper; import com.booleworks.logicng.util.FormulaRandomizer; import com.booleworks.logicng.util.FormulaRandomizerConfig; -import org.assertj.core.api.Assertions; import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; @@ -130,7 +129,7 @@ private void testFormula(final Formula formula, final ComputationHandler handler return; } final SortedSet falsifyingAssignment = - FormulaHelper.negateLiterals(f, call.model(formula.variables(f)).literals(), TreeSet::new); + FormulaHelper.negateLiterals(f, call.model(formula.variables(f)).getLiterals(), TreeSet::new); final NaivePrimeReduction naive = new NaivePrimeReduction(f, formula); final LNGResult> primeImplicate = naive.reduceImplicate(f, falsifyingAssignment, handler); if (expCanceled) { diff --git a/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java b/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java index 811f33f0..55d8b7c1 100644 --- a/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java @@ -16,7 +16,7 @@ import com.booleworks.logicng.LogicNGTest; import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.RandomTag; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.CardinalityConstraint; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; @@ -43,6 +43,8 @@ import com.booleworks.logicng.util.FormulaRandomizer; import com.booleworks.logicng.util.FormulaRandomizerConfig; import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.parallel.Execution; +import org.junit.jupiter.api.parallel.ExecutionMode; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; @@ -60,7 +62,7 @@ import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; -import java.util.function.Supplier; +import java.util.function.Function; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -68,69 +70,72 @@ public class OptimizationFunctionTest implements LogicNGTest { public static List solverSuppliers() { - final FormulaFactory f = FormulaFactory.caching(FormulaFactoryConfig.builder() - .formulaMergeStrategy(FormulaFactoryConfig.FormulaMergeStrategy.IMPORT).build()); final List solverSuppliers = SolverTestSet.solverSupplierTestSetForParameterizedTests( - Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD, INITIAL_PHASE, PROOF_GENERATION), f); - return solverSuppliers.stream().map(args -> Arguments.of(args.get()[0], f, args.get()[1])) + Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD, INITIAL_PHASE, PROOF_GENERATION)); + return solverSuppliers.stream() + .map(args -> Arguments.of( + args.get()[0], + FormulaFactory.caching(FormulaFactoryConfig.builder() + .formulaMergeStrategy(FormulaFactoryConfig.FormulaMergeStrategy.IMPORT).build()), + args.get()[1])) .collect(Collectors.toList()); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") - public void testUnsatFormula(final Supplier solver, final FormulaFactory f, + public void testUnsatFormula(final Function solver, final FormulaFactory f, final String solverDescription) throws ParserException { final Formula formula = f.parse("a & b & (a => ~b)"); - final LNGResult minimumModel = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), false, solver.get(), NopHandler.get()); + final LNGResult minimumModel = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), false, solver.apply(f), NopHandler.get()); assertThat(minimumModel).isNull(); - final LNGResult maximumModel = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), true, solver.get(), NopHandler.get()); + final LNGResult maximumModel = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), true, solver.apply(f), NopHandler.get()); assertThat(maximumModel).isNull(); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") - public void testSingleModel(final Supplier solver, final FormulaFactory f, + public void testSingleModel(final Function solver, final FormulaFactory f, final String solverDescription) throws ParserException { final Formula formula = f.parse("~a & ~b & ~c"); - final LNGResult minimumModel = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), false, solver.get(), NopHandler.get()); + final LNGResult minimumModel = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), false, solver.apply(f), NopHandler.get()); testMinimumModel(formula, minimumModel, formula.variables(f)); - final LNGResult maximumModel = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), true, solver.get(), NopHandler.get()); + final LNGResult maximumModel = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), true, solver.apply(f), NopHandler.get()); testMaximumModel(formula, maximumModel, formula.variables(f)); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") - public void testExoModel(final Supplier solver, final FormulaFactory f, + public void testExoModel(final Function solver, final FormulaFactory f, final String solverDescription) { final CardinalityConstraint exo = (CardinalityConstraint) f.exo(f.variable("a"), f.variable("b"), f.variable("c")); - final LNGResult minimumModel = optimize(Collections.singleton(exo), exo.variables(f), - Collections.emptyList(), false, solver.get(), NopHandler.get()); + final LNGResult minimumModel = optimize(Collections.singleton(exo), exo.variables(f), + Collections.emptyList(), false, solver.apply(f), NopHandler.get()); testMinimumModel(exo, minimumModel, exo.variables(f)); - final LNGResult maximumModel = optimize(Collections.singleton(exo), exo.variables(f), - Collections.emptyList(), true, solver.get(), NopHandler.get()); + final LNGResult maximumModel = optimize(Collections.singleton(exo), exo.variables(f), + Collections.emptyList(), true, solver.apply(f), NopHandler.get()); testMaximumModel(exo, maximumModel, exo.variables(f)); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") - public void testCornerCases(final Supplier solver, final FormulaFactory f, + public void testCornerCases(final Function solver, final FormulaFactory f, final String solverDescription) { final FormulaCornerCases cornerCases = new FormulaCornerCases(f); for (final Formula formula : cornerCases.cornerCases()) { if (formula.holds(new SATPredicate(f))) { final Set targetLiterals = cornerCases.getVariables(); - final LNGResult minimumModel = optimize(Collections.singleton(formula), - targetLiterals, Collections.emptySet(), false, solver.get(), NopHandler.get()); + final LNGResult minimumModel = optimize(Collections.singleton(formula), + targetLiterals, Collections.emptySet(), false, solver.apply(f), NopHandler.get()); testMinimumModel(formula, minimumModel, targetLiterals); - final LNGResult maximumModel = optimize(Collections.singleton(formula), - targetLiterals, Collections.emptySet(), true, solver.get(), NopHandler.get()); + final LNGResult maximumModel = optimize(Collections.singleton(formula), + targetLiterals, Collections.emptySet(), true, solver.apply(f), NopHandler.get()); testMaximumModel(formula, maximumModel, targetLiterals); } } @@ -139,7 +144,9 @@ public void testCornerCases(final Supplier solver, final FormulaFacto @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") @RandomTag - public void testRandomSmall(final Supplier solver, final FormulaFactory f0, + @Execution(ExecutionMode.SAME_THREAD) + + public void testRandomSmall(final Function solver, final FormulaFactory f0, final String solverDescription) { final FormulaFactory f = FormulaFactory.nonCaching(FormulaFactoryConfig.builder() // caching factory goes out of heap @@ -157,12 +164,12 @@ public void testRandomSmall(final Supplier solver, final FormulaFacto randomTargetLiterals(f, random, randomSubset(random, variables, Math.min(variables.size(), 5))); final Set additionalVariables = randomSubset(random, variables, Math.min(variables.size(), 3)); - final LNGResult minimumModel = optimize(Collections.singleton(formula), - targetLiterals, additionalVariables, false, solver.get(), NopHandler.get()); + final LNGResult minimumModel = optimize(Collections.singleton(formula), + targetLiterals, additionalVariables, false, solver.apply(f), NopHandler.get()); testMinimumModel(formula, minimumModel, targetLiterals); - final LNGResult maximumModel = optimize(Collections.singleton(formula), - targetLiterals, additionalVariables, true, solver.get(), NopHandler.get()); + final LNGResult maximumModel = optimize(Collections.singleton(formula), + targetLiterals, additionalVariables, true, solver.apply(f), NopHandler.get()); testMaximumModel(formula, maximumModel, targetLiterals); } } @@ -186,15 +193,15 @@ private static SortedSet randomTargetLiterals(final FormulaFactory f, f @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") - public void testIncrementalityMinimizeAndMaximize(final Supplier solverSupplier, final FormulaFactory f) + public void testIncrementalityMinimizeAndMaximize(final Function solverSupplier, final FormulaFactory f) throws ParserException { Formula formula = f.parse("(a|b|c|d|e) & (p|q) & (x|y|z)"); - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); final SortedSet vars = new TreeSet<>(formula.variables(f)); solver.add(formula); - Assignment minimumModel = solver.execute(builder().minimize().literals(vars).build()); - Assignment maximumModel = solver.execute(builder().maximize().literals(vars).build()); + Model minimumModel = solver.execute(builder().minimize().literals(vars).build()); + Model maximumModel = solver.execute(builder().maximize().literals(vars).build()); assertThat(minimumModel.positiveVariables()).hasSize(3); assertThat(maximumModel.positiveVariables()).hasSize(10); @@ -240,7 +247,7 @@ public void testIncrementalityMinimizeAndMaximize(final Supplier solv @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") - public void testAdditionalVariables(final Supplier solver, final FormulaFactory f, + public void testAdditionalVariables(final Function solver, final FormulaFactory f, final String solverDescription) throws ParserException { final Variable a = f.variable("a"); @@ -255,80 +262,80 @@ public void testAdditionalVariables(final Supplier solver, final Form final Formula formula = f.parse("(a|b) & (~a => c) & (x|y)"); final List literalsANBX = Arrays.asList(a, nb, x); - final LNGResult minimumModel = optimize(Collections.singleton(formula), literalsANBX, - Collections.emptyList(), false, solver.get(), NopHandler.get()); - assertThat(minimumModel.getResult().literals()).containsExactlyInAnyOrder(na, b, nx); - final LNGResult minimumModelWithY = optimize(Collections.singleton(formula), - literalsANBX, Collections.singleton(y), false, solver.get(), NopHandler.get()); - assertThat(minimumModelWithY.getResult().literals()) + final LNGResult minimumModel = optimize(Collections.singleton(formula), literalsANBX, + Collections.emptyList(), false, solver.apply(f), NopHandler.get()); + assertThat(minimumModel.getResult().getLiterals()).containsExactlyInAnyOrder(na, b, nx); + final LNGResult minimumModelWithY = optimize(Collections.singleton(formula), + literalsANBX, Collections.singleton(y), false, solver.apply(f), NopHandler.get()); + assertThat(minimumModelWithY.getResult().getLiterals()) .containsExactlyInAnyOrder(na, b, nx, y); - final Assignment minimumModelWithCY = optimize(Collections.singleton(formula), - literalsANBX, Arrays.asList(c, y), false, solver.get(), NopHandler.get()).getResult(); - assertThat(minimumModelWithCY.literals()).containsExactlyInAnyOrder(na, b, c, nx, y); + final Model minimumModelWithCY = optimize(Collections.singleton(formula), + literalsANBX, Arrays.asList(c, y), false, solver.apply(f), NopHandler.get()).getResult(); + assertThat(minimumModelWithCY.getLiterals()).containsExactlyInAnyOrder(na, b, c, nx, y); final List literalsNBNX = Arrays.asList(na, nx); - final Assignment maximumModel = optimize(Collections.singleton(formula), literalsNBNX, Collections.emptyList(), - true, solver.get(), NopHandler.get()).getResult(); - assertThat(maximumModel.literals()).containsExactlyInAnyOrder(na, nx); - final Assignment maximumModelWithC = optimize(Collections.singleton(formula), literalsNBNX, - Collections.singleton(c), true, solver.get(), NopHandler.get()).getResult(); - assertThat(maximumModelWithC.literals()).containsExactlyInAnyOrder(na, c, nx); - final Assignment maximumModelWithACY = optimize(Collections.singleton(formula), literalsNBNX, - Arrays.asList(a, c, y), true, solver.get(), NopHandler.get()).getResult(); - assertThat(maximumModelWithACY.literals()).containsExactlyInAnyOrder(na, c, nx, y); + final Model maximumModel = optimize(Collections.singleton(formula), literalsNBNX, Collections.emptyList(), + true, solver.apply(f), NopHandler.get()).getResult(); + assertThat(maximumModel.getLiterals()).containsExactlyInAnyOrder(na, nx); + final Model maximumModelWithC = optimize(Collections.singleton(formula), literalsNBNX, + Collections.singleton(c), true, solver.apply(f), NopHandler.get()).getResult(); + assertThat(maximumModelWithC.getLiterals()).containsExactlyInAnyOrder(na, c, nx); + final Model maximumModelWithACY = optimize(Collections.singleton(formula), literalsNBNX, + Arrays.asList(a, c, y), true, solver.apply(f), NopHandler.get()).getResult(); + assertThat(maximumModelWithACY.getLiterals()).containsExactlyInAnyOrder(na, c, nx, y); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") @LongRunningTag - public void testLargeFormulaMinimize(final Supplier solver, final FormulaFactory f, + public void testLargeFormulaMinimize(final Function solver, final FormulaFactory f, final String solverDescription) throws IOException, ParserException { final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); final List variables = randomSubset(formula.variables(f), 300); - final LNGResult minimumModel = optimize(Collections.singleton(formula), variables, - Collections.emptyList(), false, solver.get(), NopHandler.get()); + final LNGResult minimumModel = optimize(Collections.singleton(formula), variables, + Collections.emptyList(), false, solver.apply(f), NopHandler.get()); testMinimumModel(formula, minimumModel, variables); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") @LongRunningTag - public void testLargeFormulaMaximize(final Supplier solver, final FormulaFactory f, + public void testLargeFormulaMaximize(final Function solver, final FormulaFactory f, final String solverDescription) throws IOException, ParserException { final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); - final LNGResult maximumModel = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), true, solver.get(), NopHandler.get()); + final LNGResult maximumModel = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), true, solver.apply(f), NopHandler.get()); testMaximumModel(formula, maximumModel, formula.variables(f)); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") @LongRunningTag - public void testLargerFormulaMinimize(final Supplier solver, final FormulaFactory f, + public void testLargerFormulaMinimize(final Function solver, final FormulaFactory f, final String solverDescription) throws IOException, ParserException { final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); - final LNGResult minimumModel = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), false, solver.get(), NopHandler.get()); + final LNGResult minimumModel = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), false, solver.apply(f), NopHandler.get()); testMinimumModel(formula, minimumModel, formula.variables(f)); } @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") @LongRunningTag - public void testLargerFormulaMaximize(final Supplier solver, final FormulaFactory f, + public void testLargerFormulaMaximize(final Function solver, final FormulaFactory f, final String solverDescription) throws IOException, ParserException { final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); final List variables = randomSubset(formula.variables(f), 300); - final LNGResult maximumModel = optimize(Collections.singleton(formula), variables, - Collections.emptyList(), true, solver.get(), NopHandler.get()); + final LNGResult maximumModel = optimize(Collections.singleton(formula), variables, + Collections.emptyList(), true, solver.apply(f), NopHandler.get()); testMaximumModel(formula, maximumModel, variables); } @@ -364,27 +371,27 @@ public void compareWithMaxSat() throws IOException, ParserException { @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") @LongRunningTag - public void testTimeoutOptimizationHandler(final Supplier solver, final FormulaFactory f, + public void testTimeoutOptimizationHandler(final Function solver, final FormulaFactory f, final String solverDescription) throws IOException, ParserException { final Formula formula = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); final TimeoutHandler handlerMax = new TimeoutHandler(1L); - final LNGResult maximumModel = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), true, solver.get(), handlerMax); + final LNGResult maximumModel = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), true, solver.apply(f), handlerMax); assertThat(maximumModel.isSuccess()).isFalse(); assertThat(maximumModel.isPartial()).isFalse(); assertThat(maximumModel.getPartialResult()).isNull(); final TimeoutHandler handlerTooShort = new TimeoutHandler(0L); - final LNGResult model = optimize(Collections.singleton(formula), formula.variables(f), - Collections.emptyList(), false, solver.get(), handlerTooShort); + final LNGResult model = optimize(Collections.singleton(formula), formula.variables(f), + Collections.emptyList(), false, solver.apply(f), handlerTooShort); assertThat(model.isSuccess()).isFalse(); assertThat(model.isPartial()).isFalse(); assertThat(model.getPartialResult()).isNull(); final CustomOptimizationHandler customHandler = new CustomOptimizationHandler(); - final LNGResult modelCustom = optimize(Collections.singleton(formula), - formula.variables(f), Collections.emptyList(), true, solver.get(), customHandler); + final LNGResult modelCustom = optimize(Collections.singleton(formula), + formula.variables(f), Collections.emptyList(), true, solver.apply(f), customHandler); assertThat(modelCustom.isSuccess()).isFalse(); assertThat(modelCustom.isPartial()).isTrue(); assertThat(modelCustom.getPartialResult()).isNotNull(); @@ -394,7 +401,7 @@ public void testTimeoutOptimizationHandler(final Supplier solver, fin @ParameterizedTest(name = "{index} {2}") @MethodSource("solverSuppliers") @LongRunningTag - public void testCancellationPoints(final Supplier solverSupplier, final FormulaFactory f0, + public void testCancellationPoints(final Function solverSupplier, final FormulaFactory f0, final String solverDescription) throws IOException { final FormulaFactory f = FormulaFactory.caching(); final SortedSet selVars = new TreeSet<>(); @@ -405,12 +412,12 @@ public void testCancellationPoints(final Supplier solverSupplier, fin selVars.add(selVar); formulas.add(f.equivalence(selVar, clause)); } - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); for (int numSatHandlerStarts = 1; numSatHandlerStarts < 4; numSatHandlerStarts++) { solver.add(formulas); final ComputationHandler handler = new BoundedOptimizationHandler(numSatHandlerStarts, -1); final OptimizationFunction optimizationFunction = builder().literals(selVars).maximize().build(); - final LNGResult result = solver.execute(optimizationFunction, handler); + final LNGResult result = solver.execute(optimizationFunction, handler); assertThat(result.isSuccess()).isFalse(); } } @@ -422,13 +429,13 @@ private int solveMaxSat(final List formulas, final SortedSet return solver.solve().getOptimum(); } - private SortedSet satisfiedLiterals(final LNGResult assignment, - final Collection literals) { - final SortedSet modelLiterals = assignment.getResult().literals(); - return literals.stream().filter(modelLiterals::contains).collect(toCollection(TreeSet::new)); + private List satisfiedLiterals(final LNGResult model, + final Collection literals) { + final Set modelLiterals = new HashSet<>(model.getResult().getLiterals()); + return literals.stream().filter(modelLiterals::contains).collect(Collectors.toList()); } - private static LNGResult optimize( + private static LNGResult optimize( final Collection formulas, final Collection literals, final Collection additionalVariables, final boolean maximize, final SATSolver solver, final ComputationHandler handler) { @@ -445,21 +452,21 @@ private static LNGResult optimize( } } - private void testMinimumModel(final Formula formula, final LNGResult resultModel, + private void testMinimumModel(final Formula formula, final LNGResult resultModel, final Collection literals) { testOptimumModel(formula, resultModel, literals, false); } - private void testMaximumModel(final Formula formula, final LNGResult resultModel, + private void testMaximumModel(final Formula formula, final LNGResult resultModel, final Collection literals) { testOptimumModel(formula, resultModel, literals, true); } - private void testOptimumModel(final Formula formula, final LNGResult optimumModel, + private void testOptimumModel(final Formula formula, final LNGResult optimumModel, final Collection literals, final boolean maximize) { assertThat(optimumModel.isSuccess()).isTrue(); final FormulaFactory f = formula.factory(); - final SortedSet optimumLiterals = optimumModel.getResult().literals(); + final List optimumLiterals = optimumModel.getResult().getLiterals(); if (literals.isEmpty()) { assertThat(optimumLiterals).isEmpty(); } else { @@ -479,7 +486,7 @@ private static List randomSubset(final Collection original, } private static class CustomOptimizationHandler implements ComputationHandler { - public Assignment currentResult; + public Model currentResult; private boolean canceled; @Override diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java index 4373f3f2..8afa6174 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java @@ -319,7 +319,7 @@ public void testNonClauselSoftConstraints() throws ParserException { solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1); final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); - assertThat(result.getModel().literals()).containsExactlyInAnyOrder( + assertThat(result.getModel().getLiterals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") ); assertThat(result.getOptimum()).isEqualTo(1); @@ -337,7 +337,7 @@ public void testSoftConstraintsCornerCaseVerum() throws ParserException { solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1); final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); - assertThat(result.getModel().literals()).containsExactlyInAnyOrder( + assertThat(result.getModel().getLiterals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") ); assertThat(result.getOptimum()).isEqualTo(1); @@ -355,7 +355,7 @@ public void testSoftConstraintsCornerCaseFalsum() throws ParserException { solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1); final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); - assertThat(result.getModel().literals()).containsExactlyInAnyOrder( + assertThat(result.getModel().getLiterals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") ); assertThat(result.getOptimum()).isEqualTo(2); diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java index b4b3fbbf..1ea24179 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java @@ -343,7 +343,7 @@ public void testWeightedNonClauseSoftConstraints() throws ParserException { solver.addSoftFormula(f.parse("~a & ~b & ~c"), 2); final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); - assertThat(result.getModel().literals()).containsExactlyInAnyOrder( + assertThat(result.getModel().getLiterals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") ); assertThat(result.getOptimum()).isEqualTo(2); @@ -364,7 +364,7 @@ public void testWeightedSoftConstraintsCornerCaseVerum() throws ParserException solver.addSoftFormula(f.parse("~a & ~b & ~c"), 3); final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); - assertThat(result.getModel().literals()).containsExactlyInAnyOrder( + assertThat(result.getModel().getLiterals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") ); assertThat(result.getOptimum()).isEqualTo(3); @@ -384,7 +384,7 @@ public void testWeightedSoftConstraintsCornerCaseFalsum() throws ParserException solver.addSoftFormula(f.parse("~a & ~b & ~c"), 3); final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); - assertThat(result.getModel().literals()).containsExactlyInAnyOrder( + assertThat(result.getModel().getLiterals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") ); assertThat(result.getOptimum()).isEqualTo(5); diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java index bb31080a..e6dd3a80 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java @@ -11,7 +11,7 @@ import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.TestWithExampleFormulas; -import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Variable; import com.booleworks.logicng.io.parsers.ParserException; import com.booleworks.logicng.io.parsers.PropositionalParser; @@ -295,7 +295,7 @@ public void testAssignment() throws ParserException { final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(3); - final Assignment model = result.getModel(); + final Model model = result.getModel(); assertThat(model.size()).isEqualTo(8); assertThat(model.positiveVariables()).hasSize(1); assertThat(model.positiveVariables()).extracting(Variable::name).containsExactlyInAnyOrder("y"); @@ -315,7 +315,7 @@ public void testToString() { solvers[5] = MaxSATSolver.wmsu3(f); final String expected = "MaxSATSolver{result=ComputationResult{" + - "result=MaxSATResult{satisfiable=true, optimum=1, model=Assignment{pos=[], neg=[~a, ~b]}}, " + + "result=MaxSATResult{satisfiable=true, optimum=1, model=Model{literals=[~a, ~b]}}, " + "cancelCause=null}, var2index={@SEL_SOFT_0=2, @SEL_SOFT_1=3, a=0, b=1}}"; for (int i = 0; i < solvers.length; i++) { diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java index 79487eb1..6173a910 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/ModelTest.java @@ -10,7 +10,6 @@ import static com.booleworks.logicng.solvers.sat.SolverTestSet.solverSupplierTestSetForParameterizedTests; import static org.assertj.core.api.Assertions.assertThat; -import com.booleworks.logicng.datastructures.Assignment; import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; @@ -30,7 +29,7 @@ import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; -import java.util.function.Supplier; +import java.util.function.Function; @SuppressWarnings("unused") public class ModelTest { @@ -38,59 +37,61 @@ public class ModelTest { private static final FormulaFactory f = FormulaFactory.caching(); public static Collection solverSuppliers() { - return solverSupplierTestSetForParameterizedTests(Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD), f); + return solverSupplierTestSetForParameterizedTests(Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD)); } @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testNoModel(final Supplier solverSupplier, final String solverDescription) + public void testNoModel(final Function solverSupplier, final String solverDescription) throws ParserException { - SATSolver solver = solverSupplier.get(); + SATSolver solver = solverSupplier.apply(f); solver.add(f.falsum()); assertThat(solver.satCall().model(f.variables())).isNull(); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(f.parse("A & ~A")); assertThat(solver.satCall().model(f.variables("A"))).isNull(); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(f.parse("(A => (B & C)) & A & C & (C <=> ~B)")); assertThat(solver.satCall().model(f.variables("A", "B", "C"))).isNull(); } @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testEmptyModel(final Supplier solverSupplier, final String solverDescription) { - final SATSolver solver = solverSupplier.get(); + public void testEmptyModel(final Function solverSupplier, + final String solverDescription) { + final SATSolver solver = solverSupplier.apply(f); solver.add(f.verum()); - final Assignment model = solver.satCall().model(f.variables()); - assertThat(model.literals()).isEmpty(); + final Model model = solver.satCall().model(f.variables()); + assertThat(model.getLiterals()).isEmpty(); assertThat(model.blockingClause(f)).isEqualTo(f.falsum()); assertThat(solver.enumerateAllModels(List.of())).hasSize(1); } @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testSimpleModel(final Supplier solverSupplier, final String solverDescription) { - SATSolver solver = solverSupplier.get(); + public void testSimpleModel(final Function solverSupplier, + final String solverDescription) { + SATSolver solver = solverSupplier.apply(f); solver.add(f.literal("A", true)); - Assignment model = solver.satCall().model(f.variables("A")); - assertThat(model.literals()).containsExactly(f.literal("A", true)); + Model model = solver.satCall().model(f.variables("A")); + assertThat(model.getLiterals()).containsExactly(f.literal("A", true)); assertThat(solver.enumerateAllModels(f.variables("A"))).hasSize(1); - solver = solverSupplier.get(); + solver = solverSupplier.apply(f); solver.add(f.literal("A", false)); model = solver.satCall().model(f.variables("A")); - assertThat(model.literals()).containsExactly(f.literal("A", false)); + assertThat(model.getLiterals()).containsExactly(f.literal("A", false)); assertThat(solver.enumerateAllModels(f.variables("A"))).hasSize(1); } @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testCNFFormula(final Supplier solverSupplier, final String solverDescription) - throws ParserException { - final SATSolver solver = solverSupplier.get(); + public void testCNFFormula(final Function solverSupplier, + final String solverDescription) throws ParserException { + final SATSolver solver = solverSupplier.apply(f); final Formula formula = f.parse("(A|B|C) & (~A|~B|~C) & (A|~B|~C) & (~A|~B|C)"); solver.add(formula); - final Assignment model = solver.satCall().model(f.variables("A", "B", "C")); - assertThat(formula.evaluate(model)).isTrue(); + final Model model = solver.satCall().model(f.variables("A", "B", "C")); + assertThat(formula.evaluate(model.assignment())).isTrue(); assertThat(solver.enumerateAllModels(f.variables("A", "B", "C"))).hasSize(4); for (final Model m : solver.enumerateAllModels(f.variables("A", "B", "C"))) { assertThat(formula.evaluate(m.assignment())).isTrue(); @@ -99,15 +100,15 @@ public void testCNFFormula(final Supplier solverSupplier, final Strin @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final Supplier solverSupplier, + public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final Function solverSupplier, final String solverDescription) throws ParserException { - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); 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.satCall().model(formula.variables(f)); - assertThat(formula.evaluate(model)).isTrue(); + final Model model = solver.satCall().model(formula.variables(f)); + assertThat(formula.evaluate(model.assignment())).isTrue(); final List allModels = solver.enumerateAllModels(formula.variables(f)); assertThat(allModels).hasSize(4); assertThat(model.formula(f).variables(f)).isEqualTo(formula.variables(f)); @@ -119,13 +120,14 @@ public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final Supplier solverSupplier, final String solverDescription) + public void testNonCNFAllVars(final Function solverSupplier, + final String solverDescription) throws ParserException { - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solver.add(formula); - final Assignment model = solver.satCall().model(formula.variables(f)); - assertThat(formula.evaluate(model)).isTrue(); + final Model model = solver.satCall().model(formula.variables(f)); + assertThat(formula.evaluate(model.assignment())).isTrue(); final List allModels = solver.enumerateAllModels(formula.variables(f)); assertThat(allModels).hasSize(4); for (final Model m : allModels) { @@ -136,13 +138,14 @@ public void testNonCNFAllVars(final Supplier solverSupplier, final St @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testNonCNFOnlyFormulaVars(final Supplier solverSupplier, final String solverDescription) + public void testNonCNFOnlyFormulaVars(final Function solverSupplier, + final String solverDescription) throws ParserException { - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solver.add(formula); - final Assignment model = solver.satCall().model(formula.variables(f)); - assertThat(formula.evaluate(model)).isTrue(); + final Model model = solver.satCall().model(formula.variables(f)); + assertThat(formula.evaluate(model.assignment())).isTrue(); assertThat(model.formula(f).variables(f)).isEqualTo(formula.variables(f)); final List allModels = solver.enumerateAllModels(formula.variables(f)); assertThat(allModels).hasSize(4); @@ -154,17 +157,18 @@ public void testNonCNFOnlyFormulaVars(final Supplier solverSupplier, @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testNonCNFRestrictedVars(final Supplier solverSupplier, final String solverDescription) + public void testNonCNFRestrictedVars(final Function solverSupplier, + final String solverDescription) throws ParserException { - final SATSolver solverForMe = solverSupplier.get(); + final SATSolver solverForMe = solverSupplier.apply(f); final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); final SATSolver verificationSolver = SATSolver.newSolver(f); verificationSolver.add(formula); solverForMe.add(formula); final SortedSet relevantVariables = new TreeSet<>(Arrays.asList(f.variable("A"), f.variable("B"), f.variable("C"))); - final Assignment model = solverForMe.satCall().model(relevantVariables); - assertThat(verificationSolver.satCall().addFormulas(model.literals()).sat().getResult()).isTrue(); + final Model model = solverForMe.satCall().model(relevantVariables); + assertThat(verificationSolver.satCall().addFormulas(model.getLiterals()).sat().getResult()).isTrue(); assertThat(model.formula(f).variables(f)).isEqualTo(relevantVariables); final List allModels = solverForMe.enumerateAllModels(relevantVariables); assertThat(allModels).hasSize(2); @@ -176,10 +180,10 @@ public void testNonCNFRestrictedVars(final Supplier solverSupplier, f @ParameterizedTest(name = "{index} {1}") @MethodSource("solverSuppliers") - public void testNonCNFRestrictedAndAdditionalVars(final Supplier solverSupplier, + public void testNonCNFRestrictedAndAdditionalVars(final Function solverSupplier, final String solverDescription) throws ParserException { - final SATSolver solverForMe = solverSupplier.get(); + final SATSolver solverForMe = solverSupplier.apply(f); final SATSolver verificationSolver = SATSolver.newSolver(f); final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solverForMe.add(formula); @@ -190,8 +194,8 @@ public void testNonCNFRestrictedAndAdditionalVars(final Supplier solv new TreeSet<>(Arrays.asList(f.variable("D"), f.variable("X"), f.variable("Y"))); final SortedSet allVariables = new TreeSet<>(relevantVariables); allVariables.addAll(additionalVariables); - final Assignment model = solverForMe.satCall().model(additionalVariables); - assertThat(verificationSolver.satCall().addFormulas(model.literals()).sat().getResult()).isTrue(); + final Model model = solverForMe.satCall().model(additionalVariables); + assertThat(verificationSolver.satCall().addFormulas(model.getLiterals()).sat().getResult()).isTrue(); assertThat(model.formula(f).variables(f)).containsExactlyInAnyOrder(f.variable("D"), f.variable("X"), f.variable("Y")); final ModelEnumerationFunction me = ModelEnumerationFunction.builder(relevantVariables) diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java index eb53de96..1ae9a4bf 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java @@ -4,6 +4,7 @@ import static org.assertj.core.api.Assertions.assertThatThrownBy; import com.booleworks.logicng.datastructures.Assignment; +import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Variable; import com.booleworks.logicng.formulas.implementation.cached.CachingFormulaFactory; @@ -61,7 +62,7 @@ public void testIllegalOperationsOnOpenSatCall() throws ParserException { solver.loadState(newState); solver.add(f.variable("a")); assertThat(solver.sat()).isTrue(); - assertThat(solver.satCall().model(List.of(f.variable("a")))).isEqualTo(new Assignment(f.variable("a"))); + assertThat(solver.satCall().model(List.of(f.variable("a")))).isEqualTo(new Model(f.variable("a"))); } @Test @@ -81,13 +82,13 @@ public void testDirectModelMethod() throws ParserException { solver.add(f.parse("c & (~c | ~a)")); final Set abc = Set.of(f.variable("a"), f.variable("b"), f.variable("c")); final Set abcd = Set.of(f.variable("a"), f.variable("b"), f.variable("c"), f.variable("d")); - assertThat(solver.satCall().model(abc)) + assertThat(solver.satCall().model(abc).assignment()) .isEqualTo(new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"))); - assertThat(solver.satCall().addFormulas(f.parse("c | d")).model(abcd)).isIn( + assertThat(solver.satCall().addFormulas(f.parse("c | d")).model(abcd).assignment()).isIn( new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"), f.literal("d", false)), new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"), f.literal("d", true)) ); - assertThat(solver.satCall().model(abc)) + assertThat(solver.satCall().model(abc).assignment()) .isEqualTo(new Assignment(f.literal("a", false), f.variable("b"), f.variable("c"))); } @@ -162,15 +163,15 @@ public void testSelectionOrder() throws ParserException { final Variable c = f.variable("c"); final Variable d = f.variable("d"); - assertThat(solver.satCall().selectionOrder(List.of(a, b, c, d)).model(List.of(a, b, c, d))) + assertThat(solver.satCall().selectionOrder(List.of(a, b, c, d)).model(List.of(a, b, c, d)).assignment()) .isEqualTo(new Assignment(a, b.negate(f), c, d.negate(f))); - assertThat(solver.satCall().selectionOrder(List.of(b, a, d, c)).model(List.of(a, b, c, d))) + assertThat(solver.satCall().selectionOrder(List.of(b, a, d, c)).model(List.of(a, b, c, d)).assignment()) .isEqualTo(new Assignment(a.negate(f), b, c.negate(f), d)); assertThat(solver.satCall().selectionOrder(List.of(a.negate(f), b.negate(f), c.negate(f), d.negate(f))) - .model(List.of(a, b, c, d))) + .model(List.of(a, b, c, d)).assignment()) .isEqualTo(new Assignment(a.negate(f), b.negate(f), c.negate(f), d)); assertThat(solver.satCall().selectionOrder(List.of(a.negate(f), b.negate(f), d.negate(f), c.negate(f))) - .model(List.of(a, b, c, d))) + .model(List.of(a, b, c, d)).assignment()) .isEqualTo(new Assignment(a.negate(f), b.negate(f), c, d.negate(f))); } @@ -216,7 +217,7 @@ public void testAdditionalFormulasAndPropositions() throws ParserException { assertThat( solver.satCall().addFormulas(f.parse("e <=> f")).addPropositions(new StandardProposition(f.parse("~e"))) - .model(solver.underlyingSolver().knownVariables())).isIn( + .model(solver.underlyingSolver().knownVariables()).assignment()).isIn( new Assignment(f.literal("a", true), f.literal("b", true), f.literal("c", false), f.literal("d", false), f.literal("e", false), f.literal("f", false)), new Assignment(f.literal("a", false), f.literal("b", true), f.literal("c", false), @@ -227,7 +228,7 @@ public void testAdditionalFormulasAndPropositions() throws ParserException { assertThat(solver.satCall().addPropositions(new StandardProposition(f.parse("e <=> f"))) .addPropositions(new StandardProposition(f.parse("~e"))) - .model(solver.underlyingSolver().knownVariables())).isIn( + .model(solver.underlyingSolver().knownVariables()).assignment()).isIn( new Assignment(f.literal("a", true), f.literal("b", true), f.literal("c", false), f.literal("d", false), f.literal("e", false), f.literal("f", false)), new Assignment(f.literal("a", false), f.literal("b", true), f.literal("c", false), diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java index b2b96141..457d405f 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/SATTest.java @@ -18,7 +18,6 @@ import com.booleworks.logicng.LogicNGTest; import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.TestWithExampleFormulas; -import com.booleworks.logicng.datastructures.Assignment; import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.formulas.CType; import com.booleworks.logicng.formulas.Formula; @@ -52,18 +51,19 @@ import java.util.Collection; import java.util.Collections; import java.util.HashMap; +import java.util.HashSet; import java.util.LinkedHashSet; import java.util.List; import java.util.Map; import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; -import java.util.function.Supplier; +import java.util.function.Function; public class SATTest extends TestWithExampleFormulas implements LogicNGTest { private final List solvers; - private final List> solverSuppliers; + private final List> solverSuppliers; private final PigeonHoleGenerator pg; private final PropositionalParser parser; @@ -73,7 +73,7 @@ public SATTest() { solvers = SolverTestSet.solverTestSet( Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD, CLAUSE_MINIMIZATION, PROOF_GENERATION, INITIAL_PHASE), f); solverSuppliers = SolverTestSet.solverSupplierTestSet( - Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD, CLAUSE_MINIMIZATION, PROOF_GENERATION, INITIAL_PHASE), f); + Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD, CLAUSE_MINIMIZATION, PROOF_GENERATION, INITIAL_PHASE)); } @Test @@ -97,7 +97,7 @@ public void testLiterals1() { for (final SATSolver s : solvers) { s.add(A); assertThat(s.satCall().model(List.of(A)).size()).isEqualTo(1); - assertThat(s.satCall().model(List.of(A)).evaluateLit(A)).isTrue(); + assertThat(s.satCall().model(List.of(A)).assignment().evaluateLit(A)).isTrue(); s.add(NA); assertSolverUnsat(s); } @@ -108,7 +108,7 @@ public void testLiterals2() { for (final SATSolver s : solvers) { s.add(NA); assertThat(s.satCall().model(List.of(A)).size()).isEqualTo(1); - assertThat(s.satCall().model(List.of(A)).evaluateLit(NA)).isTrue(); + assertThat(s.satCall().model(List.of(A)).assignment().evaluateLit(NA)).isTrue(); } } @@ -117,8 +117,8 @@ public void testAnd1() { for (final SATSolver s : solvers) { s.add(AND1); assertThat(s.satCall().model(AND1.variables(f)).size()).isEqualTo(2); - assertThat(s.satCall().model(AND1.variables(f)).evaluateLit(A)).isTrue(); - assertThat(s.satCall().model(AND1.variables(f)).evaluateLit(B)).isTrue(); + assertThat(s.satCall().model(AND1.variables(f)).assignment().evaluateLit(A)).isTrue(); + assertThat(s.satCall().model(AND1.variables(f)).assignment().evaluateLit(B)).isTrue(); s.add(NOT1); assertSolverUnsat(s); assertThat(s.satCall().model(NOT1.variables(f))).isNull(); @@ -132,10 +132,10 @@ public void testAnd2() { f.and(f.literal("a", true), f.literal("b", false), f.literal("c", true), f.literal("d", false))); s.add(prop); assertThat(s.satCall().model(prop.formula().variables(f)).size()).isEqualTo(4); - assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("a"))).isTrue(); - assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("b"))).isFalse(); - assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("c"))).isTrue(); - assertThat(s.satCall().model(prop.formula().variables(f)).evaluateLit(f.variable("d"))).isFalse(); + assertThat(s.satCall().model(prop.formula().variables(f)).assignment().evaluateLit(f.variable("a"))).isTrue(); + assertThat(s.satCall().model(prop.formula().variables(f)).assignment().evaluateLit(f.variable("b"))).isFalse(); + assertThat(s.satCall().model(prop.formula().variables(f)).assignment().evaluateLit(f.variable("c"))).isTrue(); + assertThat(s.satCall().model(prop.formula().variables(f)).assignment().evaluateLit(f.variable("d"))).isFalse(); } } @@ -158,9 +158,9 @@ public void testFormula1() throws ParserException { final Formula formula = parser.parse("(x => y) & (~x => y) & (y => z) & (z => ~x)"); s.add(formula); assertThat(s.satCall().model(formula.variables(f)).size()).isEqualTo(3); - assertThat(s.satCall().model(formula.variables(f)).evaluateLit(f.variable("x"))).isFalse(); - assertThat(s.satCall().model(formula.variables(f)).evaluateLit(f.variable("y"))).isTrue(); - assertThat(s.satCall().model(formula.variables(f)).evaluateLit(f.variable("z"))).isTrue(); + assertThat(s.satCall().model(formula.variables(f)).assignment().evaluateLit(f.variable("x"))).isFalse(); + assertThat(s.satCall().model(formula.variables(f)).assignment().evaluateLit(f.variable("y"))).isTrue(); + assertThat(s.satCall().model(formula.variables(f)).assignment().evaluateLit(f.variable("z"))).isTrue(); s.add(f.variable("x")); assertSolverUnsat(s); } @@ -237,9 +237,9 @@ public void testPartialModel() { relevantVars[0] = A; relevantVars[1] = B; assertSolverSat(s); - final Assignment relModel = s.satCall().model(Arrays.asList(relevantVars)); + final Model relModel = s.satCall().model(Arrays.asList(relevantVars)); assertThat(relModel.negativeLiterals().isEmpty()).isTrue(); - assertThat(relModel.literals().contains(C)).isFalse(); + assertThat(relModel.getLiterals().contains(C)).isFalse(); } } @@ -257,7 +257,7 @@ public void testVariableRemovedBySimplificationOccursInModel() throws ParserExce // when added to the solver assertThat(solver.sat()).isTrue(); assertThat(solver.underlyingSolver().knownVariables()).isEmpty(); - assertThat(variables(f, solver.satCall().model(List.of(a, b)).literals())).containsExactlyInAnyOrder(a, b); + assertThat(variables(f, solver.satCall().model(List.of(a, b)).getLiterals())).containsExactlyInAnyOrder(a, b); } @Test @@ -265,7 +265,7 @@ public void testUnknownVariableNotOccurringInModel() { final SATSolver solver = SATSolver.newSolver(f); final Variable a = f.variable("A"); solver.add(a); - assertThat(solver.satCall().model(f.variables("A", "X")).literals()).containsExactlyInAnyOrder(a, + assertThat(solver.satCall().model(f.variables("A", "X")).getLiterals()).containsExactlyInAnyOrder(a, f.literal("X", false)); } @@ -398,7 +398,6 @@ public void testTimeoutSATHandlerLarge() { final TimeoutHandler handler = new TimeoutHandler(1000L); final LNGResult result = s.satCall().handler(handler).sat(); assertThat(result.isSuccess()).isFalse(); - assertThat(result.getResult()).isNull(); } } @@ -414,9 +413,9 @@ public void testDimacsFiles() throws IOException { final File testFolder = new File("src/test/resources/sat"); final File[] files = testFolder.listFiles(); assert files != null; - for (final Supplier solverSupplier : solverSuppliers) { + for (final Function solverSupplier : solverSuppliers) { for (final File file : files) { - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); final String fileName = file.getName(); if (fileName.endsWith(".cnf")) { readCNF(solver, file); @@ -464,8 +463,8 @@ public void testTimeoutModelEnumerationHandlerWithUNSATInstance() { solver.add(formula); final var handler = new TimeoutHandler(1000L); final var me = meWithHandler(formula.variables(f)); - final LNGResult> assignments = solver.execute(me, handler); - assertThat(assignments.isSuccess()).isFalse(); + final LNGResult> models = solver.execute(me, handler); + assertThat(models.isSuccess()).isFalse(); } } @@ -497,9 +496,9 @@ public void testTimeoutModelEnumerationHandlerWithSATInstance2() { solver.add(f.exo(variables.subList(0, 5))); final var handler = new TimeoutHandler(50L); final var me = meWithHandler(variables.subList(0, 5)); - final LNGResult> assignments = solver.execute(me, handler); - assertThat(assignments.isSuccess()).isTrue(); - assertThat(assignments.getResult()).hasSize(5); + final LNGResult> models = solver.execute(me, handler); + assertThat(models.isSuccess()).isTrue(); + assertThat(models.getResult()).hasSize(5); } } @@ -608,13 +607,13 @@ public void testEmptyEnumeration() { @Test public void testNumberOfModelHandler() { - for (final Supplier solverSupplier : solverSuppliers) { + for (final Function solverSupplier : solverSuppliers) { final Variable[] lits = new Variable[100]; for (int j = 0; j < lits.length; j++) { lits[j] = f.variable("x" + j); } - SATSolver s = solverSupplier.get(); + SATSolver s = solverSupplier.apply(f); s.add(f.exo(lits)); var handler = new NumberOfModelsHandler(101); var me = ModelEnumerationFunction.builder(lits) @@ -627,7 +626,7 @@ public void testNumberOfModelHandler() { assertThat(m.positiveVariables().size()).isEqualTo(1); } - s = solverSupplier.get(); + s = solverSupplier.apply(f); s.add(f.exo(lits)); handler = new NumberOfModelsHandler(200); me = ModelEnumerationFunction.builder(lits) @@ -640,7 +639,7 @@ public void testNumberOfModelHandler() { assertThat(m.positiveVariables().size()).isEqualTo(1); } - s = solverSupplier.get(); + s = solverSupplier.apply(f); s.add(f.exo(lits)); handler = new NumberOfModelsHandler(50); me = ModelEnumerationFunction.builder(lits) @@ -654,7 +653,7 @@ public void testNumberOfModelHandler() { assertThat(m.positiveVariables().size()).isEqualTo(1); } - s = solverSupplier.get(); + s = solverSupplier.apply(f); s.add(f.exo(lits)); handler = new NumberOfModelsHandler(1); me = ModelEnumerationFunction.builder(lits) @@ -736,9 +735,9 @@ public void testUPZeroLiterals() throws ParserException { new TreeSet<>(Collections.singletonList(f.literal("b", false)))); expectedSubsets.put(parser.parse("(b | c) & ~b & (~c | d)"), new TreeSet<>(Arrays.asList( f.literal("b", false), f.literal("c", true), f.literal("d", true)))); - for (final Supplier solverSupplier : solverSuppliers) { + for (final Function solverSupplier : solverSuppliers) { for (final Formula formula : expectedSubsets.keySet()) { - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); solver.add(formula); final boolean res = solver.sat(); assertThat(res).isTrue(); @@ -754,11 +753,11 @@ public void testUPZeroLiteralsDimacsFiles() throws IOException { final File testFolder = new File("src/test/resources/sat"); final File[] files = testFolder.listFiles(); assert files != null; - for (final Supplier solverSupplier : solverSuppliers) { + for (final Function solverSupplier : solverSuppliers) { for (final File file : files) { final String fileName = file.getName(); if (fileName.endsWith(".cnf")) { - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); readCNF(solver, file); if (solver.sat()) { final SortedSet upZeroLiterals = solver.execute(UpZeroLiteralsFunction.get()); @@ -846,28 +845,28 @@ public void testSelectionOrderSimple01() throws ParserException { solver.add(formula); List selectionOrder = Arrays.asList(X, Y); - Assignment assignment = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); - assertThat(assignment.literals()).containsExactlyInAnyOrder(X, NY); - testLocalMinimum(solver, assignment, selectionOrder); - testHighestLexicographicalAssignment(solver, assignment, selectionOrder); + Model model = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); + assertThat(model.getLiterals()).containsExactlyInAnyOrder(X, NY); + testLocalMinimum(solver, model, selectionOrder); + testHighestLexicographicalModel(solver, model, selectionOrder); selectionOrder = Arrays.asList(Y, X); - assignment = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); - assertThat(assignment.literals()).containsExactlyInAnyOrder(Y, NX); - testLocalMinimum(solver, assignment, selectionOrder); - testHighestLexicographicalAssignment(solver, assignment, selectionOrder); + model = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); + assertThat(model.getLiterals()).containsExactlyInAnyOrder(Y, NX); + testLocalMinimum(solver, model, selectionOrder); + testHighestLexicographicalModel(solver, model, selectionOrder); selectionOrder = Collections.singletonList(NX); - assignment = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); - assertThat(assignment.literals()).containsExactlyInAnyOrder(Y, NX); - testLocalMinimum(solver, assignment, selectionOrder); - testHighestLexicographicalAssignment(solver, assignment, selectionOrder); + model = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); + assertThat(model.getLiterals()).containsExactlyInAnyOrder(Y, NX); + testLocalMinimum(solver, model, selectionOrder); + testHighestLexicographicalModel(solver, model, selectionOrder); selectionOrder = Arrays.asList(NY, NX); - assignment = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); - assertThat(assignment.literals()).containsExactlyInAnyOrder(X, NY); - testLocalMinimum(solver, assignment, selectionOrder); - testHighestLexicographicalAssignment(solver, assignment, selectionOrder); + model = solver.satCall().selectionOrder(selectionOrder).model(formula.variables(f)); + assertThat(model.getLiterals()).containsExactlyInAnyOrder(X, NY); + testLocalMinimum(solver, model, selectionOrder); + testHighestLexicographicalModel(solver, model, selectionOrder); } } @@ -883,10 +882,10 @@ public void testSelectionOrderSimple02() { for (int i = 0; i < 10; ++i) { assertThat(solver.satCall().selectionOrder(literals).sat().getResult()).isTrue(); - final Assignment assignment = solver.satCall().selectionOrder(literals).model(literals); - testLocalMinimum(solver, assignment, literals); - testHighestLexicographicalAssignment(solver, assignment, literals); - solver.add(assignment.blockingClause(f, literals)); + final Model model = solver.satCall().selectionOrder(literals).model(literals); + testLocalMinimum(solver, model, literals); + testHighestLexicographicalModel(solver, model, literals); + solver.add(model.blockingClause(f, literals)); } } } @@ -907,10 +906,10 @@ public void testSelectionOrderSimple03() { for (int i = 0; i < 10; ++i) { assertThat(solver.satCall().selectionOrder(selectionOrder02).sat().getResult()).isTrue(); - final Assignment assignment = solver.satCall().selectionOrder(selectionOrder02).model(literals); - testLocalMinimum(solver, assignment, selectionOrder02); - testHighestLexicographicalAssignment(solver, assignment, selectionOrder02); - solver.add(assignment.blockingClause(f, selectionOrder02)); + final Model model = solver.satCall().selectionOrder(selectionOrder02).model(literals); + testLocalMinimum(solver, model, selectionOrder02); + testHighestLexicographicalModel(solver, model, selectionOrder02); + solver.add(model.blockingClause(f, selectionOrder02)); } } } @@ -927,11 +926,11 @@ public void testDimacsFilesWithSelectionOrder() throws IOException { final File testFolder = new File("src/test/resources/sat"); final File[] files = testFolder.listFiles(); assert files != null; - for (final Supplier solverSupplier : solverSuppliers) { + for (final Function solverSupplier : solverSuppliers) { for (final File file : files) { final String fileName = file.getName(); if (fileName.endsWith(".cnf")) { - final SATSolver solver = solverSupplier.get(); + final SATSolver solver = solverSupplier.apply(f); readCNF(solver, file); final List selectionOrder = new ArrayList<>(); for (final Variable var : variables(f, solver.execute(FormulaOnSolverFunction.get()))) { @@ -942,10 +941,10 @@ public void testDimacsFilesWithSelectionOrder() throws IOException { final boolean res = solver.satCall().selectionOrder(selectionOrder).sat().getResult(); assertThat(res).isEqualTo(expectedResults.get(fileName)); if (expectedResults.get(fileName)) { - final Assignment assignment = + final Model model = solver.satCall().model(solver.underlyingSolver().knownVariables()); - testLocalMinimum(solver, assignment, selectionOrder); - testHighestLexicographicalAssignment(solver, assignment, selectionOrder); + testLocalMinimum(solver, model, selectionOrder); + testHighestLexicographicalModel(solver, model, selectionOrder); } } } @@ -991,9 +990,9 @@ private void compareFormulas(final Collection original, final Collectio assertThat(models1).hasSameElementsAs(models2); } - private void testLocalMinimum(final SATSolver solver, final Assignment assignment, + private void testLocalMinimum(final SATSolver solver, final Model model, final Collection relevantLiterals) { - final SortedSet literals = assignment.literals(); + final Set literals = new HashSet<>(model.getLiterals()); for (final Literal lit : relevantLiterals) { if (!literals.contains(lit)) { final SortedSet literalsWithFlip = new TreeSet<>(literals); @@ -1005,15 +1004,15 @@ private void testLocalMinimum(final SATSolver solver, final Assignment assignmen } /** - * Tests if the given satisfying assignment is the highest assignment in the + * Tests if the given satisfying model is the highest model in the * lexicographical order based on the given literals order. - * @param solver the solver with the loaded formulas - * @param assignment the satisfying assignment - * @param order the literals order + * @param solver the solver with the loaded formulas + * @param model the satisfying model + * @param order the literals order */ - private void testHighestLexicographicalAssignment(final SATSolver solver, final Assignment assignment, - final List order) { - final SortedSet literals = assignment.literals(); + private void testHighestLexicographicalModel(final SATSolver solver, final Model model, + final List order) { + final Set literals = new HashSet<>(model.getLiterals()); final List orderSublist = new ArrayList<>(); for (final Literal lit : order) { final boolean containsLit = literals.contains(lit); diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/SolverTestSet.java b/src/test/java/com/booleworks/logicng/solvers/sat/SolverTestSet.java index 0f94219c..f08f76de 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/SolverTestSet.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/SolverTestSet.java @@ -14,7 +14,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; -import java.util.function.Supplier; +import java.util.function.Function; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -25,18 +25,18 @@ static List solverTestSetForParameterizedTests(final Collection solverSupplierTestSetForParameterizedTests(final Collection variance, - final FormulaFactory f) { - return solverSupplierTestSet(variance, f).stream() - .map(s -> Arguments.of(s, solverDescription(s.get(), variance))).collect(Collectors.toList()); + static List solverSupplierTestSetForParameterizedTests(final Collection variance) { + return solverSupplierTestSet(variance).stream() + .map(s -> Arguments.of(s, solverDescription(s.apply(FormulaFactory.nonCaching()), variance))) + .collect(Collectors.toList()); } static List solverTestSet(final Collection variance, final FormulaFactory f) { - return solverSupplierTestSet(variance, f).stream().map(Supplier::get).collect(Collectors.toList()); + return solverSupplierTestSet(variance).stream().map(s -> s.apply(f)).collect(Collectors.toList()); } - static List> solverSupplierTestSet(final Collection variance, - final FormulaFactory f) { + static List> solverSupplierTestSet( + final Collection variance) { List currentList = List.of(SATSolverConfig.builder().build()); if (variance.contains(SATSolverConfigParam.PROOF_GENERATION)) { currentList = currentList.stream().flatMap(config -> Stream.of( @@ -70,7 +70,8 @@ static List> solverSupplierTestSet(final Collection (Supplier) () -> SATSolver.newSolver(f, config)) + return currentList.stream() + .map(config -> (Function) f -> SATSolver.newSolver(f, config)) .collect(Collectors.toList()); }