From 8fb005a88e9d7748e27a8751820622b5f2bc0259 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Tue, 30 Jul 2024 11:29:54 +0200 Subject: [PATCH 1/9] 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")); } From f72daf21e4fa99657170bc1cf32253d949839aed Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Thu, 1 Aug 2024 21:29:06 +0200 Subject: [PATCH 2/9] Optimization config in prime compiler --- pom.xml | 2 +- .../explanations/smus/SmusComputation.java | 7 +- .../primecomputation/PrimeCompiler.java | 138 +++++++++++---- .../solvers/maxsat/algorithms/IncWBO.java | 2 - .../solvers/maxsat/algorithms/MaxSAT.java | 4 - .../smus/SmusComputationTest.java | 1 - .../primecomputation/PrimeCompilerTest.java | 157 +++++++++++------- 7 files changed, 207 insertions(+), 104 deletions(-) diff --git a/pom.xml b/pom.xml index 70ebfd72..00fb5a6b 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.5.1 + 2.6.0-SNAPSHOT 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 2e3f0585..10cc940d 100644 --- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java @@ -137,7 +137,7 @@ public static

List

computeSmus( final FormulaFactory f, final OptimizationConfig config) { if (config.getOptimizationType() == SAT_OPTIMIZATION) { - return computeSmusSat(propositions, additionalConstraints, f, config.getOptimizationHandler()); + return computeSmusSAT(propositions, additionalConstraints, f, config.getOptimizationHandler()); } else { return computeSmusMaxSAT(propositions, additionalConstraints, f, config); } @@ -193,7 +193,7 @@ public static List computeSmusForFormulas( return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList()); } - private static

List

computeSmusSat( + private static

List

computeSmusSAT( final List

propositions, final List additionalConstraints, final FormulaFactory f, @@ -283,9 +283,6 @@ private static SortedSet minimumHs( 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) { diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java index 634bc51e..e2aa195e 100644 --- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java @@ -39,12 +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.maxsat.OptimizationConfig; import org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType; -import org.logicng.solvers.sat.MiniSatConfig; +import org.logicng.solvers.maxsat.algorithms.MaxSAT; import org.logicng.transformations.LiteralSubstitution; import org.logicng.util.FormulaHelper; import org.logicng.util.Pair; @@ -71,24 +73,20 @@ * {@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 { private static final String POS = "_POS"; private static final String NEG = "_NEG"; - 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 static final PrimeCompiler INSTANCE_MIN = new PrimeCompiler(false); + private static final PrimeCompiler INSTANCE_MAX = new PrimeCompiler(true); private final boolean computeWithMaximization; - private final OptimizationConfig config; - private PrimeCompiler(final boolean computeWithMaximization, final OptimizationConfig config) { + private PrimeCompiler(final boolean computeWithMaximization) { this.computeWithMaximization = computeWithMaximization; - this.config = config; } /** @@ -108,31 +106,36 @@ public static PrimeCompiler getWithMaximization() { } /** - * 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 + * 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. + * @param formula the formula + * @param type the coverage type + * @return the prime result */ - public static PrimeCompiler getWithMaximization(final OptimizationConfig config) { - return new PrimeCompiler(false, config); + public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type) { + return compute(formula, type, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, null, null)); } /** * 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 - * @return the prime result + * @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) { - return compute(formula, type, null); + public PrimeResult compute( + final Formula formula, + final PrimeResult.CoverageType type, + final OptimizationHandler handler) { + return compute(formula, type, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, handler, null)); } /** @@ -146,15 +149,23 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType * the handler's SAT handler is used for every subsequent SAT call. * @param formula the formula * @param type the coverage type - * @param handler an optimization handler, can be {@code null} + * @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 OptimizationHandler handler) { - start(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( @@ -163,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<>(); @@ -216,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) { + 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/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/test/java/org/logicng/explanations/smus/SmusComputationTest.java b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java index b3630a09..bc445360 100644 --- a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java +++ b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java @@ -78,7 +78,6 @@ public static Collection configs() { return configs; } - @ParameterizedTest @MethodSource("configs") public void testFromPaper(final OptimizationConfig cfg) { diff --git a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java index 061cacf7..78963778 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[]{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; } - @Test - public void testCornerCases() { + public static Collection fastConfigs() { + final List configs = new ArrayList<>(); + configs.add(new Object[]{new OptimizationConfig(SAT_OPTIMIZATION, null, null, null), "SAT"}); + 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"}); + 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()); } From 18f3c7262e97b0b7bef76e2bb42c642bff8bce4a Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Thu, 1 Aug 2024 22:12:23 +0200 Subject: [PATCH 3/9] Optimization config in advanced simplifier --- .../explanations/smus/SmusComputation.java | 8 +- .../primecomputation/PrimeCompiler.java | 4 +- .../solvers/maxsat/OptimizationConfig.java | 105 +++++++++++++++++- .../simplification/AdvancedSimplifier.java | 62 ++++++----- .../AdvancedSimplifierConfig.java | 50 +++++++-- .../smus/SmusComputationTest.java | 15 ++- .../primecomputation/PrimeCompilerTest.java | 24 ++-- .../AdvancedSimplifierTest.java | 98 ++++++++++++---- 8 files changed, 277 insertions(+), 89 deletions(-) diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java index 10cc940d..5de12377 100644 --- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java @@ -92,7 +92,7 @@ private SmusComputation() { */ public static

List

computeSmus( final List

propositions, final List additionalConstraints, final FormulaFactory f) { - final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, null, null); + final OptimizationConfig cfg = OptimizationConfig.sat(null); return computeSmus(propositions, additionalConstraints, f, cfg); } @@ -114,7 +114,7 @@ public static

List

computeSmus( final List additionalConstraints, final FormulaFactory f, final OptimizationHandler handler) { - final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, handler, null); + final OptimizationConfig cfg = OptimizationConfig.sat(handler); return computeSmus(propositions, additionalConstraints, f, cfg); } @@ -154,7 +154,7 @@ public static List computeSmusForFormulas( final List formulas, final List additionalConstraints, final FormulaFactory f) { - final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, null, null); + final OptimizationConfig cfg = OptimizationConfig.sat(null); return computeSmusForFormulas(formulas, additionalConstraints, f, cfg); } @@ -171,7 +171,7 @@ public static List computeSmusForFormulas( final List additionalConstraints, final FormulaFactory f, final OptimizationHandler handler) { - final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, handler, null); + final OptimizationConfig cfg = OptimizationConfig.sat(handler); return computeSmusForFormulas(formulas, additionalConstraints, f, cfg); } diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java index e2aa195e..fde8a8a6 100644 --- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java @@ -114,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, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, null, null)); + return compute(formula, type, OptimizationConfig.sat(null)); } /** @@ -135,7 +135,7 @@ public PrimeResult compute( final Formula formula, final PrimeResult.CoverageType type, final OptimizationHandler handler) { - return compute(formula, type, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, handler, null)); + return compute(formula, type, OptimizationConfig.sat(handler)); } /** diff --git a/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java index 35c8e1f9..1b4cf7ee 100644 --- a/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java +++ b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java @@ -3,11 +3,26 @@ 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, @@ -24,7 +39,7 @@ public enum OptimizationType { private final OptimizationHandler optimizationHandler; private final MaxSATHandler maxSATHandler; - public OptimizationConfig( + private OptimizationConfig( final OptimizationType optType, final MaxSATConfig maxConfig, final OptimizationHandler optHandler, @@ -36,22 +51,62 @@ public OptimizationConfig( this.maxSATHandler = maxHandler; } - public OptimizationType getOptimizationType() { - return this.optimizationType; + /** + * 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); } - public MaxSATConfig getMaxSATConfig() { - return this.maxSATConfig; + /** + * Returns the optimization type. + * @return the optimization type + */ + public OptimizationType getOptimizationType() { + return this.optimizationType; } + /** + * 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: @@ -71,6 +126,46 @@ public MaxSATSolver genMaxSATSolver(final FormulaFactory f) { } } + /** + * Starts the solver of 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) { diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java index e5e78f80..594e2e70 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java @@ -28,19 +28,29 @@ package org.logicng.transformations.simplification; +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.solvers.maxsat.OptimizationConfig; 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. @@ -59,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 { @@ -113,25 +123,26 @@ 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); // TODO activate + 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 // 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 Backbone backbone = BackboneGeneration + .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(); + } + backboneLiterals.addAll(backbone.getCompleteBackbone()); + simplified = formula.restrict(new Assignment(backboneLiterals)); } final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); if (simplifyMinDnf == null) { - return null; + return config.returnIntermediateResult ? simplified : null; } simplified = simplifyWithRating(simplified, simplifyMinDnf, config); if (config.factorOut) { @@ -149,19 +160,18 @@ public Formula apply(final Formula formula, final boolean cache) { } 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; + final PrimeResult primeResult = + 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.optimizationConfig); + if (minimizedPIs == null || config.optimizationConfig.aborted()) { + return null; + } + 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 83c8d063..cdfada01 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -28,6 +28,8 @@ package org.logicng.transformations.simplification; +import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.SAT_OPTIMIZATION; + import org.logicng.configurations.Configuration; import org.logicng.configurations.ConfigurationType; import org.logicng.handlers.OptimizationHandler; @@ -35,7 +37,7 @@ /** * The configuration object for the {@link AdvancedSimplifier}. - * @version 2.3.0 + * @version 2.6.0 * @since 2.3.0 */ @@ -44,6 +46,7 @@ public class AdvancedSimplifierConfig extends Configuration { boolean restrictBackbone; boolean factorOut; boolean simplifyNegations; + boolean returnIntermediateResult; RatingFunction ratingFunction; OptimizationConfig optimizationConfig; @@ -53,6 +56,7 @@ public String toString() { "restrictBackbone=" + this.restrictBackbone + ", factorOut=" + this.factorOut + ", simplifyNegations=" + this.simplifyNegations + + ", returnIntermediateResult=" + this.returnIntermediateResult + ", ratingFunction=" + this.ratingFunction + ", optimizationConfig=" + this.optimizationConfig + '}'; @@ -67,6 +71,7 @@ private AdvancedSimplifierConfig(final Builder builder) { this.restrictBackbone = builder.restrictBackbone; this.factorOut = builder.factorOut; this.simplifyNegations = builder.simplifyNegations; + this.returnIntermediateResult = builder.returnIntermediateResult; this.ratingFunction = builder.ratingFunction; this.optimizationConfig = builder.optimizationConfig; } @@ -87,15 +92,17 @@ public static class Builder { boolean restrictBackbone = true; boolean factorOut = true; boolean simplifyNegations = true; - private RatingFunction ratingFunction = new DefaultRatingFunction(); - private OptimizationConfig optimizationConfig = null; + 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 */ @@ -105,7 +112,8 @@ 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 the formula should be factorized. The + * default is 'true'. * @param factorOut flag for the factorisation * @return the current builder */ @@ -115,7 +123,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 */ @@ -125,8 +134,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 */ @@ -136,22 +148,40 @@ 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.optimizationConfig = new OptimizationConfig(OptimizationConfig.OptimizationType.SAT_OPTIMIZATION, null, handler, null); + 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; + } + /** * Builds the configuration. * @return the configuration. diff --git a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java index bc445360..e4a24068 100644 --- a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java +++ b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java @@ -35,7 +35,6 @@ 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; @@ -68,13 +67,13 @@ public class SmusComputationTest extends TestWithExampleFormulas { 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"}); + 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; } diff --git a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java index 78963778..b9530d06 100644 --- a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java +++ b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java @@ -78,23 +78,23 @@ public class PrimeCompilerTest extends TestWithExampleFormulas { 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"}); + 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; } public static Collection fastConfigs() { final List configs = new ArrayList<>(); - configs.add(new Object[]{new OptimizationConfig(SAT_OPTIMIZATION, null, null, null), "SAT"}); - 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[]{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; } diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java index be2b3cad..ec902ca3 100644 --- a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java +++ b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java @@ -29,8 +29,16 @@ 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 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 +51,80 @@ 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; /** * 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 +134,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 +148,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 +157,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 +178,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); } } } @@ -164,20 +210,28 @@ public void testAdvancedSimplifierConfig() { } } - private void computeAndVerify(final Formula formula) { - final Formula simplified = formula.transform(this.simplifier); + 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(); From 09e61b08866f927a85fe9fc7cf1d24156dd7923e Mon Sep 17 00:00:00 2001 From: Rouven Walter Date: Fri, 2 Aug 2024 19:34:36 +0200 Subject: [PATCH 4/9] minor refactoring and improvements --- .../explanations/smus/SmusComputation.java | 75 +++++++++---------- .../primecomputation/PrimeCompiler.java | 2 +- .../solvers/maxsat/OptimizationConfig.java | 15 +++- .../AdvancedSimplifierConfig.java | 2 - 4 files changed, 49 insertions(+), 45 deletions(-) diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java index 5de12377..4a66ab9c 100644 --- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java @@ -32,6 +32,8 @@ 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 static org.logicng.util.CollectionHelper.difference; +import static org.logicng.util.CollectionHelper.nullSafe; import org.logicng.datastructures.Assignment; import org.logicng.datastructures.Tristate; @@ -52,14 +54,13 @@ 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; import java.util.Set; import java.util.SortedSet; import java.util.TreeMap; import java.util.TreeSet; +import java.util.function.Consumer; import java.util.stream.Collectors; /** @@ -100,7 +101,7 @@ public static

List

computeSmus( * 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 + * 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 @@ -200,13 +201,8 @@ private static

List

computeSmusSAT( final OptimizationHandler handler) { 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())); - } + growSolver.add(nullSafe(additionalConstraints)); + final Map propositionMapping = createPropositionsMapping(propositions, growSolver::add, f); final boolean sat = growSolver.sat(satHandler(handler), propositionMapping.keySet()) == Tristate.TRUE; if (sat || aborted(handler)) { return null; @@ -230,26 +226,15 @@ private static

List

computeSmusSAT( private static

List

computeSmusMaxSAT( final List

propositions, - final List addConstraints, + final List additionalConstraints, 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)) { + final List growSolverConstraints = new ArrayList<>(nullSafe(additionalConstraints)); + final Map propositionMapping = createPropositionsMapping(propositions, growSolverConstraints::add, f); + final boolean sat = sat(growSolverConstraints, propositionMapping.keySet(), handler, f); + if (sat || aborted(handler)) { return null; } final List hSolverConstraints = new ArrayList<>(); @@ -269,6 +254,24 @@ private static

List

computeSmusMaxSAT( } } + private static

Map createPropositionsMapping( + final List

propositions, final Consumer consumer, 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); + consumer.accept(f.equivalence(selector, proposition.formula())); + } + return propositionMapping; + } + + private static boolean sat(final List constraints, final Set variables, final MaxSATHandler handler, final FormulaFactory f) { + final SATHandler satHandler = handler == null ? null : handler.satHandler(); + final SATSolver satSolver = MiniSat.miniSat(f); + satSolver.add(constraints); + return satSolver.sat(satHandler, variables) == Tristate.TRUE; + } + private static SortedSet minimumHs( final SATSolver hSolver, final Set variables, final OptimizationHandler handler) { final Assignment minimumHsModel = hSolver.execute(OptimizationFunction.builder() @@ -288,8 +291,9 @@ private static SortedSet minimumHs( for (final Variable v : variables) { maxSatSolver.addSoftFormula(v.negate(), 1); } - final MaxSAT.MaxSATResult result = maxSatSolver.solve(config.getMaxSATHandler()); - if (result == MaxSAT.MaxSATResult.UNDEF) { + final MaxSATHandler handler = config.getMaxSATHandler(); + final MaxSAT.MaxSATResult result = maxSatSolver.solve(handler); + if (result == MaxSAT.MaxSATResult.UNDEF || aborted(handler)) { return null; } return new TreeSet<>(maxSatSolver.model().positiveVariables()); @@ -309,11 +313,8 @@ private static SortedSet grow( if (maxModel == null || aborted(handler)) { return null; } else { - final List maximumSatisfiableSet = maxModel.positiveVariables(); growSolver.loadState(solverState); - final SortedSet minimumCorrectionSet = new TreeSet<>(variables); - maximumSatisfiableSet.forEach(minimumCorrectionSet::remove); - return minimumCorrectionSet; + return difference(variables, maxModel.positiveVariables(), TreeSet::new); } } @@ -329,18 +330,16 @@ private static SortedSet grow( for (final Variable v : variables) { maxSatSolver.addSoftFormula(v, 1); } - final MaxSAT.MaxSATResult result = maxSatSolver.solve(config.getMaxSATHandler()); - if (result == MaxSAT.MaxSATResult.UNDEF) { + final MaxSATHandler handler = config.getMaxSATHandler(); + final MaxSAT.MaxSATResult result = maxSatSolver.solve(handler); + if (result == MaxSAT.MaxSATResult.UNDEF || aborted(handler)) { 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; + return difference(variables, maxModel.positiveVariables(), TreeSet::new); } } } diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java index fde8a8a6..4eab4d82 100644 --- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java @@ -250,7 +250,7 @@ private Pair>, List>> computeMaxSAT( 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) { + if (result == MaxSAT.MaxSATResult.UNDEF || aborted(cfg.getMaxSATHandler())) { return null; } final Assignment hModel = hSolver.model(); diff --git a/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java index 1b4cf7ee..5627acb5 100644 --- a/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java +++ b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java @@ -19,7 +19,6 @@ * 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 */ @@ -53,8 +52,8 @@ private OptimizationConfig( /** * Generate a MaxSAT solver based configuration - * @param optType the optimization type (MaxSAT algorithm) - * @param maxConfig the optional MaxSAT solver 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 */ @@ -86,6 +85,14 @@ 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 @@ -127,7 +134,7 @@ public MaxSATSolver genMaxSATSolver(final FormulaFactory f) { } /** - * Starts the solver of this config's handler (if present) + * Starts this config's handler (if present) */ public void startHandler() { if (this.optimizationHandler != null) { diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java index cdfada01..3f491c05 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -28,8 +28,6 @@ package org.logicng.transformations.simplification; -import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.SAT_OPTIMIZATION; - import org.logicng.configurations.Configuration; import org.logicng.configurations.ConfigurationType; import org.logicng.handlers.OptimizationHandler; From b783c194805ea74420c6df6c03c1f04ab462a909 Mon Sep 17 00:00:00 2001 From: Rouven Walter Date: Fri, 2 Aug 2024 21:04:38 +0200 Subject: [PATCH 5/9] bugfix: added backbone literals to intermediate result in AdvancedSimplifier --- .../simplification/AdvancedSimplifier.java | 11 +++++++---- .../simplification/AdvancedSimplifierTest.java | 14 ++++++++++++++ 2 files changed, 21 insertions(+), 4 deletions(-) diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java index 594e2e70..c5fe33a3 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java @@ -142,16 +142,14 @@ public Formula apply(final Formula formula, final boolean cache) { } final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); if (simplifyMinDnf == null) { - return config.returnIntermediateResult ? simplified : null; + return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null; } 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); @@ -159,6 +157,11 @@ public Formula apply(final Formula formula, final boolean cache) { return simplified; } + 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.optimizationConfig); diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java index ec902ca3..64a87dee 100644 --- a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java +++ b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java @@ -35,6 +35,8 @@ 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; @@ -63,6 +65,7 @@ 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}. @@ -210,6 +213,17 @@ public void testAdvancedSimplifierConfig() { } } + @Test + public void testBackboneIntermediateResult() { + final FormulaFactory f = new FormulaFactory(); + Formula formula = parse(f, "(a & b) | (a & c)"); + 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))) From c03d34212a9a9b114be9b675e7f399517241e0b8 Mon Sep 17 00:00:00 2001 From: Rouven Walter Date: Fri, 2 Aug 2024 21:37:41 +0200 Subject: [PATCH 6/9] added minimalDnfCover config flag in AdvancedSimplifierConfig --- CHANGELOG.md | 6 ++++++ .../simplification/AdvancedSimplifier.java | 16 +++++++++------- .../simplification/AdvancedSimplifierConfig.java | 15 +++++++++++++++ .../simplification/AdvancedSimplifierTest.java | 10 ++++++---- 4 files changed, 36 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 40ca17f6..43bcfdba 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,12 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [2.6.0] - 2024-08-02 + +### Added + +- Added configuration flag `minimalDnfCover` in `AdvancedSimplifierConfig` to set whether the step for computing the minimal DNF cover should be performed. Default is `true`. + ## [2.5.1] - 2024-07-31 ### Changed diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java index c5fe33a3..5e28a285 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java @@ -135,16 +135,18 @@ public Formula apply(final Formula formula, final boolean cache) { return config.returnIntermediateResult ? formula : null; } if (!backbone.isSat()) { - return f.falsum(); + return f.falsum(); } backboneLiterals.addAll(backbone.getCompleteBackbone()); simplified = formula.restrict(new Assignment(backboneLiterals)); } - final Formula simplifyMinDnf = computeMinDnf(f, simplified, config); - if (simplifyMinDnf == null) { - return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : 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); @@ -164,13 +166,13 @@ private static Formula addLiterals(final Formula formula, final SortedSet> primeImplicants = primeResult.getPrimeImplicants(); final List minimizedPIs = SmusComputation.computeSmusForFormulas(negateAllLiterals(primeImplicants, f), - Collections.singletonList(simplified), f, config.optimizationConfig); + Collections.singletonList(simplified), f, config.optimizationConfig); if (minimizedPIs == null || config.optimizationConfig.aborted()) { return null; } diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java index 3f491c05..b9e941c2 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -42,6 +42,7 @@ public class AdvancedSimplifierConfig extends Configuration { boolean restrictBackbone; + boolean minimalDnfCover; boolean factorOut; boolean simplifyNegations; boolean returnIntermediateResult; @@ -52,6 +53,7 @@ public class AdvancedSimplifierConfig extends Configuration { public String toString() { return "AdvancedSimplifierConfig{" + "restrictBackbone=" + this.restrictBackbone + + ", minimalDnfCover=" + this.minimalDnfCover + ", factorOut=" + this.factorOut + ", simplifyNegations=" + this.simplifyNegations + ", returnIntermediateResult=" + this.returnIntermediateResult + @@ -67,6 +69,7 @@ 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; @@ -88,6 +91,7 @@ public static Builder builder() { public static class Builder { boolean restrictBackbone = true; + boolean minimalDnfCover = true; boolean factorOut = true; boolean simplifyNegations = true; boolean returnIntermediateResult = false; @@ -109,6 +113,17 @@ public Builder restrictBackbone(final boolean restrictBackbone) { return this; } + /** + * 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'. diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java index 64a87dee..1a9905e6 100644 --- a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java +++ b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java @@ -191,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()); @@ -216,11 +218,11 @@ public void testAdvancedSimplifierConfig() { @Test public void testBackboneIntermediateResult() { final FormulaFactory f = new FormulaFactory(); - Formula formula = parse(f, "(a & b) | (a & c)"); - OptimizationHandler optHandler = mock(OptimizationHandler.class); + 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); + when(optHandler.aborted()).then(invocationOnMock -> count.addAndGet(1) > 1); testHandler(optHandler, formula, true, true); } From 84a374cbd9a391289f604e8ff80409ff3d7f354e Mon Sep 17 00:00:00 2001 From: Rouven Walter Date: Fri, 2 Aug 2024 22:28:33 +0200 Subject: [PATCH 7/9] refactoring SmusComputation to avoid redundant code --- .../explanations/smus/SmusComputation.java | 311 ++++++++++-------- 1 file changed, 181 insertions(+), 130 deletions(-) diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java index 4a66ab9c..81c024a9 100644 --- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java @@ -30,8 +30,6 @@ 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 static org.logicng.util.CollectionHelper.difference; import static org.logicng.util.CollectionHelper.nullSafe; @@ -39,7 +37,9 @@ 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; @@ -52,15 +52,16 @@ 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.ArrayList; +import java.util.Collection; import java.util.List; import java.util.Map; import java.util.Set; import java.util.SortedSet; import java.util.TreeMap; import java.util.TreeSet; -import java.util.function.Consumer; import java.util.stream.Collectors; /** @@ -137,10 +138,29 @@ public static

List

computeSmus( 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); + final Handler handler = getHandler(config); + start(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 OptSolver hSolver = OptSolver.create(f, config); + while (true) { + final SortedSet h = hSolver.minimize(propositionMapping.keySet()); + if (h == null || aborted(handler)) { + return null; + } + 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.addConstraint(f.or(c)); } } @@ -194,152 +214,183 @@ public static List computeSmusForFormulas( 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(nullSafe(additionalConstraints)); - final Map propositionMapping = createPropositionsMapping(propositions, growSolver::add, f); - final boolean sat = growSolver.sat(satHandler(handler), propositionMapping.keySet()) == Tristate.TRUE; - if (sat || aborted(handler)) { - return null; - } - final SATSolver hSolver = MiniSat.miniSat(f); - while (true) { - final SortedSet h = minimumHs(hSolver, propositionMapping.keySet(), handler); - if (h == null || aborted(handler)) { - return null; - } - final SortedSet c = grow(growSolver, h, propositionMapping.keySet(), handler); - if (aborted(handler)) { - return null; - } - if (c == null) { - return h.stream().map(propositionMapping::get).collect(Collectors.toList()); - } - hSolver.add(f.or(c)); - } - } - - private static

List

computeSmusMaxSAT( - final List

propositions, - final List additionalConstraints, - final FormulaFactory f, - final OptimizationConfig config) { - final MaxSATHandler handler = config.getMaxSATHandler(); - start(handler); - final List growSolverConstraints = new ArrayList<>(nullSafe(additionalConstraints)); - final Map propositionMapping = createPropositionsMapping(propositions, growSolverConstraints::add, f); - final boolean sat = sat(growSolverConstraints, propositionMapping.keySet(), handler, f); - if (sat || aborted(handler)) { - 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 Handler getHandler(final OptimizationConfig config) { + return config.getOptimizationType() == OptimizationConfig.OptimizationType.SAT_OPTIMIZATION + ? config.getOptimizationHandler() + : config.getMaxSATHandler(); } private static

Map createPropositionsMapping( - final List

propositions, final Consumer consumer, final FormulaFactory f) { + 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); - consumer.accept(f.equivalence(selector, proposition.formula())); + solver.addConstraint(f.equivalence(selector, proposition.formula())); } return propositionMapping; } - private static boolean sat(final List constraints, final Set variables, final MaxSATHandler handler, final FormulaFactory f) { - final SATHandler satHandler = handler == null ? null : handler.satHandler(); - final SATSolver satSolver = MiniSat.miniSat(f); - satSolver.add(constraints); - return satSolver.sat(satHandler, variables) == Tristate.TRUE; + 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; + } + growSolver.loadState(); + return difference(variables, maxModel, TreeSet::new); } - 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 abstract static class OptSolver { + protected final FormulaFactory f; + protected final OptimizationConfig config; - private static SortedSet minimumHs( - final List constraints, - final Set variables, - final OptimizationConfig config, - final FormulaFactory f) { - final MaxSATSolver maxSatSolver = config.genMaxSATSolver(f); - constraints.forEach(maxSatSolver::addHardFormula); - for (final Variable v : variables) { - maxSatSolver.addSoftFormula(v.negate(), 1); + OptSolver(final FormulaFactory f, final OptimizationConfig config) { + this.f = f; + this.config = config; } - final MaxSATHandler handler = config.getMaxSATHandler(); - final MaxSAT.MaxSATResult result = maxSatSolver.solve(handler); - if (result == MaxSAT.MaxSATResult.UNDEF || aborted(handler)) { - return null; + + 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)); } - return new TreeSet<>(maxSatSolver.model().positiveVariables()); + + abstract boolean aborted(); } - 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)) { - return null; - } else { - growSolver.loadState(solverState); - return difference(variables, maxModel.positiveVariables(), TreeSet::new); + 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 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); + 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; } - final MaxSATHandler handler = config.getMaxSATHandler(); - final MaxSAT.MaxSATResult result = maxSatSolver.solve(handler); - if (result == MaxSAT.MaxSATResult.UNDEF || aborted(handler)) { - return null; + + @Override + void addConstraint(final Formula formula) { + this.constraints.add(formula); } - final Assignment maxModel = maxSatSolver.model(); - if (maxModel == null) { - return null; - } else { - return difference(variables, maxModel.positiveVariables(), TreeSet::new); + + @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()); } } } From 567a53fe217698186d03ff5bee8166269404ed0c Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Mon, 9 Sep 2024 18:15:27 +0200 Subject: [PATCH 8/9] updated changelog and made some fields private --- CHANGELOG.md | 10 +++++++++- .../simplification/AdvancedSimplifierConfig.java | 10 +++++----- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 43bcfdba..9b6c3cd2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,7 +6,15 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### Added -- Added configuration flag `minimalDnfCover` in `AdvancedSimplifierConfig` to set whether the step for computing the minimal DNF cover should be performed. Default is `true`. +- 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 diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java index b9e941c2..a89733e3 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -90,11 +90,11 @@ public static Builder builder() { */ public static class Builder { - boolean restrictBackbone = true; - boolean minimalDnfCover = true; - boolean factorOut = true; - boolean simplifyNegations = true; - boolean returnIntermediateResult = false; + 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); From 6fb3568a3a6b05293f24487d45a3db776e885282 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Mon, 9 Sep 2024 20:30:41 +0200 Subject: [PATCH 9/9] Final 2.6.0 --- CHANGELOG.md | 2 +- README.md | 2 +- pom.xml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b6c3cd2..5e21a70e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,7 +2,7 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [2.6.0] - 2024-08-02 +## [2.6.0] - 2024-09-10 ### Added 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 00fb5a6b..dfe8c374 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.6.0-SNAPSHOT + 2.6.0 bundle LogicNG