Skip to content

Commit

Permalink
WIP configure optimization in algorithms
Browse files Browse the repository at this point in the history
  • Loading branch information
@czengler
czengler committed Jul 30, 2024
1 parent 5ba79db commit 8fb005a
Show file tree
Hide file tree
Showing 7 changed files with 446 additions and 110 deletions.
231 changes: 198 additions & 33 deletions src/main/java/org/logicng/explanations/smus/SmusComputation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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 {
Expand All @@ -82,24 +90,114 @@ 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 <P extends Proposition> List<P> computeSmus(final List<P> propositions, final List<Formula> additionalConstraints, final FormulaFactory f) {
return computeSmus(propositions, additionalConstraints, f, null);
public static <P extends Proposition> List<P> computeSmus(
final List<P> propositions, final List<Formula> 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.
* <p>
* 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 <P> the subtype of the propositions
* @param propositions the propositions
* @param additionalConstraints the additional constraints
* @param f the formula factory
* @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 <P extends Proposition> List<P> computeSmus(final List<P> propositions, final List<Formula> additionalConstraints, final FormulaFactory f,
final OptimizationHandler handler) {
public static <P extends Proposition> List<P> computeSmus(
final List<P> propositions,
final List<Formula> 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.
* <p>
* 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 <P> 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 <P extends Proposition> List<P> computeSmus(
final List<P> propositions,
final List<Formula> 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<Formula> computeSmusForFormulas(
final List<Formula> formulas,
final List<Formula> 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<Formula> computeSmusForFormulas(
final List<Formula> formulas,
final List<Formula> 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<Formula> computeSmusForFormulas(
final List<Formula> formulas,
final List<Formula> additionalConstraints,
final FormulaFactory f,
final OptimizationConfig config) {
final List<Proposition> props = formulas.stream().map(StandardProposition::new).collect(Collectors.toList());
final List<Proposition> smus = computeSmus(props, additionalConstraints, f, config);
return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList());
}

private static <P extends Proposition> List<P> computeSmusSat(
final List<P> propositions,
final List<Formula> additionalConstraints,
final FormulaFactory f,
final OptimizationHandler handler) {
start(handler);
final SATSolver growSolver = MiniSat.miniSat(f);
growSolver.add(additionalConstraints == null ? Collections.singletonList(f.verum()) : additionalConstraints);
Expand Down Expand Up @@ -130,41 +228,81 @@ public static <P extends Proposition> List<P> computeSmus(final List<P> 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<Formula> computeSmusForFormulas(final List<Formula> formulas, final List<Formula> 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<Formula> computeSmusForFormulas(final List<Formula> formulas, final List<Formula> additionalConstraints, final FormulaFactory f,
final OptimizationHandler handler) {
final List<Proposition> props = formulas.stream().map(StandardProposition::new).collect(Collectors.toList());
final List<Proposition> smus = computeSmus(props, additionalConstraints, f, handler);
return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList());
private static <P extends Proposition> List<P> computeSmusMaxSAT(
final List<P> propositions,
final List<Formula> addConstraints,
final FormulaFactory f,
final OptimizationConfig config) {
final MaxSATHandler handler = config.getMaxSATHandler();
start(handler);
final Collection<? extends Formula> additionalConstraints = addConstraints == null
? Collections.singletonList(f.verum())
: addConstraints;
final List<Formula> growSolverConstraints = new ArrayList<>(additionalConstraints);
final Map<Variable, P> 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<Formula> hSolverConstraints = new ArrayList<>();
while (true) {
final SortedSet<Variable> h = minimumHs(hSolverConstraints, propositionMapping.keySet(), config, f);
if (h == null || aborted(handler)) {
return null;
}
final SortedSet<Variable> 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<Variable> minimumHs(final SATSolver hSolver, final Set<Variable> variables, final OptimizationHandler handler) {
private static SortedSet<Variable> minimumHs(
final SATSolver hSolver, final Set<Variable> variables, final OptimizationHandler handler) {
final Assignment minimumHsModel = hSolver.execute(OptimizationFunction.builder()
.handler(handler)
.literals(variables)
.minimize().build());
return aborted(handler) ? null : new TreeSet<>(minimumHsModel.positiveVariables());
}

private static SortedSet<Variable> grow(final SATSolver growSolver, final SortedSet<Variable> h, final Set<Variable> variables, final OptimizationHandler handler) {
private static SortedSet<Variable> minimumHs(
final List<Formula> constraints,
final Set<Variable> 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<Variable> grow(
final SATSolver growSolver,
final SortedSet<Variable> h,
final Set<Variable> variables,
final OptimizationHandler handler) {
final SolverState solverState = growSolver.saveState();
growSolver.add(h);
final Assignment maxModel = growSolver.execute(OptimizationFunction.builder()
Expand All @@ -181,4 +319,31 @@ private static SortedSet<Variable> grow(final SATSolver growSolver, final Sorted
return minimumCorrectionSet;
}
}

private static SortedSet<Variable> grow(
final List<Formula> constraints,
final SortedSet<Variable> h,
final Set<Variable> 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<Variable> maximumSatisfiableSet = maxModel.positiveVariables();
final SortedSet<Variable> minimumCorrectionSet = new TreeSet<>(variables);
maximumSatisfiableSet.forEach(minimumCorrectionSet::remove);
return minimumCorrectionSet;
}
}
}
32 changes: 28 additions & 4 deletions src/main/java/org/logicng/primecomputation/PrimeCompiler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
}

/**
Expand All @@ -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
Expand Down Expand Up @@ -167,7 +189,9 @@ private Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> computeGeneric(
return null;
}
if (fSat == Tristate.FALSE) {
final SortedSet<Literal> primeImplicant = this.computeWithMaximization ? primeReduction.reduceImplicant(fModel.literals(), satHandler(handler)) : fModel.literals();
final SortedSet<Literal> primeImplicant = this.computeWithMaximization
? primeReduction.reduceImplicant(fModel.literals(), satHandler(handler))
: fModel.literals();
if (primeImplicant == null || aborted(handler)) {
return null;
}
Expand Down
Loading

0 comments on commit 8fb005a

Please sign in to comment.