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"));
}