Skip to content

Commit

Permalink
introduce LNGResult
Browse files Browse the repository at this point in the history
  • Loading branch information
@SHildebrandt
SHildebrandt committed Jul 2, 2024
1 parent 90f441d commit 662f7bf
Show file tree
Hide file tree
Showing 175 changed files with 2,995 additions and 2,682 deletions.
15 changes: 8 additions & 7 deletions src/main/java/com/booleworks/logicng/backbones/BackboneGeneration.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
import com.booleworks.logicng.formulas.FormulaFactory;
import com.booleworks.logicng.formulas.Variable;
import com.booleworks.logicng.handlers.ComputationHandler;
import com.booleworks.logicng.handlers.LNGResult;
import com.booleworks.logicng.handlers.NopHandler;
import com.booleworks.logicng.solvers.SATSolver;
import com.booleworks.logicng.solvers.functions.BackboneFunction;
Expand Down Expand Up @@ -46,16 +47,16 @@ private BackboneGeneration() {
* @return the backbone or {@code null} if the computation was aborted by
* the handler
*/
public static Backbone compute(final FormulaFactory f, final Collection<Formula> formulas,
final Collection<Variable> variables, final BackboneType type,
final ComputationHandler handler) {
public static LNGResult<Backbone> compute(final FormulaFactory f, final Collection<Formula> formulas,
final Collection<Variable> variables, final BackboneType type,
final ComputationHandler handler) {
if (formulas == null || formulas.isEmpty()) {
throw new IllegalArgumentException("Provide at least one formula for backbone computation");
}
final SATSolver solver = SATSolver.newSolver(f,
SATSolverConfig.builder().cnfMethod(SATSolverConfig.CNFMethod.PG_ON_SOLVER).build());
solver.add(formulas);
return solver.execute(BackboneFunction.builder().handler(handler).variables(variables).type(type).build());
return solver.execute(BackboneFunction.builder().variables(variables).type(type).build(), handler);
}

/**
Expand All @@ -70,7 +71,7 @@ public static Backbone compute(final FormulaFactory f, final Collection<Formula>
*/
public static Backbone compute(final FormulaFactory f, final Collection<Formula> formulas,
final Collection<Variable> variables, final BackboneType type) {
return compute(f, formulas, variables, type, NopHandler.get());
return compute(f, formulas, variables, type, NopHandler.get()).getResult();
}

/**
Expand Down Expand Up @@ -120,8 +121,8 @@ public static Backbone compute(final FormulaFactory f, final Collection<Formula>
* @param type the type of backbone variables that should be computed
* @return the backbone
*/
public static Backbone compute(final FormulaFactory f, final Formula formula, final Collection<Variable> variables,
final BackboneType type) {
public static Backbone compute(final FormulaFactory f, final Formula formula,
final Collection<Variable> variables, final BackboneType type) {
return compute(f, Collections.singletonList(formula), variables, type);
}

Expand Down
31 changes: 17 additions & 14 deletions src/main/java/com/booleworks/logicng/explanations/mus/DeletionBasedMUS.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@
package com.booleworks.logicng.explanations.mus;

import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.MUS_COMPUTATION_STARTED;
import static com.booleworks.logicng.handlers.events.SimpleEvent.NO_EVENT;

import com.booleworks.logicng.datastructures.Tristate;
import com.booleworks.logicng.explanations.UNSATCore;
import com.booleworks.logicng.formulas.FormulaFactory;
import com.booleworks.logicng.handlers.ComputationHandler;
import com.booleworks.logicng.handlers.LNGResult;
import com.booleworks.logicng.propositions.Proposition;
import com.booleworks.logicng.solvers.SATSolver;
import com.booleworks.logicng.solvers.SolverState;
Expand All @@ -25,36 +25,39 @@
public final class DeletionBasedMUS extends MUSAlgorithm {

@Override
public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, final List<T> propositions,
final MUSConfig config) {
config.handler.shouldResume(MUS_COMPUTATION_STARTED);
public <T extends Proposition> LNGResult<UNSATCore<T>> computeMUS(
final FormulaFactory f, final List<T> propositions,
final MUSConfig config, final ComputationHandler handler) {
if (!handler.shouldResume(MUS_COMPUTATION_STARTED)) {
return LNGResult.aborted(MUS_COMPUTATION_STARTED);
}
final List<T> mus = new ArrayList<>(propositions.size());
final List<SolverState> solverStates = new ArrayList<>(propositions.size());
final SATSolver solver = SATSolver.newSolver(f);
for (final Proposition proposition : propositions) {
solverStates.add(solver.saveState());
solver.add(proposition);
}
boolean sat = solver.satCall().handler(config.handler).sat() == Tristate.TRUE;
if (!config.handler.shouldResume(NO_EVENT)) {
return null;
LNGResult<Boolean> sat = solver.satCall().handler(handler).sat();
if (!sat.isSuccess()) {
return LNGResult.aborted(sat.getAbortionEvent());
}
if (sat) {
if (sat.getResult()) {
throw new IllegalArgumentException("Cannot compute a MUS for a satisfiable formula set.");
}
for (int i = solverStates.size() - 1; i >= 0; i--) {
solver.loadState(solverStates.get(i));
for (final Proposition prop : mus) {
solver.add(prop);
}
sat = solver.satCall().handler(config.handler).sat() == Tristate.TRUE;
if (!config.handler.shouldResume(NO_EVENT)) {
return null;
sat = solver.satCall().handler(handler).sat();
if (!sat.isSuccess()) {
return LNGResult.aborted(sat.getAbortionEvent());
}
if (sat) {
if (sat.getResult()) {
mus.add(propositions.get(i));
}
}
return new UNSATCore<>(mus, true);
return LNGResult.of(new UNSATCore<>(mus, true));
}
}
32 changes: 27 additions & 5 deletions src/main/java/com/booleworks/logicng/explanations/mus/MUSAlgorithm.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,16 @@

import com.booleworks.logicng.explanations.UNSATCore;
import com.booleworks.logicng.formulas.FormulaFactory;
import com.booleworks.logicng.handlers.ComputationHandler;
import com.booleworks.logicng.handlers.LNGResult;
import com.booleworks.logicng.handlers.NopHandler;
import com.booleworks.logicng.propositions.Proposition;

import java.util.List;

/**
* Abstract super class for MUS computation algorithms.
* @version 2.1.0
* @version 3.0.0
* @since 1.1
*/
abstract class MUSAlgorithm {
Expand All @@ -23,9 +26,28 @@ abstract class MUSAlgorithm {
* @param f the formula factory
* @param propositions the propositions
* @param config the MUS configuration
* @return the MUS or null if the MUS computation was configured with a
* handler and this handler aborted the computation
* @param handler the computation handler
* @return an LNG result containing the MUS (unless the handler aborted
* the computation)
* @throws IllegalArgumentException if the set of propositions is
* satisfiable
*/
public abstract <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, final List<T> propositions,
final MUSConfig config);
public abstract <T extends Proposition> LNGResult<UNSATCore<T>> computeMUS(
final FormulaFactory f, final List<T> propositions,
final MUSConfig config, final ComputationHandler handler);

/**
* Computes a MUS for the given propositions.
* @param <T> the type of the MUSes propositions
* @param f the formula factory
* @param propositions the propositions
* @param config the MUS configuration
* @return the MUS
* @throws IllegalArgumentException if the set of propositions is
* satisfiable
*/
public <T extends Proposition> UNSATCore<T> computeMUS(
final FormulaFactory f, final List<T> propositions, final MUSConfig config) {
return computeMUS(f, propositions, config, NopHandler.get()).getResult();
}
}
15 changes: 0 additions & 15 deletions src/main/java/com/booleworks/logicng/explanations/mus/MUSConfig.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@

import com.booleworks.logicng.configurations.Configuration;
import com.booleworks.logicng.configurations.ConfigurationType;
import com.booleworks.logicng.handlers.ComputationHandler;
import com.booleworks.logicng.handlers.NopHandler;

/**
* The configuration object for the MUS generation.
Expand All @@ -25,7 +23,6 @@ public enum Algorithm {
}

final Algorithm algorithm;
final ComputationHandler handler;

/**
* Constructs a new configuration with a given type.
Expand All @@ -34,7 +31,6 @@ public enum Algorithm {
private MUSConfig(final Builder builder) {
super(ConfigurationType.MUS);
algorithm = builder.algorithm;
handler = builder.handler;
}

/**
Expand All @@ -59,7 +55,6 @@ public String toString() {
public static class Builder {

private Algorithm algorithm = Algorithm.DELETION;
private ComputationHandler handler = NopHandler.get();

private Builder() {
// Initialize only via factory
Expand All @@ -76,16 +71,6 @@ public Builder algorithm(final Algorithm algorithm) {
return this;
}

/**
* Sets the SAT handler for the MUS generation.
* @param handler the SAT handler
* @return the current builder
*/
public Builder handler(final ComputationHandler handler) {
this.handler = handler;
return this;
}

/**
* Builds the configuration.
* @return the configuration.
Expand Down
23 changes: 21 additions & 2 deletions src/main/java/com/booleworks/logicng/explanations/mus/MUSGeneration.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,9 @@
import com.booleworks.logicng.configurations.ConfigurationType;
import com.booleworks.logicng.explanations.UNSATCore;
import com.booleworks.logicng.formulas.FormulaFactory;
import com.booleworks.logicng.handlers.ComputationHandler;
import com.booleworks.logicng.handlers.LNGResult;
import com.booleworks.logicng.handlers.NopHandler;
import com.booleworks.logicng.propositions.Proposition;

import java.util.List;
Expand Down Expand Up @@ -53,14 +56,30 @@ public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, f
*/
public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, final List<T> propositions,
final MUSConfig config) {
return computeMUS(f, propositions, config, NopHandler.get()).getResult();
}

/**
* Computes a MUS for the given propositions and the given configuration of
* the MUS generation.
* @param <T> the type of the MUSes propositions
* @param f the formula factory
* @param propositions the propositions
* @param config the MUS configuration
* @param handler the computation handler
* @return the MUS
*/
public <T extends Proposition> LNGResult<UNSATCore<T>> computeMUS(
final FormulaFactory f, final List<T> propositions,
final MUSConfig config, final ComputationHandler handler) {
if (propositions.isEmpty()) {
throw new IllegalArgumentException("Cannot generate a MUS for an empty list of propositions");
}
switch (config.algorithm) {
case PLAIN_INSERTION:
return insertion.computeMUS(f, propositions, config);
return insertion.computeMUS(f, propositions, config, handler);
case DELETION:
return deletion.computeMUS(f, propositions, config);
return deletion.computeMUS(f, propositions, config, handler);
default:
throw new IllegalStateException("Unknown MUS algorithm: " + config.algorithm);
}
Expand Down
30 changes: 16 additions & 14 deletions src/main/java/com/booleworks/logicng/explanations/mus/PlainInsertionBasedMUS.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,11 @@
package com.booleworks.logicng.explanations.mus;

import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.MUS_COMPUTATION_STARTED;
import static com.booleworks.logicng.handlers.events.SimpleEvent.NO_EVENT;

import com.booleworks.logicng.datastructures.Tristate;
import com.booleworks.logicng.explanations.UNSATCore;
import com.booleworks.logicng.formulas.FormulaFactory;
import com.booleworks.logicng.handlers.ComputationHandler;
import com.booleworks.logicng.handlers.LNGResult;
import com.booleworks.logicng.propositions.Proposition;
import com.booleworks.logicng.solvers.SATSolver;

Expand All @@ -25,9 +24,12 @@
public class PlainInsertionBasedMUS extends MUSAlgorithm {

@Override
public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, final List<T> propositions,
final MUSConfig config) {
config.handler.shouldResume(MUS_COMPUTATION_STARTED);
public <T extends Proposition> LNGResult<UNSATCore<T>> computeMUS(
final FormulaFactory f, final List<T> propositions,
final MUSConfig config, final ComputationHandler handler) {
if (!handler.shouldResume(MUS_COMPUTATION_STARTED)) {
return LNGResult.aborted(MUS_COMPUTATION_STARTED);
}
final List<T> currentFormula = new ArrayList<>(propositions.size());
currentFormula.addAll(propositions);
final List<T> mus = new ArrayList<>(propositions.size());
Expand All @@ -39,7 +41,14 @@ public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, f
solver.add(p);
}
int count = currentFormula.size();
while (shouldProceed(solver, config.handler)) {
while (true) {
final LNGResult<Boolean> sat = solver.satCall().handler(handler).sat();
if (!sat.isSuccess()) {
return LNGResult.aborted(sat.getAbortionEvent());
}
if (!sat.getResult()) {
break;
}
if (count == 0) {
throw new IllegalArgumentException("Cannot compute a MUS for a satisfiable formula set.");
}
Expand All @@ -48,21 +57,14 @@ public <T extends Proposition> UNSATCore<T> computeMUS(final FormulaFactory f, f
transitionProposition = removeProposition;
solver.add(removeProposition);
}
if (!config.handler.shouldResume(NO_EVENT)) {
return null;
}
currentFormula.clear();
currentFormula.addAll(currentSubset);
if (transitionProposition != null) {
currentFormula.remove(transitionProposition);
mus.add(transitionProposition);
}
}
return new UNSATCore<>(mus, true);
return LNGResult.of(new UNSATCore<>(mus, true));
}

private static boolean shouldProceed(final SATSolver solver, final ComputationHandler handler) {
final boolean sat = solver.satCall().handler(handler).sat() == Tristate.TRUE;
return sat && handler.shouldResume(NO_EVENT);
}
}
Loading

0 comments on commit 662f7bf

Please sign in to comment.