Skip to content

Commit

Permalink
minor refactoring and improvements
Browse files Browse the repository at this point in the history
  • Loading branch information
@rouven-walter
rouven-walter committed Aug 2, 2024
1 parent 18f3c72 commit 09e61b0
Show file tree
Hide file tree
Showing 4 changed files with 49 additions and 45 deletions.
75 changes: 37 additions & 38 deletions src/main/java/org/logicng/explanations/smus/SmusComputation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;

/**
Expand Down Expand Up @@ -100,7 +101,7 @@ public static <P extends Proposition> List<P> computeSmus(
* 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
* 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
Expand Down Expand Up @@ -200,13 +201,8 @@ private static <P extends Proposition> List<P> computeSmusSAT(
final OptimizationHandler handler) {
start(handler);
final SATSolver growSolver = MiniSat.miniSat(f);
growSolver.add(additionalConstraints == null ? Collections.singletonList(f.verum()) : 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);
growSolver.add(f.equivalence(selector, proposition.formula()));
}
growSolver.add(nullSafe(additionalConstraints));
final Map<Variable, P> propositionMapping = createPropositionsMapping(propositions, growSolver::add, f);
final boolean sat = growSolver.sat(satHandler(handler), propositionMapping.keySet()) == Tristate.TRUE;
if (sat || aborted(handler)) {
return null;
Expand All @@ -230,26 +226,15 @@ private static <P extends Proposition> List<P> computeSmusSAT(

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

private static <P extends Proposition> Map<Variable, P> createPropositionsMapping(
final List<P> propositions, final Consumer<Formula> consumer, final FormulaFactory f) {
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);
consumer.accept(f.equivalence(selector, proposition.formula()));
}
return propositionMapping;
}

private static boolean sat(final List<Formula> constraints, final Set<Variable> 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<Variable> minimumHs(
final SATSolver hSolver, final Set<Variable> variables, final OptimizationHandler handler) {
final Assignment minimumHsModel = hSolver.execute(OptimizationFunction.builder()
Expand All @@ -288,8 +291,9 @@ private static SortedSet<Variable> 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());
Expand All @@ -309,11 +313,8 @@ private static SortedSet<Variable> grow(
if (maxModel == null || aborted(handler)) {
return null;
} else {
final List<Variable> maximumSatisfiableSet = maxModel.positiveVariables();
growSolver.loadState(solverState);
final SortedSet<Variable> minimumCorrectionSet = new TreeSet<>(variables);
maximumSatisfiableSet.forEach(minimumCorrectionSet::remove);
return minimumCorrectionSet;
return difference(variables, maxModel.positiveVariables(), TreeSet::new);
}
}

Expand All @@ -329,18 +330,16 @@ private static SortedSet<Variable> 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<Variable> maximumSatisfiableSet = maxModel.positiveVariables();
final SortedSet<Variable> minimumCorrectionSet = new TreeSet<>(variables);
maximumSatisfiableSet.forEach(minimumCorrectionSet::remove);
return minimumCorrectionSet;
return difference(variables, maxModel.positiveVariables(), TreeSet::new);
}
}
}
2 changes: 1 addition & 1 deletion src/main/java/org/logicng/primecomputation/PrimeCompiler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ private Pair<List<SortedSet<Literal>>, List<SortedSet<Literal>>> 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();
Expand Down
15 changes: 11 additions & 4 deletions src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
* with the drawback of generating the solver again in each step.
* <p>
* These algorithms can be configured with this config object.
*
* @version 2.6.0
* @since 2.6.0
*/
Expand Down Expand Up @@ -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
*/
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) {
Expand Down
2 changes: 0 additions & 2 deletions src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down

0 comments on commit 09e61b0

Please sign in to comment.