diff --git a/CHANGELOG.md b/CHANGELOG.md index 40ca17f6..5e21a70e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,20 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [2.6.0] - 2024-09-10 + +### Added + +- New class `OptimizationConfig` used to configure optimization computations in various algorithms. It allows to configure the following aspects: + - the `optimizationType` (either SAT-based optimization or a MaxSAT algorithm) + - the `maxSATConfig` to further configure the MaxSAT algorithm + - the `optimizationHandler` to use + - the `maxSATHandler` to use +- Added three new configuration options to `AdvancedSimplifierConfig`: + - `minimalDnfCover` determines whether the step for computing the minimal DNF cover should be performed. Default is `true`. + - `returnIntermediateResult` allows to return an intermediate result from the `AdvancedSimplifier` if the computation was aborted by a handler. Default is `false`. + - `optimizationConfig` can be used to configure the algorithms in the simplifier which perform optimizations, also the `OptimizationHandler handler` moved into this config + ## [2.5.1] - 2024-07-31 ### Changed diff --git a/README.md b/README.md index 9bc07c4b..abadb25c 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ LogicNG is released in the Maven Central Repository. To include it just add org.logicng logicng - 2.5.1 + 2.6.0 ``` diff --git a/pom.xml b/pom.xml index 70ebfd72..dfe8c374 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.5.1 + 2.6.0 bundle LogicNG diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java index b8a10202..81c024a9 100644 --- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java @@ -30,22 +30,32 @@ import static org.logicng.handlers.Handler.aborted; import static org.logicng.handlers.Handler.start; -import static org.logicng.handlers.OptimizationHandler.satHandler; +import static org.logicng.util.CollectionHelper.difference; +import static org.logicng.util.CollectionHelper.nullSafe; import org.logicng.datastructures.Assignment; import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; +import org.logicng.formulas.Literal; import org.logicng.formulas.Variable; +import org.logicng.handlers.Handler; +import org.logicng.handlers.MaxSATHandler; import org.logicng.handlers.OptimizationHandler; +import org.logicng.handlers.SATHandler; import org.logicng.propositions.Proposition; import org.logicng.propositions.StandardProposition; +import org.logicng.solvers.MaxSATSolver; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; import org.logicng.solvers.SolverState; import org.logicng.solvers.functions.OptimizationFunction; +import org.logicng.solvers.maxsat.OptimizationConfig; +import org.logicng.solvers.maxsat.algorithms.MaxSAT; +import org.logicng.util.FormulaHelper; -import java.util.Collections; +import java.util.ArrayList; +import java.util.Collection; import java.util.List; import java.util.Map; import java.util.Set; @@ -60,7 +70,7 @@ * Implementation is based on "Smallest MUS extraction with minimal * hitting set dualization" (Ignatiev, Previti, Liffiton, & * Marques-Silva, 2015). - * @version 2.1.0 + * @version 2.6.0 * @since 2.0.0 */ public final class SmusComputation { @@ -82,15 +92,18 @@ private SmusComputation() { * @param f the formula factory * @return the SMUS or {@code null} if the given propositions are satisfiable or the handler aborted the computation */ - public static

List

computeSmus(final List

propositions, final List additionalConstraints, final FormulaFactory f) { - return computeSmus(propositions, additionalConstraints, f, null); + public static

List

computeSmus( + final List

propositions, final List additionalConstraints, final FormulaFactory f) { + final OptimizationConfig cfg = OptimizationConfig.sat(null); + return computeSmus(propositions, additionalConstraints, f, cfg); } /** * Computes the SMUS for the given list of propositions modulo some additional constraint. *

- * The SMUS computation can be called with an {@link OptimizationHandler}. The given handler instance will be used for every subsequent - * * {@link org.logicng.solvers.functions.OptimizationFunction} call and the handler's SAT handler is used for every subsequent SAT call. + * The SMUS computation can be called with an {@link OptimizationHandler}. The given handler instance will be + * used for every subsequent {@link org.logicng.solvers.functions.OptimizationFunction} call and the handler's + * SAT handler is used for every subsequent SAT call. * @param

the subtype of the propositions * @param propositions the propositions * @param additionalConstraints the additional constraints @@ -98,35 +111,56 @@ public static

List

computeSmus(final List

proposit * @param handler the handler, can be {@code null} * @return the SMUS or {@code null} if the given propositions are satisfiable or the handler aborted the computation */ - public static

List

computeSmus(final List

propositions, final List additionalConstraints, final FormulaFactory f, - final OptimizationHandler handler) { + public static

List

computeSmus( + final List

propositions, + final List additionalConstraints, + final FormulaFactory f, + final OptimizationHandler handler) { + final OptimizationConfig cfg = OptimizationConfig.sat(handler); + return computeSmus(propositions, additionalConstraints, f, cfg); + } + + /** + * Computes the SMUS for the given list of propositions modulo some additional constraint. + *

+ * The SMUS computation can be called with an {@link OptimizationHandler}. The given handler instance will be used + * for every subsequent {@link org.logicng.solvers.functions.OptimizationFunction} call and the handler's SAT + * handler is used for every subsequent SAT call. + * @param

the subtype of the propositions + * @param propositions the propositions + * @param additionalConstraints the additional constraints + * @param f the formula factory + * @param config the optimization configuration + * @return the SMUS or {@code null} if the given propositions are satisfiable or the handler aborted the computation + */ + public static

List

computeSmus( + final List

propositions, + final List additionalConstraints, + final FormulaFactory f, + final OptimizationConfig config) { + final Handler handler = getHandler(config); start(handler); - final SATSolver growSolver = MiniSat.miniSat(f); - growSolver.add(additionalConstraints == null ? Collections.singletonList(f.verum()) : additionalConstraints); - final Map propositionMapping = new TreeMap<>(); - for (final P proposition : propositions) { - final Variable selector = f.variable(PROPOSITION_SELECTOR + propositionMapping.size()); - propositionMapping.put(selector, proposition); - growSolver.add(f.equivalence(selector, proposition.formula())); - } - final boolean sat = growSolver.sat(satHandler(handler), propositionMapping.keySet()) == Tristate.TRUE; - if (sat || aborted(handler)) { + final OptSolver growSolver = OptSolver.create(f, config); + growSolver.addConstraint(nullSafe(additionalConstraints)); + final Map propositionMapping = createPropositionsMapping(propositions, growSolver, f); + final boolean sat = growSolver.sat(propositionMapping.keySet()); + if (sat || growSolver.aborted()) { return null; } - final SATSolver hSolver = MiniSat.miniSat(f); + final OptSolver hSolver = OptSolver.create(f, config); while (true) { - final SortedSet h = minimumHs(hSolver, propositionMapping.keySet(), handler); + final SortedSet h = hSolver.minimize(propositionMapping.keySet()); if (h == null || aborted(handler)) { return null; } - final SortedSet c = grow(growSolver, h, propositionMapping.keySet(), handler); + final SortedSet c = grow(growSolver, h, propositionMapping.keySet()); if (aborted(handler)) { return null; } if (c == null) { return h.stream().map(propositionMapping::get).collect(Collectors.toList()); } - hSolver.add(f.or(c)); + hSolver.addConstraint(f.or(c)); } } @@ -137,8 +171,12 @@ public static

List

computeSmus(final List

proposit * @param f the formula factory * @return the SMUS or {@code null} if the given propositions are satisfiable or the handler aborted the computation */ - public static List computeSmusForFormulas(final List formulas, final List additionalConstraints, final FormulaFactory f) { - return computeSmusForFormulas(formulas, additionalConstraints, f, null); + public static List computeSmusForFormulas( + final List formulas, + final List additionalConstraints, + final FormulaFactory f) { + final OptimizationConfig cfg = OptimizationConfig.sat(null); + return computeSmusForFormulas(formulas, additionalConstraints, f, cfg); } /** @@ -149,36 +187,210 @@ public static List computeSmusForFormulas(final List formulas, * @param handler the SMUS handler, can be {@code null} * @return the SMUS or {@code null} if the given propositions are satisfiable or the handler aborted the computation */ - public static List computeSmusForFormulas(final List formulas, final List additionalConstraints, final FormulaFactory f, - final OptimizationHandler handler) { + public static List computeSmusForFormulas( + final List formulas, + final List additionalConstraints, + final FormulaFactory f, + final OptimizationHandler handler) { + final OptimizationConfig cfg = OptimizationConfig.sat(handler); + return computeSmusForFormulas(formulas, additionalConstraints, f, cfg); + } + + /** + * Computes the SMUS for the given list of formulas and some additional constraints. + * @param formulas the formulas + * @param additionalConstraints the additional constraints + * @param f the formula factory + * @param config the optimization configuration + * @return the SMUS or {@code null} if the given propositions are satisfiable or the handler aborted the computation + */ + public static List computeSmusForFormulas( + final List formulas, + final List additionalConstraints, + final FormulaFactory f, + final OptimizationConfig config) { final List props = formulas.stream().map(StandardProposition::new).collect(Collectors.toList()); - final List smus = computeSmus(props, additionalConstraints, f, handler); + final List smus = computeSmus(props, additionalConstraints, f, config); return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList()); } - private static SortedSet minimumHs(final SATSolver hSolver, final Set variables, final OptimizationHandler handler) { - final Assignment minimumHsModel = hSolver.execute(OptimizationFunction.builder() - .handler(handler) - .literals(variables) - .minimize().build()); - return aborted(handler) ? null : new TreeSet<>(minimumHsModel.positiveVariables()); + private static Handler getHandler(final OptimizationConfig config) { + return config.getOptimizationType() == OptimizationConfig.OptimizationType.SAT_OPTIMIZATION + ? config.getOptimizationHandler() + : config.getMaxSATHandler(); } - private static SortedSet grow(final SATSolver growSolver, final SortedSet h, final Set variables, final OptimizationHandler handler) { - final SolverState solverState = growSolver.saveState(); - growSolver.add(h); - final Assignment maxModel = growSolver.execute(OptimizationFunction.builder() - .handler(handler) - .literals(variables) - .maximize().build()); - if (maxModel == null || aborted(handler)) { + private static

Map createPropositionsMapping( + final List

propositions, final OptSolver solver, final FormulaFactory f) { + final Map propositionMapping = new TreeMap<>(); + for (final P proposition : propositions) { + final Variable selector = f.variable(PROPOSITION_SELECTOR + propositionMapping.size()); + propositionMapping.put(selector, proposition); + solver.addConstraint(f.equivalence(selector, proposition.formula())); + } + return propositionMapping; + } + + private static SortedSet grow(final OptSolver growSolver, final SortedSet h, final Set variables) { + growSolver.saveState(); + growSolver.addConstraint(h); + final SortedSet maxModel = growSolver.maximize(variables); + if (maxModel == null) { return null; - } else { - final List maximumSatisfiableSet = maxModel.positiveVariables(); - growSolver.loadState(solverState); - final SortedSet minimumCorrectionSet = new TreeSet<>(variables); - maximumSatisfiableSet.forEach(minimumCorrectionSet::remove); - return minimumCorrectionSet; + } + growSolver.loadState(); + return difference(variables, maxModel, TreeSet::new); + } + + private abstract static class OptSolver { + protected final FormulaFactory f; + protected final OptimizationConfig config; + + OptSolver(final FormulaFactory f, final OptimizationConfig config) { + this.f = f; + this.config = config; + } + + public static OptSolver create(final FormulaFactory f, final OptimizationConfig config) { + if (config.getOptimizationType() == OptimizationConfig.OptimizationType.SAT_OPTIMIZATION) { + return new SatOptSolver(f, config); + } else { + return new MaxSatOptSolver(f, config); + } + } + + abstract void addConstraint(final Formula formula); + + abstract void addConstraint(final Collection formulas); + + abstract boolean sat(final Collection variables); + + abstract void saveState(); + + abstract void loadState(); + + abstract SortedSet maximize(final Collection targetLiterals); + + SortedSet minimize(final Collection targetLiterals) { + return maximize(FormulaHelper.negateLiterals(targetLiterals, TreeSet::new)); + } + + abstract boolean aborted(); + } + + private static class SatOptSolver extends OptSolver { + private final MiniSat solver; + private SolverState state; + + SatOptSolver(final FormulaFactory f, final OptimizationConfig config) { + super(f, config); + this.solver = MiniSat.miniSat(f); + this.state = null; + } + + @Override + void addConstraint(final Formula formula) { + this.solver.add(formula); + } + + @Override + void addConstraint(final Collection formulas) { + this.solver.add(formulas); + } + + @Override + boolean sat(final Collection variables) { + final SATHandler satHandler = this.config.getOptimizationHandler() == null ? null : this.config.getOptimizationHandler().satHandler(); + return this.solver.sat(satHandler, variables) == Tristate.TRUE; + } + + @Override + void saveState() { + this.state = this.solver.saveState(); + } + + @Override + void loadState() { + if (this.state != null) { + this.solver.loadState(this.state); + this.state = null; + } + } + + @Override + SortedSet maximize(final Collection targetLiterals) { + final OptimizationFunction optFunction = OptimizationFunction.builder() + .handler(this.config.getOptimizationHandler()) + .literals(targetLiterals) + .maximize().build(); + final Assignment model = this.solver.execute(optFunction); + return model == null || aborted() ? null : new TreeSet<>(model.positiveVariables()); + } + + @Override + boolean aborted() { + return Handler.aborted(this.config.getOptimizationHandler()); + } + } + + private static class MaxSatOptSolver extends OptSolver { + private List constraints; + private int saveIdx; + + public MaxSatOptSolver(final FormulaFactory f, final OptimizationConfig config) { + super(f, config); + this.constraints = new ArrayList<>(); + this.saveIdx = -1; + } + + @Override + void addConstraint(final Formula formula) { + this.constraints.add(formula); + } + + @Override + void addConstraint(final Collection formulas) { + this.constraints.addAll(formulas); + } + + @Override + boolean sat(final Collection variables) { + final SATHandler satHandler = this.config.getMaxSATHandler() == null ? null : this.config.getMaxSATHandler().satHandler(); + final SATSolver satSolver = MiniSat.miniSat(this.f); + satSolver.add(this.constraints); + return satSolver.sat(satHandler, variables) == Tristate.TRUE; + } + + @Override + void saveState() { + this.saveIdx = this.constraints.size(); + } + + @Override + void loadState() { + if (this.saveIdx != -1) { + this.constraints = this.constraints.subList(0, this.saveIdx); + this.saveIdx = -1; + } + } + + @Override + SortedSet maximize(final Collection targetLiterals) { + final MaxSATSolver maxSatSolver = this.config.genMaxSATSolver(this.f); + this.constraints.forEach(maxSatSolver::addHardFormula); + for (final Literal lit : targetLiterals) { + maxSatSolver.addSoftFormula(lit, 1); + } + final MaxSATHandler handler = this.config.getMaxSATHandler(); + final MaxSAT.MaxSATResult result = maxSatSolver.solve(handler); + return result == MaxSAT.MaxSATResult.UNDEF || result == MaxSAT.MaxSATResult.UNSATISFIABLE || aborted() + ? null + : new TreeSet<>(maxSatSolver.model().positiveVariables()); + } + + @Override + boolean aborted() { + return Handler.aborted(this.config.getMaxSATHandler()); } } } diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java index a3e433af..4eab4d82 100644 --- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java @@ -39,10 +39,14 @@ import org.logicng.formulas.Literal; import org.logicng.formulas.Variable; import org.logicng.handlers.OptimizationHandler; +import org.logicng.handlers.SATHandler; +import org.logicng.solvers.MaxSATSolver; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; import org.logicng.solvers.functions.OptimizationFunction; -import org.logicng.solvers.sat.MiniSatConfig; +import org.logicng.solvers.maxsat.OptimizationConfig; +import org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType; +import org.logicng.solvers.maxsat.algorithms.MaxSAT; import org.logicng.transformations.LiteralSubstitution; import org.logicng.util.FormulaHelper; import org.logicng.util.Pair; @@ -69,7 +73,7 @@ * {@link #getWithMaximization()} and another which searches for minimum models * {@link #getWithMaximization()}. From experience, the one with minimum models usually * outperforms the one with maximum models. - * @version 2.1.0 + * @version 2.6.0 * @since 2.0.0 */ public final class PrimeCompiler { @@ -110,7 +114,7 @@ public static PrimeCompiler getWithMaximization() { * @return the prime result */ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type) { - return compute(formula, type, null); + return compute(formula, type, OptimizationConfig.sat(null)); } /** @@ -127,12 +131,41 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType * @param handler an optimization handler, can be {@code null} * @return the prime result or null if the computation was aborted by the handler */ - public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type, final OptimizationHandler handler) { - start(handler); + public PrimeResult compute( + final Formula formula, + final PrimeResult.CoverageType type, + final OptimizationHandler handler) { + return compute(formula, type, OptimizationConfig.sat(handler)); + } + + /** + * Computes prime implicants and prime implicates for a given formula. + * The coverage type specifies if the implicants or the implicates will + * be complete, the other one will still be a cover of the given formula. + *

+ * The prime compiler can be called with an {@link OptimizationHandler}. + * The given handler instance will be used for every subsequent + * {@link org.logicng.solvers.functions.OptimizationFunction} call and + * the handler's SAT handler is used for every subsequent SAT call. + * @param formula the formula + * @param type the coverage type + * @param cfg the optimization configuration + * @return the prime result or null if the computation was aborted by the handler + */ + public PrimeResult compute( + final Formula formula, + final PrimeResult.CoverageType type, + final OptimizationConfig cfg) { + final boolean completeImplicants = type == PrimeResult.CoverageType.IMPLICANTS_COMPLETE; final Formula formulaForComputation = completeImplicants ? formula : formula.negate(); - final Pair>, List>> result = computeGeneric(formulaForComputation, handler); - if (result == null || aborted(handler)) { + final Pair>, List>> result; + if (cfg.getOptimizationType() == OptimizationType.SAT_OPTIMIZATION) { + result = computeSAT(formulaForComputation, cfg.getOptimizationHandler()); + } else { + result = computeMaxSAT(formulaForComputation, cfg); + } + if (result == null) { return null; } return new PrimeResult( @@ -141,12 +174,15 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type); } - private Pair>, List>> computeGeneric(final Formula formula, final OptimizationHandler handler) { + private Pair>, List>> computeSAT( + final Formula formula, + final OptimizationHandler handler) { + start(handler); final FormulaFactory f = formula.factory(); final SubstitutionResult sub = createSubstitution(formula); - final SATSolver hSolver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()); + final SATSolver hSolver = MiniSat.miniSat(f); hSolver.add(sub.constraintFormula); - final SATSolver fSolver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()); + final SATSolver fSolver = MiniSat.miniSat(f); fSolver.add(formula.negate()); final NaivePrimeReduction primeReduction = new NaivePrimeReduction(formula); final List> primeImplicants = new ArrayList<>(); @@ -167,7 +203,9 @@ private Pair>, List>> computeGeneric( return null; } if (fSat == Tristate.FALSE) { - final SortedSet primeImplicant = this.computeWithMaximization ? primeReduction.reduceImplicant(fModel.literals(), satHandler(handler)) : fModel.literals(); + final SortedSet primeImplicant = this.computeWithMaximization + ? primeReduction.reduceImplicant(fModel.literals(), satHandler(handler)) + : fModel.literals(); if (primeImplicant == null || aborted(handler)) { return null; } @@ -192,6 +230,66 @@ private Pair>, List>> computeGeneric( } } + private Pair>, List>> computeMaxSAT( + final Formula formula, + final OptimizationConfig cfg) { + start(cfg.getMaxSATHandler()); + final SATHandler handler = cfg.getMaxSATHandler() == null ? null : cfg.getMaxSATHandler().satHandler(); + final FormulaFactory f = formula.factory(); + final SubstitutionResult sub = createSubstitution(formula); + final List hSolverConstraints = new ArrayList<>(); + hSolverConstraints.add(sub.constraintFormula); + final SATSolver fSolver = MiniSat.miniSat(f); + fSolver.add(formula.negate()); + final NaivePrimeReduction primeReduction = new NaivePrimeReduction(formula); + final List> primeImplicants = new ArrayList<>(); + final List> primeImplicates = new ArrayList<>(); + while (true) { + final MaxSATSolver hSolver = cfg.genMaxSATSolver(f); + hSolverConstraints.forEach(hSolver::addHardFormula); + sub.newVar2oldLit.keySet().forEach(it -> + hSolver.addSoftFormula(f.literal(it.name(), this.computeWithMaximization), 1)); + final MaxSAT.MaxSATResult result = hSolver.solve(cfg.getMaxSATHandler()); + if (result == MaxSAT.MaxSATResult.UNDEF || aborted(cfg.getMaxSATHandler())) { + return null; + } + final Assignment hModel = hSolver.model(); + if (hModel == null) { + return new Pair<>(primeImplicants, primeImplicates); + } + final Assignment fModel = transformModel(hModel, sub.newVar2oldLit); + final Tristate fSat = fSolver.sat(handler, fModel.literals()); + if (aborted(handler)) { + return null; + } + if (fSat == Tristate.FALSE) { + final SortedSet primeImplicant = this.computeWithMaximization + ? primeReduction.reduceImplicant(fModel.literals(), handler) + : fModel.literals(); + if (primeImplicant == null || aborted(handler)) { + return null; + } + primeImplicants.add(primeImplicant); + final List blockingClause = new ArrayList<>(); + for (final Literal lit : primeImplicant) { + blockingClause.add(((Literal) lit.transform(sub.substitution)).negate()); + } + hSolverConstraints.add(f.or(blockingClause)); + } else { + final SortedSet implicate = new TreeSet<>(); + for (final Literal lit : (this.computeWithMaximization ? fModel : fSolver.model(formula.variables())).literals()) { + implicate.add(lit.negate()); + } + final SortedSet primeImplicate = primeReduction.reduceImplicate(implicate, handler); + if (primeImplicate == null || aborted(handler)) { + return null; + } + primeImplicates.add(primeImplicate); + hSolverConstraints.add(f.or(primeImplicate).transform(sub.substitution)); + } + } + } + private SubstitutionResult createSubstitution(final Formula formula) { final Map newVar2oldLit = new HashMap<>(); final LiteralSubstitution substitution = new LiteralSubstitution(); diff --git a/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java new file mode 100644 index 00000000..5627acb5 --- /dev/null +++ b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java @@ -0,0 +1,205 @@ +package org.logicng.solvers.maxsat; + +import org.logicng.formulas.FormulaFactory; +import org.logicng.handlers.MaxSATHandler; +import org.logicng.handlers.OptimizationHandler; +import org.logicng.handlers.SATHandler; +import org.logicng.solvers.MaxSATSolver; +import org.logicng.solvers.maxsat.algorithms.MaxSATConfig; + +import java.util.Objects; + +/** + * Configuration for optimization via a SAT or MaxSAT solver. + *

+ * Some algorithms use optimization internally. If they use many incremental + * solving steps, they usually use the SAT solver based + * {@link org.logicng.solvers.functions.OptimizationFunction}. For some cases + * however it can be more performant to use a MaxSAT solver based optimization + * with the drawback of generating the solver again in each step. + *

+ * These algorithms can be configured with this config object. + * @version 2.6.0 + * @since 2.6.0 + */ +public class OptimizationConfig { + public enum OptimizationType { + SAT_OPTIMIZATION, + MAXSAT_INCWBO, + MAXSAT_LINEAR_SU, + MAXSAT_LINEAR_US, + MAXSAT_MSU3, + MAXSAT_OLL, + MAXSAT_WBO, + } + + private final OptimizationType optimizationType; + private final MaxSATConfig maxSATConfig; + private final OptimizationHandler optimizationHandler; + private final MaxSATHandler maxSATHandler; + + private OptimizationConfig( + final OptimizationType optType, + final MaxSATConfig maxConfig, + final OptimizationHandler optHandler, + final MaxSATHandler maxHandler + ) { + this.optimizationType = optType; + this.maxSATConfig = maxConfig; + this.optimizationHandler = optHandler; + this.maxSATHandler = maxHandler; + } + + /** + * Generate a MaxSAT solver based configuration + * @param optType the optimization type (MaxSAT algorithm) + * @param maxConfig the optional MaxSAT solver configuration + * @param maxHandler the optional MaxSAT solver handler + * @return the configuration + */ + public static OptimizationConfig maxsat( + final OptimizationType optType, + final MaxSATConfig maxConfig, + final MaxSATHandler maxHandler + ) { + if (optType == OptimizationType.SAT_OPTIMIZATION) { + throw new IllegalArgumentException("SAT Optimization cannot be parametrized with MaxSat config and handler"); + } + return new OptimizationConfig(optType, maxConfig, null, maxHandler); + } + + /** + * Generate a SAT solver based configuration + * @param optHandler the optional optimization handler + * @return the configuration + */ + public static OptimizationConfig sat(final OptimizationHandler optHandler) { + return new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, optHandler, null); + } + + /** + * Returns the optimization type. + * @return the optimization type + */ + public OptimizationType getOptimizationType() { + return this.optimizationType; + } + + /** + * Returns the optional MaxSAT configuration + * @return the optional MaxSAT configuration + */ + public MaxSATConfig getMaxSATConfig() { + return this.maxSATConfig; + } + + /** + * Returns the optional optimization handler. + * @return the optional optimization handler + */ + public OptimizationHandler getOptimizationHandler() { + return this.optimizationHandler; + } + + /** + * Returns the optional MaxSAT handler. + * @return the optional MaxSAT handler + */ + public MaxSATHandler getMaxSATHandler() { + return this.maxSATHandler; + } + + /** + * Generates a MaxSAT solver with the current configuration. + * @param f the formula factory + * @return the MAxSAT solver + */ + public MaxSATSolver genMaxSATSolver(final FormulaFactory f) { + switch (this.optimizationType) { + case MAXSAT_INCWBO: + return this.maxSATConfig == null ? MaxSATSolver.incWBO(f) : MaxSATSolver.incWBO(f, this.maxSATConfig); + case MAXSAT_LINEAR_SU: + return this.maxSATConfig == null ? MaxSATSolver.linearSU(f) : MaxSATSolver.linearSU(f, this.maxSATConfig); + case MAXSAT_LINEAR_US: + return this.maxSATConfig == null ? MaxSATSolver.linearUS(f) : MaxSATSolver.linearUS(f, this.maxSATConfig); + case MAXSAT_MSU3: + return this.maxSATConfig == null ? MaxSATSolver.msu3(f) : MaxSATSolver.msu3(f, this.maxSATConfig); + case MAXSAT_OLL: + return this.maxSATConfig == null ? MaxSATSolver.oll(f) : MaxSATSolver.oll(f, this.maxSATConfig); + case MAXSAT_WBO: + return this.maxSATConfig == null ? MaxSATSolver.wbo(f) : MaxSATSolver.wbo(f, this.maxSATConfig); + default: + throw new IllegalArgumentException("Not a valid MaxSAT algorithm: " + this.optimizationType); + } + } + + /** + * Starts this config's handler (if present) + */ + public void startHandler() { + if (this.optimizationHandler != null) { + this.optimizationHandler.started(); + } + if (this.maxSATHandler != null) { + this.maxSATHandler.started(); + } + } + + /** + * Return the SAT handler of this config's handler (if present) + * @return the SAT handler + */ + public SATHandler satHandler() { + if (this.optimizationHandler != null) { + return this.optimizationHandler.satHandler(); + } + if (this.maxSATHandler != null) { + return this.maxSATHandler.satHandler(); + } + return null; + } + + /** + * Returns whether this config's handler (if present) was aborted. + * @return whether this config's handler was aborted + */ + public boolean aborted() { + if (this.optimizationHandler != null) { + return this.optimizationHandler.aborted(); + } + if (this.maxSATHandler != null) { + return this.maxSATHandler.aborted(); + } + return false; + } + + @Override + public boolean equals(final Object object) { + if (this == object) { + return true; + } + if (object == null || getClass() != object.getClass()) { + return false; + } + final OptimizationConfig that = (OptimizationConfig) object; + return this.optimizationType == that.optimizationType && + Objects.equals(this.maxSATConfig, that.maxSATConfig) && + Objects.equals(this.optimizationHandler, that.optimizationHandler) && + Objects.equals(this.maxSATHandler, that.maxSATHandler); + } + + @Override + public int hashCode() { + return Objects.hash(this.optimizationType, this.maxSATConfig, this.optimizationHandler, this.maxSATHandler); + } + + @Override + public String toString() { + return "OptimizationConfig{" + + "optimizationType=" + this.optimizationType + + ", maxSATConfig=" + this.maxSATConfig + + ", optimizationHandler=" + this.optimizationHandler + + ", maxSATHandler=" + this.maxSATHandler + + '}'; + } +} diff --git a/src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java b/src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java index db3e9336..01bfa499 100644 --- a/src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java +++ b/src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java @@ -404,7 +404,6 @@ protected MaxSATResult weightSearch() { } protected int incComputeCostModel(final LNGBooleanVector currentModel) { - assert currentModel.size() != 0; int currentCost = 0; for (int i = 0; i < nSoft(); i++) { boolean unsatisfied = true; @@ -413,7 +412,6 @@ protected int incComputeCostModel(final LNGBooleanVector currentModel) { unsatisfied = false; continue; } - assert var(this.softClauses.get(i).clause().get(j)) < currentModel.size(); if ((sign(this.softClauses.get(i).clause().get(j)) && !currentModel.get(var(this.softClauses.get(i).clause().get(j)))) || (!sign(this.softClauses.get(i).clause().get(j)) && currentModel.get(var(this.softClauses.get(i).clause().get(j))))) { unsatisfied = false; diff --git a/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java b/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java index b0bc8fec..3104dce4 100644 --- a/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java +++ b/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java @@ -329,8 +329,6 @@ public MiniSatStyleSolver newSATSolver() { * @param currentModel the model found by the solver */ public void saveModel(final LNGBooleanVector currentModel) { - assert this.nbInitialVariables != 0; - assert currentModel.size() != 0; this.model.clear(); for (int i = 0; i < this.nbInitialVariables; i++) { this.model.push(currentModel.get(i)); @@ -346,7 +344,6 @@ public void saveModel(final LNGBooleanVector currentModel) { * @return the cost of the given model */ public int computeCostModel(final LNGBooleanVector currentModel, final int weight) { - assert currentModel.size() != 0; int currentCost = 0; for (int i = 0; i < nSoft(); i++) { boolean unsatisfied = true; @@ -355,7 +352,6 @@ public int computeCostModel(final LNGBooleanVector currentModel, final int weigh unsatisfied = false; continue; } - assert var(this.softClauses.get(i).clause().get(j)) < currentModel.size(); if ((sign(this.softClauses.get(i).clause().get(j)) && !currentModel.get(var(this.softClauses.get(i).clause().get(j)))) || (!sign(this.softClauses.get(i).clause().get(j)) && currentModel.get(var(this.softClauses.get(i).clause().get(j))))) { unsatisfied = false; diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java index 7d57439c..5e28a285 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java @@ -28,10 +28,6 @@ package org.logicng.transformations.simplification; -import static org.logicng.handlers.Handler.aborted; -import static org.logicng.handlers.Handler.start; -import static org.logicng.handlers.OptimizationHandler.satHandler; - import org.logicng.backbones.Backbone; import org.logicng.backbones.BackboneGeneration; import org.logicng.backbones.BackboneType; @@ -45,6 +41,7 @@ import org.logicng.handlers.OptimizationHandler; import org.logicng.primecomputation.PrimeCompiler; import org.logicng.primecomputation.PrimeResult; +import org.logicng.solvers.maxsat.OptimizationConfig; import org.logicng.util.FormulaHelper; import java.util.ArrayList; @@ -72,7 +69,7 @@ * * The first and the last two steps can be configured using the {@link AdvancedSimplifierConfig}. Also, the handler and the rating * function can be configured. If no rating function is specified, the {@link DefaultRatingFunction} is chosen. - * @version 2.3.0 + * @version 2.6.0 * @since 2.0.0 */ public final class AdvancedSimplifier implements FormulaTransformation { @@ -126,15 +123,16 @@ public Formula apply(final Formula formula, final boolean cache) { final AdvancedSimplifierConfig config = this.initConfig != null ? this.initConfig : (AdvancedSimplifierConfig) formula.factory().configurationFor(ConfigurationType.ADVANCED_SIMPLIFIER); - start(config.handler); + final OptimizationConfig cfg = config.optimizationConfig; + cfg.startHandler(); final FormulaFactory f = formula.factory(); Formula simplified = formula; final SortedSet backboneLiterals = new TreeSet<>(); if (config.restrictBackbone) { final Backbone backbone = BackboneGeneration - .compute(Collections.singletonList(formula), formula.variables(), BackboneType.POSITIVE_AND_NEGATIVE, satHandler(config.handler)); - if (backbone == null || aborted(config.handler)) { - return null; + .compute(Collections.singletonList(formula), formula.variables(), BackboneType.POSITIVE_AND_NEGATIVE, cfg.satHandler()); + if (backbone == null || cfg.aborted()) { + return config.returnIntermediateResult ? formula : null; } if (!backbone.isSat()) { return f.falsum(); @@ -142,18 +140,18 @@ public Formula apply(final Formula formula, final boolean cache) { backboneLiterals.addAll(backbone.getCompleteBackbone()); simplified = formula.restrict(new Assignment(backboneLiterals)); } - final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); - if (simplifyMinDnf == null) { - return null; + if (config.minimalDnfCover) { + final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); + if (simplifyMinDnf == null) { + return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null; + } + simplified = simplifyWithRating(simplified, simplifyMinDnf, config); } - simplified = simplifyWithRating(simplified, simplifyMinDnf, config); if (config.factorOut) { final Formula factoredOut = simplified.transform(new FactorOutSimplifier(config.ratingFunction)); simplified = simplifyWithRating(simplified, factoredOut, config); } - if (config.restrictBackbone) { - simplified = f.and(f.and(backboneLiterals), simplified); - } + simplified = addLiterals(simplified, backboneLiterals); if (config.simplifyNegations) { final Formula negationSimplified = simplified.transform(NegationSimplifier.get()); simplified = simplifyWithRating(simplified, negationSimplified, config); @@ -161,20 +159,24 @@ public Formula apply(final Formula formula, final boolean cache) { return simplified; } - private Formula computeMinDnf(final FormulaFactory f, Formula simplified, final AdvancedSimplifierConfig config) { + private static Formula addLiterals(final Formula formula, final SortedSet literals) { + final FormulaFactory f = formula.factory(); + return f.and(f.and(literals), formula); + } + + private Formula computeMinDnf(final FormulaFactory f, final Formula simplified, final AdvancedSimplifierConfig config) { final PrimeResult primeResult = - PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.handler); - if (primeResult == null || aborted(config.handler)) { + PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.optimizationConfig); + if (primeResult == null || config.optimizationConfig.aborted()) { return null; } final List> primeImplicants = primeResult.getPrimeImplicants(); final List minimizedPIs = SmusComputation.computeSmusForFormulas(negateAllLiterals(primeImplicants, f), - Collections.singletonList(simplified), f, config.handler); - if (minimizedPIs == null || aborted(config.handler)) { + Collections.singletonList(simplified), f, config.optimizationConfig); + if (minimizedPIs == null || config.optimizationConfig.aborted()) { return null; } - simplified = f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList())); - return simplified; + return f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList())); } private List negateAllLiterals(final Collection> literalSets, final FormulaFactory f) { diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java index f3f1af55..a89733e3 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -31,29 +31,34 @@ import org.logicng.configurations.Configuration; import org.logicng.configurations.ConfigurationType; import org.logicng.handlers.OptimizationHandler; +import org.logicng.solvers.maxsat.OptimizationConfig; /** * The configuration object for the {@link AdvancedSimplifier}. - * @version 2.3.0 + * @version 2.6.0 * @since 2.3.0 */ public class AdvancedSimplifierConfig extends Configuration { boolean restrictBackbone; + boolean minimalDnfCover; boolean factorOut; boolean simplifyNegations; + boolean returnIntermediateResult; RatingFunction ratingFunction; - OptimizationHandler handler; + OptimizationConfig optimizationConfig; @Override public String toString() { return "AdvancedSimplifierConfig{" + "restrictBackbone=" + this.restrictBackbone + + ", minimalDnfCover=" + this.minimalDnfCover + ", factorOut=" + this.factorOut + ", simplifyNegations=" + this.simplifyNegations + + ", returnIntermediateResult=" + this.returnIntermediateResult + ", ratingFunction=" + this.ratingFunction + - ", handler=" + this.handler + + ", optimizationConfig=" + this.optimizationConfig + '}'; } @@ -64,10 +69,12 @@ public String toString() { private AdvancedSimplifierConfig(final Builder builder) { super(ConfigurationType.ADVANCED_SIMPLIFIER); this.restrictBackbone = builder.restrictBackbone; + this.minimalDnfCover = builder.minimalDnfCover; this.factorOut = builder.factorOut; this.simplifyNegations = builder.simplifyNegations; + this.returnIntermediateResult = builder.returnIntermediateResult; this.ratingFunction = builder.ratingFunction; - this.handler = builder.handler; + this.optimizationConfig = builder.optimizationConfig; } /** @@ -83,18 +90,21 @@ public static Builder builder() { */ public static class Builder { - boolean restrictBackbone = true; - boolean factorOut = true; - boolean simplifyNegations = true; - private RatingFunction ratingFunction = new DefaultRatingFunction(); - private OptimizationHandler handler = null; + private boolean restrictBackbone = true; + private boolean minimalDnfCover = true; + private boolean factorOut = true; + private boolean simplifyNegations = true; + private boolean returnIntermediateResult = false; + private RatingFunction ratingFunction = DefaultRatingFunction.get(); + private OptimizationConfig optimizationConfig = OptimizationConfig.sat(null); private Builder() { // Initialize only via factory } /** - * Sets the flag for whether the formula should be restricted with the backbone. The default is 'true'. + * Sets the flag for whether the formula should be restricted with the + * backbone. The default is 'true'. * @param restrictBackbone flag for the restriction * @return the current builder */ @@ -104,7 +114,19 @@ public Builder restrictBackbone(final boolean restrictBackbone) { } /** - * Sets the flag for whether the formula should be factorized. The default is 'true'. + * Sets the flag for whether a minimal DNF cover should be computed. The + * default is 'true'. + * @param minimalDnfCover flag for the minimal DNF cover computation + * @return the current builder + */ + public Builder minimalDnfCover(final boolean minimalDnfCover) { + this.minimalDnfCover = minimalDnfCover; + return this; + } + + /** + * Sets the flag for whether the formula should be factorized. The + * default is 'true'. * @param factorOut flag for the factorisation * @return the current builder */ @@ -114,7 +136,8 @@ public Builder factorOut(final boolean factorOut) { } /** - * Sets the flag for whether negations shall be simplified. The default is 'true'. + * Sets the flag for whether negations shall be simplified. The + * default is 'true'. * @param simplifyNegations flag * @return the current builder */ @@ -124,8 +147,11 @@ public Builder simplifyNegations(final boolean simplifyNegations) { } /** - * Sets the rating function. The aim of the simplification is to minimize the formula with respect to this rating function, - * e.g. finding a formula with a minimal number of symbols when represented as string. The default is the {@code DefaultRatingFunction}. + * Sets the rating function. The aim of the simplification is to + * minimize the formula with respect to this rating function, + * e.g. finding a formula with a minimal number of symbols when + * represented as string. The default is the + * {@code DefaultRatingFunction}. * @param ratingFunction the desired rating function * @return the current builder */ @@ -135,12 +161,37 @@ public Builder ratingFunction(final RatingFunction ratingFunction) { } /** - * Sets the handler to control the computation. The default is 'no handler'. + * Sets the handler to control the computation. The default is + * 'no handler'. * @param handler the optimization handler * @return the current builder + * @deprecated use the {@link #optimizationConfig} */ + @Deprecated public Builder handler(final OptimizationHandler handler) { - this.handler = handler; + this.optimizationConfig = OptimizationConfig.sat(handler); + return this; + } + + /** + * Sets the optimization config of the computation. The default is a + * config with a SAT based optimization without a handler. + * @param config the optimization config + * @return the current builder + */ + public Builder optimizationConfig(final OptimizationConfig config) { + this.optimizationConfig = config; + return this; + } + + /** + * Sets whether the intermediate result should be returned in case of + * a handler abortion. The default is 'false'. + * @param returnIntermediateResult the flag + * @return the current builder + */ + public Builder returnIntermediateResult(final boolean returnIntermediateResult) { + this.returnIntermediateResult = returnIntermediateResult; return this; } diff --git a/src/test/java/org/logicng/LogicNGVersionTest.java b/src/test/java/org/logicng/LogicNGVersionTest.java index 178fd82f..ed3a0628 100644 --- a/src/test/java/org/logicng/LogicNGVersionTest.java +++ b/src/test/java/org/logicng/LogicNGVersionTest.java @@ -34,9 +34,23 @@ import org.junit.jupiter.api.Test; import org.junit.jupiter.api.extension.ExtendWith; +import org.logicng.formulas.Formula; +import org.logicng.formulas.FormulaFactory; +import org.logicng.io.parsers.ParserException; +import org.logicng.io.parsers.PseudoBooleanParser; +import org.logicng.io.writers.FormulaWriter; +import org.logicng.transformations.Anonymizer; import org.mockito.MockedStatic; import org.mockito.junit.jupiter.MockitoExtension; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + /** * Unit tests for {@link LogicNGVersion}. * @version 2.1.0 diff --git a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java index e160bd82..e4a24068 100644 --- a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java +++ b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java @@ -29,8 +29,16 @@ package org.logicng.explanations.smus; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_INCWBO; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_SU; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_US; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_MSU3; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_OLL; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_WBO; import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.MethodSource; import org.logicng.TestWithExampleFormulas; import org.logicng.formulas.Formula; import org.logicng.handlers.BoundedOptimizationHandler; @@ -40,22 +48,38 @@ import org.logicng.io.parsers.ParserException; import org.logicng.io.readers.DimacsReader; import org.logicng.io.readers.FormulaReader; +import org.logicng.solvers.maxsat.OptimizationConfig; import java.io.IOException; +import java.util.ArrayList; import java.util.Arrays; +import java.util.Collection; import java.util.Collections; import java.util.List; import java.util.stream.Collectors; /** * Unit Tests for the class {@link SmusComputation}. - * @version 2.1.0 + * @version 2.6.0 * @since 2.0.0 */ public class SmusComputationTest extends TestWithExampleFormulas { - @Test - public void testFromPaper() { + public static Collection configs() { + final List configs = new ArrayList<>(); + configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_INCWBO, null, null), "INCWBO"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_WBO, null, null), "WBO"}); + return configs; + } + + @ParameterizedTest + @MethodSource("configs") + public void testFromPaper(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -66,12 +90,13 @@ public void testFromPaper() { parse(this.f, "~m|l"), parse(this.f, "~l") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f, cfg); assertThat(result).containsExactlyInAnyOrder(parse(this.f, "~s"), parse(this.f, "s|~p"), parse(this.f, "p")); } - @Test - public void testWithAdditionalConstraint() { + @ParameterizedTest + @MethodSource("configs") + public void testWithAdditionalConstraint(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -82,12 +107,13 @@ public void testWithAdditionalConstraint() { parse(this.f, "~m|l"), parse(this.f, "~l") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f, cfg); assertThat(result).containsExactlyInAnyOrder(parse(this.f, "~n"), parse(this.f, "~l")); } - @Test - public void testSatisfiable() { + @ParameterizedTest + @MethodSource("configs") + public void testSatisfiable(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -96,12 +122,13 @@ public void testSatisfiable() { parse(this.f, "~n"), parse(this.f, "~m|l") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f, cfg); assertThat(result).isNull(); } - @Test - public void testUnsatisfiableAdditionalConstraints() { + @ParameterizedTest + @MethodSource("configs") + public void testUnsatisfiableAdditionalConstraints(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -109,12 +136,13 @@ public void testUnsatisfiableAdditionalConstraints() { parse(this.f, "~m|n"), parse(this.f, "~n|s") ); - final List result = SmusComputation.computeSmusForFormulas(input, Arrays.asList(parse(this.f, "~a&b"), parse(this.f, "a|~b")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Arrays.asList(parse(this.f, "~a&b"), parse(this.f, "a|~b")), this.f, cfg); assertThat(result).isEmpty(); } - @Test - public void testTrivialUnsatFormula() { + @ParameterizedTest + @MethodSource("configs") + public void testTrivialUnsatFormula(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -126,12 +154,13 @@ public void testTrivialUnsatFormula() { parse(this.f, "~l"), parse(this.f, "a&~a") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f, cfg); assertThat(result).containsExactly(this.f.falsum()); } - @Test - public void testUnsatFormula() { + @ParameterizedTest + @MethodSource("configs") + public void testUnsatFormula(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -143,12 +172,13 @@ public void testUnsatFormula() { parse(this.f, "~l"), parse(this.f, "(a<=>b)&(~a<=>b)") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f, cfg); assertThat(result).containsExactly(parse(this.f, "(a<=>b)&(~a<=>b)")); } - @Test - public void testShorterConflict() { + @ParameterizedTest + @MethodSource("configs") + public void testShorterConflict(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -160,12 +190,13 @@ public void testShorterConflict() { parse(this.f, "~m|l"), parse(this.f, "~l") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f, cfg); assertThat(result).containsExactlyInAnyOrder(parse(this.f, "s|~p"), parse(this.f, "p&~s")); } - @Test - public void testCompleteConflict() { + @ParameterizedTest + @MethodSource("configs") + public void testCompleteConflict(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -174,12 +205,13 @@ public void testCompleteConflict() { parse(this.f, "n|~l"), parse(this.f, "l|s") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f, cfg); assertThat(result).containsExactlyInAnyOrderElementsOf(input); } - @Test - public void testLongConflictWithShortcut() { + @ParameterizedTest + @MethodSource("configs") + public void testLongConflictWithShortcut(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "~s"), parse(this.f, "s|~p"), @@ -189,7 +221,7 @@ public void testLongConflictWithShortcut() { parse(this.f, "l|s"), parse(this.f, "n|s") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f, cfg); assertThat(result).containsExactlyInAnyOrder(parse(this.f, "~s"), parse(this.f, "s|~p"), parse(this.f, "p|~m"), @@ -197,8 +229,9 @@ public void testLongConflictWithShortcut() { parse(this.f, "n|s")); } - @Test - public void testManyConflicts() { + @ParameterizedTest + @MethodSource("configs") + public void testManyConflicts(final OptimizationConfig cfg) { final List input = Arrays.asList( parse(this.f, "a"), parse(this.f, "~a|b"), @@ -220,7 +253,7 @@ public void testManyConflicts() { parse(this.f, "x&~y"), parse(this.f, "x=>y") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f, cfg); assertThat(result).containsExactlyInAnyOrder(parse(this.f, "x&~y"), parse(this.f, "x=>y")); } diff --git a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java index 061cacf7..b9530d06 100644 --- a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java +++ b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java @@ -29,8 +29,19 @@ package org.logicng.primecomputation; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.primecomputation.PrimeResult.CoverageType.IMPLICANTS_COMPLETE; +import static org.logicng.primecomputation.PrimeResult.CoverageType.IMPLICATES_COMPLETE; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_INCWBO; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_SU; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_US; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_MSU3; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_OLL; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_WBO; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.SAT_OPTIMIZATION; import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.MethodSource; import org.logicng.RandomTag; import org.logicng.TestWithExampleFormulas; import org.logicng.formulas.Formula; @@ -43,6 +54,7 @@ import org.logicng.io.parsers.ParserException; import org.logicng.io.readers.FormulaReader; import org.logicng.predicates.satisfiability.TautologyPredicate; +import org.logicng.solvers.maxsat.OptimizationConfig; import org.logicng.util.FormulaCornerCases; import org.logicng.util.FormulaRandomizer; import org.logicng.util.FormulaRandomizerConfig; @@ -53,72 +65,99 @@ import java.nio.file.Paths; import java.util.ArrayList; import java.util.Arrays; +import java.util.Collection; import java.util.List; import java.util.SortedSet; /** * Unit Tests for the class {@link PrimeCompiler}. - * @version 2.1.0 + * @version 2.6.0 * @since 2.0.0 */ public class PrimeCompilerTest extends TestWithExampleFormulas { - @Test - public void testSimple() { - computeAndVerify(this.TRUE); - computeAndVerify(this.FALSE); - computeAndVerify(this.A); - computeAndVerify(this.NA); - computeAndVerify(this.AND1); - computeAndVerify(this.AND2); - computeAndVerify(this.AND3); - computeAndVerify(this.OR1); - computeAndVerify(this.OR2); - computeAndVerify(this.OR3); - computeAndVerify(this.NOT1); - computeAndVerify(this.NOT2); - computeAndVerify(this.IMP1); - computeAndVerify(this.IMP2); - computeAndVerify(this.IMP3); - computeAndVerify(this.IMP4); - computeAndVerify(this.EQ1); - computeAndVerify(this.EQ2); - computeAndVerify(this.EQ3); - computeAndVerify(this.EQ4); - computeAndVerify(this.PBC1); - computeAndVerify(this.PBC2); - computeAndVerify(this.PBC3); - computeAndVerify(this.PBC4); - computeAndVerify(this.PBC5); + public static Collection configs() { + final List configs = new ArrayList<>(); + configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_INCWBO, null, null), "INCWBO"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_WBO, null, null), "WBO"}); + return configs; } - @Test - public void testCornerCases() { + public static Collection fastConfigs() { + final List configs = new ArrayList<>(); + configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"}); + return configs; + } + + @ParameterizedTest + @MethodSource("configs") + public void testSimple(final OptimizationConfig cfg) { + computeAndVerify(cfg, this.TRUE); + computeAndVerify(cfg, this.FALSE); + computeAndVerify(cfg, this.A); + computeAndVerify(cfg, this.NA); + computeAndVerify(cfg, this.AND1); + computeAndVerify(cfg, this.AND2); + computeAndVerify(cfg, this.AND3); + computeAndVerify(cfg, this.OR1); + computeAndVerify(cfg, this.OR2); + computeAndVerify(cfg, this.OR3); + computeAndVerify(cfg, this.NOT1); + computeAndVerify(cfg, this.NOT2); + computeAndVerify(cfg, this.IMP1); + computeAndVerify(cfg, this.IMP2); + computeAndVerify(cfg, this.IMP3); + computeAndVerify(cfg, this.IMP4); + computeAndVerify(cfg, this.EQ1); + computeAndVerify(cfg, this.EQ2); + computeAndVerify(cfg, this.EQ3); + computeAndVerify(cfg, this.EQ4); + computeAndVerify(cfg, this.PBC1); + computeAndVerify(cfg, this.PBC2); + computeAndVerify(cfg, this.PBC3); + computeAndVerify(cfg, this.PBC4); + computeAndVerify(cfg, this.PBC5); + } + + @ParameterizedTest + @MethodSource("configs") + public void testCornerCases(final OptimizationConfig cfg) { final FormulaFactory f = new FormulaFactory(); final FormulaCornerCases cornerCases = new FormulaCornerCases(f); - cornerCases.cornerCases().forEach(this::computeAndVerify); + cornerCases.cornerCases().forEach(it -> computeAndVerify(cfg, it)); } - @Test + @ParameterizedTest + @MethodSource("configs") @RandomTag - public void testRandomized() { + public void testRandomized(final OptimizationConfig cfg) { for (int i = 0; i < 200; i++) { final FormulaFactory f = new FormulaFactory(); final FormulaRandomizer randomizer = new FormulaRandomizer(f, FormulaRandomizerConfig.builder().numVars(10).weightPbc(2).seed(i * 42).build()); final Formula formula = randomizer.formula(4); - computeAndVerify(formula); + computeAndVerify(cfg, formula); } } - @Test - public void testOriginalFormulas() throws IOException { + @ParameterizedTest + @MethodSource("fastConfigs") + public void testOriginalFormulas(final OptimizationConfig cfg) throws IOException { Files.lines(Paths.get("src/test/resources/formulas/simplify_formulas.txt")) .filter(s -> !s.isEmpty()) .forEach(s -> { final Formula formula = parse(this.f, s); - final PrimeResult resultImplicantsMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICANTS_COMPLETE); + final PrimeResult resultImplicantsMin = PrimeCompiler.getWithMinimization().compute(formula, IMPLICANTS_COMPLETE , cfg); verify(resultImplicantsMin, formula); - final PrimeResult resultImplicatesMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICATES_COMPLETE); + final PrimeResult resultImplicatesMin = PrimeCompiler.getWithMinimization().compute(formula, IMPLICATES_COMPLETE, cfg); verify(resultImplicatesMin, formula); }); } @@ -126,10 +165,10 @@ public void testOriginalFormulas() throws IOException { @Test public void testTimeoutHandlerSmall() { final List> compilers = Arrays.asList( - new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), - new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE), - new Pair<>(PrimeCompiler.getWithMinimization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), - new Pair<>(PrimeCompiler.getWithMinimization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE)); + new Pair<>(PrimeCompiler.getWithMaximization(), IMPLICANTS_COMPLETE), + new Pair<>(PrimeCompiler.getWithMaximization(), IMPLICATES_COMPLETE), + new Pair<>(PrimeCompiler.getWithMinimization(), IMPLICANTS_COMPLETE), + new Pair<>(PrimeCompiler.getWithMinimization(), IMPLICATES_COMPLETE)); for (final Pair compiler : compilers) { final List handlers = Arrays.asList( new TimeoutOptimizationHandler(5_000L, TimeoutHandler.TimerType.SINGLE_TIMEOUT), @@ -146,10 +185,10 @@ public void testTimeoutHandlerSmall() { @Test public void testTimeoutHandlerLarge() throws IOException, ParserException { final List> compilers = Arrays.asList( - new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), - new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE), - new Pair<>(PrimeCompiler.getWithMinimization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), - new Pair<>(PrimeCompiler.getWithMinimization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE)); + new Pair<>(PrimeCompiler.getWithMaximization(), IMPLICANTS_COMPLETE), + new Pair<>(PrimeCompiler.getWithMaximization(), IMPLICATES_COMPLETE), + new Pair<>(PrimeCompiler.getWithMinimization(), IMPLICANTS_COMPLETE), + new Pair<>(PrimeCompiler.getWithMinimization(), IMPLICATES_COMPLETE)); for (final Pair compiler : compilers) { final List handlers = Arrays.asList( new TimeoutOptimizationHandler(1L, TimeoutHandler.TimerType.SINGLE_TIMEOUT), @@ -167,10 +206,10 @@ public void testTimeoutHandlerLarge() throws IOException, ParserException { public void testCancellationPoints() throws IOException { final Formula formula = parse(this.f, Files.readAllLines(Paths.get("src/test/resources/formulas/simplify_formulas.txt")).get(0)); final List> compilers = Arrays.asList( - new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), - new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE), - new Pair<>(PrimeCompiler.getWithMinimization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), - new Pair<>(PrimeCompiler.getWithMinimization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE)); + new Pair<>(PrimeCompiler.getWithMaximization(), IMPLICANTS_COMPLETE), + new Pair<>(PrimeCompiler.getWithMaximization(), IMPLICATES_COMPLETE), + new Pair<>(PrimeCompiler.getWithMinimization(), IMPLICANTS_COMPLETE), + new Pair<>(PrimeCompiler.getWithMinimization(), IMPLICATES_COMPLETE)); for (final Pair compiler : compilers) { for (int numOptimizationStarts = 1; numOptimizationStarts < 5; numOptimizationStarts++) { for (int numSatHandlerStarts = 1; numSatHandlerStarts < 10; numSatHandlerStarts++) { @@ -181,21 +220,21 @@ public void testCancellationPoints() throws IOException { } } - private void computeAndVerify(final Formula formula) { - final PrimeResult resultImplicantsMax = PrimeCompiler.getWithMaximization().compute(formula, PrimeResult.CoverageType.IMPLICANTS_COMPLETE); + private void computeAndVerify(final OptimizationConfig cfg, final Formula formula) { + final PrimeResult resultImplicantsMax = PrimeCompiler.getWithMaximization().compute(formula, IMPLICANTS_COMPLETE, cfg); verify(resultImplicantsMax, formula); - final PrimeResult resultImplicantsMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICANTS_COMPLETE); + final PrimeResult resultImplicantsMin = PrimeCompiler.getWithMinimization().compute(formula, IMPLICANTS_COMPLETE, cfg); verify(resultImplicantsMin, formula); - assertThat(resultImplicantsMax.getCoverageType()).isEqualTo(PrimeResult.CoverageType.IMPLICANTS_COMPLETE); - assertThat(resultImplicantsMin.getCoverageType()).isEqualTo(PrimeResult.CoverageType.IMPLICANTS_COMPLETE); + assertThat(resultImplicantsMax.getCoverageType()).isEqualTo(IMPLICANTS_COMPLETE); + assertThat(resultImplicantsMin.getCoverageType()).isEqualTo(IMPLICANTS_COMPLETE); assertThat(resultImplicantsMax.getPrimeImplicants()).containsExactlyInAnyOrderElementsOf(resultImplicantsMin.getPrimeImplicants()); - final PrimeResult resultImplicatesMax = PrimeCompiler.getWithMaximization().compute(formula, PrimeResult.CoverageType.IMPLICATES_COMPLETE); + final PrimeResult resultImplicatesMax = PrimeCompiler.getWithMaximization().compute(formula, IMPLICATES_COMPLETE, cfg); verify(resultImplicatesMax, formula); - final PrimeResult resultImplicatesMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICATES_COMPLETE); + final PrimeResult resultImplicatesMin = PrimeCompiler.getWithMinimization().compute(formula, IMPLICATES_COMPLETE, cfg); verify(resultImplicatesMin, formula); - assertThat(resultImplicatesMax.getCoverageType()).isEqualTo(PrimeResult.CoverageType.IMPLICATES_COMPLETE); - assertThat(resultImplicatesMin.getCoverageType()).isEqualTo(PrimeResult.CoverageType.IMPLICATES_COMPLETE); + assertThat(resultImplicatesMax.getCoverageType()).isEqualTo(IMPLICATES_COMPLETE); + assertThat(resultImplicatesMin.getCoverageType()).isEqualTo(IMPLICATES_COMPLETE); assertThat(resultImplicatesMax.getPrimeImplicates()).containsExactlyInAnyOrderElementsOf(resultImplicatesMin.getPrimeImplicates()); } diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java index be2b3cad..1a9905e6 100644 --- a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java +++ b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java @@ -29,8 +29,18 @@ package org.logicng.transformations.simplification; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_INCWBO; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_SU; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_US; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_MSU3; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_OLL; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_WBO; +import static org.mockito.Mockito.mock; +import static org.mockito.Mockito.when; import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.MethodSource; import org.logicng.LongRunningTag; import org.logicng.RandomTag; import org.logicng.TestWithExampleFormulas; @@ -43,46 +53,81 @@ import org.logicng.io.parsers.ParserException; import org.logicng.io.readers.FormulaReader; import org.logicng.predicates.satisfiability.TautologyPredicate; +import org.logicng.solvers.maxsat.OptimizationConfig; import org.logicng.util.FormulaCornerCases; import org.logicng.util.FormulaRandomizer; import org.logicng.util.FormulaRandomizerConfig; import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.ArrayList; import java.util.Arrays; +import java.util.Collection; import java.util.List; +import java.util.concurrent.atomic.AtomicInteger; /** * Unit Tests for the class {@link AdvancedSimplifier}. - * @version 2.3.0 + * @version 2.6.0 * @since 2.0.0 */ public class AdvancedSimplifierTest extends TestWithExampleFormulas { - private final AdvancedSimplifier simplifier = new AdvancedSimplifier(); + public static Collection configs() { + final List configs = new ArrayList<>(); + configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_INCWBO, null, null), "INCWBO"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"}); + configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_WBO, null, null), "WBO"}); + return configs; + } - @Test - public void testConstants() { - assertThat(this.f.falsum().transform(this.simplifier)).isEqualTo(this.f.falsum()); - assertThat(this.f.verum().transform(this.simplifier)).isEqualTo(this.f.verum()); + @ParameterizedTest + @MethodSource("configs") + public void testConstants(final OptimizationConfig cfg) { + final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build()); + assertThat(this.f.falsum().transform(simplifier)).isEqualTo(this.f.falsum()); + assertThat(this.f.verum().transform(simplifier)).isEqualTo(this.f.verum()); } - @Test - public void testCornerCases() { + @ParameterizedTest + @MethodSource("configs") + public void testCornerCases(final OptimizationConfig cfg) { + final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build()); final FormulaCornerCases cornerCases = new FormulaCornerCases(this.f); - cornerCases.cornerCases().forEach(this::computeAndVerify); + cornerCases.cornerCases().forEach(it -> computeAndVerify(it, simplifier)); } - @Test + @ParameterizedTest + @MethodSource("configs") @RandomTag - public void testRandomized() { + public void testRandomized(final OptimizationConfig cfg) { + final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build()); for (int i = 0; i < 100; i++) { final FormulaFactory f = new FormulaFactory(); final FormulaRandomizer randomizer = new FormulaRandomizer(f, FormulaRandomizerConfig.builder().numVars(8).weightPbc(2).seed(i * 42).build()); final Formula formula = randomizer.formula(5); - computeAndVerify(formula); + computeAndVerify(formula, simplifier); } } + @ParameterizedTest + @MethodSource("configs") + public void testOriginalFormula(final OptimizationConfig cfg) throws IOException { + final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build()); + Files.lines(Paths.get("src/test/resources/formulas/simplify_formulas.txt")) + .filter(s -> !s.isEmpty()) + .forEach(s -> { + final FormulaFactory f = new FormulaFactory(); + final Formula formula = parse(f, s); + computeAndVerify(formula, simplifier); + }); + } + @Test public void testTimeoutHandlerSmall() { final List handlers = Arrays.asList( @@ -92,7 +137,8 @@ public void testTimeoutHandlerSmall() { ); final Formula formula = parse(this.f, "a & b | ~c & a"); for (final TimeoutOptimizationHandler handler : handlers) { - testHandler(handler, formula, false); + testHandler(handler, formula, false, false); + testHandler(handler, formula, false, true); } } @@ -105,7 +151,8 @@ public void testTimeoutHandlerLarge() throws IOException, ParserException { ); final Formula formula = FormulaReader.readPseudoBooleanFormula("src/test/resources/formulas/large_formula.txt", this.f); for (final TimeoutOptimizationHandler handler : handlers) { - testHandler(handler, formula, true); + testHandler(handler, formula, true, false); + testHandler(handler, formula, true, true); } } @@ -113,14 +160,16 @@ public void testTimeoutHandlerLarge() throws IOException, ParserException { public void testPrimeCompilerIsCancelled() { final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 0); final Formula formula = parse(this.f, "a&(b|c)"); - testHandler(handler, formula, true); + testHandler(handler, formula, true, false); + testHandler(handler, formula, true, true); } @Test public void testSmusComputationIsCancelled() { final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 5); final Formula formula = parse(this.f, "a&(b|c)"); - testHandler(handler, formula, true); + testHandler(handler, formula, true, false); + testHandler(handler, formula, true, true); } @LongRunningTag @@ -132,7 +181,7 @@ public void testCancellationPoints() { for (int numOptimizationStarts = 1; numOptimizationStarts < 30; numOptimizationStarts++) { for (int numSatHandlerStarts = 1; numSatHandlerStarts < 500; numSatHandlerStarts++) { final OptimizationHandler handler = new BoundedOptimizationHandler(numSatHandlerStarts, numOptimizationStarts); - testHandler(handler, formula, true); + testHandler(handler, formula, true, false); } } } @@ -142,11 +191,13 @@ public void testAdvancedSimplifierConfig() { final FormulaFactory f = new FormulaFactory(); final List configs = Arrays.asList( AdvancedSimplifierConfig.builder().build(), - AdvancedSimplifierConfig.builder().restrictBackbone(false).factorOut(false).simplifyNegations(false).build(), + AdvancedSimplifierConfig.builder().restrictBackbone(false).minimalDnfCover(false).factorOut(false).simplifyNegations(false).build(), AdvancedSimplifierConfig.builder().factorOut(false).simplifyNegations(false).build(), AdvancedSimplifierConfig.builder().restrictBackbone(false).simplifyNegations(false).build(), + AdvancedSimplifierConfig.builder().restrictBackbone(false).minimalDnfCover(false).build(), AdvancedSimplifierConfig.builder().restrictBackbone(false).factorOut(false).build(), AdvancedSimplifierConfig.builder().restrictBackbone(false).build(), + AdvancedSimplifierConfig.builder().minimalDnfCover(false).build(), AdvancedSimplifierConfig.builder().factorOut(false).build(), AdvancedSimplifierConfig.builder().simplifyNegations(false).build()); @@ -164,20 +215,39 @@ public void testAdvancedSimplifierConfig() { } } - private void computeAndVerify(final Formula formula) { - final Formula simplified = formula.transform(this.simplifier); + @Test + public void testBackboneIntermediateResult() { + final FormulaFactory f = new FormulaFactory(); + final Formula formula = parse(f, "(a & b) | (a & c)"); + final OptimizationHandler optHandler = mock(OptimizationHandler.class); + // abort simplification after successful backbone computation + final AtomicInteger count = new AtomicInteger(0); + when(optHandler.aborted()).then(invocationOnMock -> count.addAndGet(1) > 1); + testHandler(optHandler, formula, true, true); + } + + private void computeAndVerify(final Formula formula, final AdvancedSimplifier simplifier) { + final Formula simplified = formula.transform(simplifier); assertThat(formula.factory().equivalence(formula, simplified).holds(new TautologyPredicate(this.f))) .as("Minimized formula is equivalent to original Formula") .isTrue(); } - private void testHandler(final OptimizationHandler handler, final Formula formula, final boolean expAborted) { - final AdvancedSimplifier simplifierWithHandler = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().handler(handler).build()); + private void testHandler(final OptimizationHandler handler, final Formula formula, final boolean expAborted, final boolean expIntermediate) { + final AdvancedSimplifier simplifierWithHandler = new AdvancedSimplifier(AdvancedSimplifierConfig.builder() + .optimizationConfig(OptimizationConfig.sat(handler)) + .returnIntermediateResult(expIntermediate) + .build()); final Formula simplified = formula.transform(simplifierWithHandler); assertThat(handler.aborted()).isEqualTo(expAborted); if (expAborted) { assertThat(handler.aborted()).isTrue(); - assertThat(simplified).isNull(); + if (!expIntermediate) { + assertThat(simplified).isNull(); + } else { + assertThat(simplified).isNotNull(); + assertThat(simplified.isEquivalentTo(formula)).isTrue(); + } } else { assertThat(handler.aborted()).isFalse(); assertThat(simplified).isNotNull();