From 8fb005a88e9d7748e27a8751820622b5f2bc0259 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Tue, 30 Jul 2024 11:29:54 +0200 Subject: [PATCH] WIP configure optimization in algorithms --- .../explanations/smus/SmusComputation.java | 231 +++++++++++++++--- .../primecomputation/PrimeCompiler.java | 32 ++- .../solvers/maxsat/OptimizationConfig.java | 103 ++++++++ .../simplification/AdvancedSimplifier.java | 61 ++--- .../AdvancedSimplifierConfig.java | 18 +- .../java/org/logicng/LogicNGVersionTest.java | 14 ++ .../smus/SmusComputationTest.java | 97 +++++--- 7 files changed, 446 insertions(+), 110 deletions(-) create mode 100644 src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java index b8a10202..2e3f0585 100644 --- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java @@ -31,20 +31,28 @@ 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.solvers.maxsat.OptimizationConfig.OptimizationType.SAT_OPTIMIZATION; import org.logicng.datastructures.Assignment; import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Variable; +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 java.util.ArrayList; +import java.util.Collection; import java.util.Collections; import java.util.List; import java.util.Map; @@ -60,7 +68,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 +90,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 = new OptimizationConfig(SAT_OPTIMIZATION, null, null, 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,8 +109,95 @@ 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 = new OptimizationConfig(SAT_OPTIMIZATION, null, handler, 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. + * @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) { + if (config.getOptimizationType() == SAT_OPTIMIZATION) { + return computeSmusSat(propositions, additionalConstraints, f, config.getOptimizationHandler()); + } else { + return computeSmusMaxSAT(propositions, additionalConstraints, f, config); + } + } + + /** + * 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 + * @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 cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, null, null); + 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 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) { + final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, handler, null); + 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, config); + return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList()); + } + + private static

List

computeSmusSat( + final List

propositions, + final List additionalConstraints, + final FormulaFactory f, + final OptimizationHandler handler) { start(handler); final SATSolver growSolver = MiniSat.miniSat(f); growSolver.add(additionalConstraints == null ? Collections.singletonList(f.verum()) : additionalConstraints); @@ -130,33 +228,49 @@ public static

List

computeSmus(final List

proposit } } - /** - * 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 - * @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); - } - - /** - * 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 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) { - final List props = formulas.stream().map(StandardProposition::new).collect(Collectors.toList()); - final List smus = computeSmus(props, additionalConstraints, f, handler); - return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList()); + private static

List

computeSmusMaxSAT( + final List

propositions, + final List addConstraints, + final FormulaFactory f, + final OptimizationConfig config) { + final MaxSATHandler handler = config.getMaxSATHandler(); + start(handler); + final Collection additionalConstraints = addConstraints == null + ? Collections.singletonList(f.verum()) + : addConstraints; + final List growSolverConstraints = new ArrayList<>(additionalConstraints); + final Map propositionMapping = new TreeMap<>(); + for (final P proposition : propositions) { + final Variable selector = f.variable(PROPOSITION_SELECTOR + propositionMapping.size()); + propositionMapping.put(selector, proposition); + growSolverConstraints.add(f.equivalence(selector, proposition.formula())); + } + final SATSolver satSolver = MiniSat.miniSat(f); + satSolver.add(growSolverConstraints); + final SATHandler satHandler = handler == null ? null : handler.satHandler(); + final boolean sat = satSolver.sat(satHandler, propositionMapping.keySet()) == Tristate.TRUE; + if (sat || aborted(satHandler)) { + return null; + } + final List hSolverConstraints = new ArrayList<>(); + while (true) { + final SortedSet h = minimumHs(hSolverConstraints, propositionMapping.keySet(), config, f); + if (h == null || aborted(handler)) { + return null; + } + final SortedSet c = grow(growSolverConstraints, h, propositionMapping.keySet(), config, f); + if (aborted(handler)) { + return null; + } + if (c == null) { + return h.stream().map(propositionMapping::get).collect(Collectors.toList()); + } + hSolverConstraints.add(f.or(c)); + } } - private static SortedSet minimumHs(final SATSolver hSolver, final Set variables, final OptimizationHandler handler) { + private static SortedSet minimumHs( + final SATSolver hSolver, final Set variables, final OptimizationHandler handler) { final Assignment minimumHsModel = hSolver.execute(OptimizationFunction.builder() .handler(handler) .literals(variables) @@ -164,7 +278,31 @@ private static SortedSet minimumHs(final SATSolver hSolver, final Set< return aborted(handler) ? null : new TreeSet<>(minimumHsModel.positiveVariables()); } - private static SortedSet grow(final SATSolver growSolver, final SortedSet h, final Set variables, final OptimizationHandler handler) { + private static SortedSet minimumHs( + final List constraints, + final Set variables, + final OptimizationConfig config, + final FormulaFactory f) { + if (variables.isEmpty()) { + return new TreeSet<>(); // TODO workaround: MaxSAT assertion fails for corner case + } + final MaxSATSolver maxSatSolver = config.genMaxSATSolver(f); + constraints.forEach(maxSatSolver::addHardFormula); + for (final Variable v : variables) { + maxSatSolver.addSoftFormula(v.negate(), 1); + } + final MaxSAT.MaxSATResult result = maxSatSolver.solve(config.getMaxSATHandler()); + if (result == MaxSAT.MaxSATResult.UNDEF) { + return null; + } + return new TreeSet<>(maxSatSolver.model().positiveVariables()); + } + + 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() @@ -181,4 +319,31 @@ private static SortedSet grow(final SATSolver growSolver, final Sorted return minimumCorrectionSet; } } + + private static SortedSet grow( + final List constraints, + final SortedSet h, + final Set variables, + final OptimizationConfig config, + final FormulaFactory f) { + final MaxSATSolver maxSatSolver = config.genMaxSATSolver(f); + constraints.forEach(maxSatSolver::addHardFormula); + h.forEach(maxSatSolver::addHardFormula); + for (final Variable v : variables) { + maxSatSolver.addSoftFormula(v, 1); + } + final MaxSAT.MaxSATResult result = maxSatSolver.solve(config.getMaxSATHandler()); + if (result == MaxSAT.MaxSATResult.UNDEF) { + return null; + } + final Assignment maxModel = maxSatSolver.model(); + if (maxModel == null) { + return null; + } else { + final List maximumSatisfiableSet = maxModel.positiveVariables(); + final SortedSet minimumCorrectionSet = new TreeSet<>(variables); + maximumSatisfiableSet.forEach(minimumCorrectionSet::remove); + return minimumCorrectionSet; + } + } } diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java index a3e433af..634bc51e 100644 --- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java @@ -42,6 +42,8 @@ import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; import org.logicng.solvers.functions.OptimizationFunction; +import org.logicng.solvers.maxsat.OptimizationConfig; +import org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType; import org.logicng.solvers.sat.MiniSatConfig; import org.logicng.transformations.LiteralSubstitution; import org.logicng.util.FormulaHelper; @@ -76,13 +78,17 @@ public final class PrimeCompiler { private static final String POS = "_POS"; private static final String NEG = "_NEG"; - private static final PrimeCompiler INSTANCE_MIN = new PrimeCompiler(false); - private static final PrimeCompiler INSTANCE_MAX = new PrimeCompiler(true); + private static final OptimizationConfig DEFAULT_CFG = + new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, null, null); + private static final PrimeCompiler INSTANCE_MIN = new PrimeCompiler(false, DEFAULT_CFG); + private static final PrimeCompiler INSTANCE_MAX = new PrimeCompiler(true, DEFAULT_CFG); private final boolean computeWithMaximization; + private final OptimizationConfig config; - private PrimeCompiler(final boolean computeWithMaximization) { + private PrimeCompiler(final boolean computeWithMaximization, final OptimizationConfig config) { this.computeWithMaximization = computeWithMaximization; + this.config = config; } /** @@ -101,6 +107,22 @@ public static PrimeCompiler getWithMaximization() { return INSTANCE_MAX; } + /** + * Returns a compiler which uses minimum models to compute the primes. + * @return a compiler which uses minimum models to compute the primes + */ + public static PrimeCompiler getWithMinimization(final OptimizationConfig config) { + return new PrimeCompiler(false, config); + } + + /** + * Returns a compiler which uses maximum models to compute the primes. + * @return a compiler which uses maximum models to compute the primes + */ + public static PrimeCompiler getWithMaximization(final OptimizationConfig config) { + return new PrimeCompiler(false, config); + } + /** * Computes prime implicants and prime implicates for a given formula. * The coverage type specifies if the implicants or the implicates will @@ -167,7 +189,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; } 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..35c8e1f9 --- /dev/null +++ b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java @@ -0,0 +1,103 @@ +package org.logicng.solvers.maxsat; + +import org.logicng.formulas.FormulaFactory; +import org.logicng.handlers.MaxSATHandler; +import org.logicng.handlers.OptimizationHandler; +import org.logicng.solvers.MaxSATSolver; +import org.logicng.solvers.maxsat.algorithms.MaxSATConfig; + +import java.util.Objects; + +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; + + public 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; + } + + public OptimizationType getOptimizationType() { + return this.optimizationType; + } + + public MaxSATConfig getMaxSATConfig() { + return this.maxSATConfig; + } + + public OptimizationHandler getOptimizationHandler() { + return this.optimizationHandler; + } + + public MaxSATHandler getMaxSATHandler() { + return this.maxSATHandler; + } + + 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); + } + } + + @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/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java index 7d57439c..e5e78f80 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java @@ -28,32 +28,19 @@ 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; import org.logicng.configurations.ConfigurationType; -import org.logicng.datastructures.Assignment; -import org.logicng.explanations.smus.SmusComputation; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.FormulaTransformation; import org.logicng.formulas.Literal; import org.logicng.handlers.OptimizationHandler; -import org.logicng.primecomputation.PrimeCompiler; -import org.logicng.primecomputation.PrimeResult; import org.logicng.util.FormulaHelper; import java.util.ArrayList; import java.util.Collection; -import java.util.Collections; import java.util.List; import java.util.SortedSet; import java.util.TreeSet; -import java.util.stream.Collectors; /** * An advanced simplifier for formulas. @@ -126,21 +113,21 @@ 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); + //start(config.handler); // TODO activate 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; - } - if (!backbone.isSat()) { - return f.falsum(); - } - backboneLiterals.addAll(backbone.getCompleteBackbone()); - simplified = formula.restrict(new Assignment(backboneLiterals)); + //final Backbone backbone = BackboneGeneration // TODO activate + // .compute(Collections.singletonList(formula), formula.variables(), BackboneType.POSITIVE_AND_NEGATIVE, satHandler(config.handler)); + //if (backbone == null || aborted(config.handler)) { + // return null; + //} + //if (!backbone.isSat()) { + // return f.falsum(); + //} + //backboneLiterals.addAll(backbone.getCompleteBackbone()); + //simplified = formula.restrict(new Assignment(backboneLiterals)); } final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); if (simplifyMinDnf == null) { @@ -161,19 +148,19 @@ public Formula apply(final Formula formula, final boolean cache) { return simplified; } - private Formula computeMinDnf(final FormulaFactory f, Formula simplified, final AdvancedSimplifierConfig config) { - final PrimeResult primeResult = - PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.handler); - if (primeResult == null || aborted(config.handler)) { - 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)) { - return null; - } - simplified = f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList())); + private Formula computeMinDnf(final FormulaFactory f, final Formula simplified, final AdvancedSimplifierConfig config) { + //final PrimeResult primeResult = //TODO + // PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.handler); + //if (primeResult == null || aborted(config.handler)) { + // 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)) { + // return null; + //} + //simplified = f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList())); return simplified; } diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java index f3f1af55..83c8d063 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -31,6 +31,7 @@ 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}. @@ -44,7 +45,7 @@ public class AdvancedSimplifierConfig extends Configuration { boolean factorOut; boolean simplifyNegations; RatingFunction ratingFunction; - OptimizationHandler handler; + OptimizationConfig optimizationConfig; @Override public String toString() { @@ -53,7 +54,7 @@ public String toString() { ", factorOut=" + this.factorOut + ", simplifyNegations=" + this.simplifyNegations + ", ratingFunction=" + this.ratingFunction + - ", handler=" + this.handler + + ", optimizationConfig=" + this.optimizationConfig + '}'; } @@ -67,7 +68,7 @@ private AdvancedSimplifierConfig(final Builder builder) { this.factorOut = builder.factorOut; this.simplifyNegations = builder.simplifyNegations; this.ratingFunction = builder.ratingFunction; - this.handler = builder.handler; + this.optimizationConfig = builder.optimizationConfig; } /** @@ -87,7 +88,7 @@ public static class Builder { boolean factorOut = true; boolean simplifyNegations = true; private RatingFunction ratingFunction = new DefaultRatingFunction(); - private OptimizationHandler handler = null; + private OptimizationConfig optimizationConfig = null; private Builder() { // Initialize only via factory @@ -138,9 +139,16 @@ public Builder ratingFunction(final RatingFunction ratingFunction) { * 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 = new OptimizationConfig(OptimizationConfig.OptimizationType.SAT_OPTIMIZATION, null, handler, null); + return this; + } + + public Builder optimizationConfig(final OptimizationConfig config) { + this.optimizationConfig = config; 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..b3630a09 100644 --- a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java +++ b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java @@ -29,8 +29,17 @@ 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 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.TestWithExampleFormulas; import org.logicng.formulas.Formula; import org.logicng.handlers.BoundedOptimizationHandler; @@ -40,22 +49,39 @@ 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[]{new OptimizationConfig(SAT_OPTIMIZATION, null, null, null), "SAT"}); + configs.add(new Object[]{new OptimizationConfig(MAXSAT_INCWBO, null, null, null), "INCWBO"}); + configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_SU, null, null, null), "LINEAR_SU"}); + configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_US, null, null, null), "LINEAR_US"}); + configs.add(new Object[]{new OptimizationConfig(MAXSAT_MSU3, null, null, null), "MSU3"}); + configs.add(new Object[]{new OptimizationConfig(MAXSAT_OLL, null, null, null), "OLL"}); + configs.add(new Object[]{new OptimizationConfig(MAXSAT_WBO, null, 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 +92,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 +109,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 +124,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 +138,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 +156,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 +174,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 +192,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 +207,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 +223,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 +231,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 +255,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")); }