Skip to content

Commit

Permalink
Optimization config in advanced simplifier
Browse files Browse the repository at this point in the history
  • Loading branch information
@czengler
czengler committed Aug 1, 2024
1 parent f72daf2 commit 18f3c72
Show file tree
Hide file tree
Showing 8 changed files with 277 additions and 89 deletions.
8 changes: 4 additions & 4 deletions src/main/java/org/logicng/explanations/smus/SmusComputation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ private SmusComputation() {
*/
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);
final OptimizationConfig cfg = OptimizationConfig.sat(null);
return computeSmus(propositions, additionalConstraints, f, cfg);
}

Expand All @@ -114,7 +114,7 @@ public static <P extends Proposition> List<P> computeSmus(
final List<Formula> 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);
}

Expand Down Expand Up @@ -154,7 +154,7 @@ 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);
final OptimizationConfig cfg = OptimizationConfig.sat(null);
return computeSmusForFormulas(formulas, additionalConstraints, f, cfg);
}

Expand All @@ -171,7 +171,7 @@ public static List<Formula> computeSmusForFormulas(
final List<Formula> 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);
}

Expand Down
4 changes: 2 additions & 2 deletions src/main/java/org/logicng/primecomputation/PrimeCompiler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}

/**
Expand All @@ -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));
}

/**
Expand Down
105 changes: 100 additions & 5 deletions src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
* <p>
* 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.
* <p>
* 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,
Expand All @@ -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,
Expand All @@ -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:
Expand All @@ -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) {
Expand Down
62 changes: 36 additions & 26 deletions src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -59,7 +69,7 @@
* </ul>
* 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 {
Expand Down Expand Up @@ -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<Literal> 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) {
Expand All @@ -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<SortedSet<Literal>> primeImplicants = primeResult.getPrimeImplicants();
//final List<Formula> 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<SortedSet<Literal>> primeImplicants = primeResult.getPrimeImplicants();
final List<Formula> 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<Formula> negateAllLiterals(final Collection<SortedSet<Literal>> literalSets, final FormulaFactory f) {
Expand Down
Loading

0 comments on commit 18f3c72

Please sign in to comment.