additionalConstraints, final FormulaFactory f) {
+ final OptimizationConfig cfg = OptimizationConfig.sat(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,35 +111,56 @@ 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 = OptimizationConfig.sat(handler);
+ 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) {
+ final Handler handler = getHandler(config);
start(handler);
- final SATSolver growSolver = MiniSat.miniSat(f);
- growSolver.add(additionalConstraints == null ? Collections.singletonList(f.verum()) : additionalConstraints);
- final Map 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()));
- }
- final boolean sat = growSolver.sat(satHandler(handler), propositionMapping.keySet()) == Tristate.TRUE;
- if (sat || aborted(handler)) {
+ final OptSolver growSolver = OptSolver.create(f, config);
+ growSolver.addConstraint(nullSafe(additionalConstraints));
+ final Map propositionMapping = createPropositionsMapping(propositions, growSolver, f);
+ final boolean sat = growSolver.sat(propositionMapping.keySet());
+ if (sat || growSolver.aborted()) {
return null;
}
- final SATSolver hSolver = MiniSat.miniSat(f);
+ final OptSolver hSolver = OptSolver.create(f, config);
while (true) {
- final SortedSet h = minimumHs(hSolver, propositionMapping.keySet(), handler);
+ final SortedSet h = hSolver.minimize(propositionMapping.keySet());
if (h == null || aborted(handler)) {
return null;
}
- final SortedSet c = grow(growSolver, h, propositionMapping.keySet(), handler);
+ final SortedSet c = grow(growSolver, h, propositionMapping.keySet());
if (aborted(handler)) {
return null;
}
if (c == null) {
return h.stream().map(propositionMapping::get).collect(Collectors.toList());
}
- hSolver.add(f.or(c));
+ hSolver.addConstraint(f.or(c));
}
}
@@ -137,8 +171,12 @@ public static List
computeSmus(final List
proposit
* @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);
+ public static List computeSmusForFormulas(
+ final List formulas,
+ final List additionalConstraints,
+ final FormulaFactory f) {
+ final OptimizationConfig cfg = OptimizationConfig.sat(null);
+ return computeSmusForFormulas(formulas, additionalConstraints, f, cfg);
}
/**
@@ -149,36 +187,210 @@ public static List computeSmusForFormulas(final List formulas,
* @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) {
+ public static List computeSmusForFormulas(
+ final List formulas,
+ final List additionalConstraints,
+ final FormulaFactory f,
+ final OptimizationHandler handler) {
+ final OptimizationConfig cfg = OptimizationConfig.sat(handler);
+ 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, handler);
+ final List smus = computeSmus(props, additionalConstraints, f, config);
return smus == null ? null : smus.stream().map(Proposition::formula).collect(Collectors.toList());
}
- private static SortedSet minimumHs(final SATSolver hSolver, final Set 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 Handler getHandler(final OptimizationConfig config) {
+ return config.getOptimizationType() == OptimizationConfig.OptimizationType.SAT_OPTIMIZATION
+ ? config.getOptimizationHandler()
+ : config.getMaxSATHandler();
}
- 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()
- .handler(handler)
- .literals(variables)
- .maximize().build());
- if (maxModel == null || aborted(handler)) {
+ private static Map createPropositionsMapping(
+ final List propositions, final OptSolver solver, final FormulaFactory f) {
+ final Map propositionMapping = new TreeMap<>();
+ for (final P proposition : propositions) {
+ final Variable selector = f.variable(PROPOSITION_SELECTOR + propositionMapping.size());
+ propositionMapping.put(selector, proposition);
+ solver.addConstraint(f.equivalence(selector, proposition.formula()));
+ }
+ return propositionMapping;
+ }
+
+ private static SortedSet grow(final OptSolver growSolver, final SortedSet h, final Set variables) {
+ growSolver.saveState();
+ growSolver.addConstraint(h);
+ final SortedSet maxModel = growSolver.maximize(variables);
+ if (maxModel == null) {
return null;
- } else {
- final List maximumSatisfiableSet = maxModel.positiveVariables();
- growSolver.loadState(solverState);
- final SortedSet minimumCorrectionSet = new TreeSet<>(variables);
- maximumSatisfiableSet.forEach(minimumCorrectionSet::remove);
- return minimumCorrectionSet;
+ }
+ growSolver.loadState();
+ return difference(variables, maxModel, TreeSet::new);
+ }
+
+ private abstract static class OptSolver {
+ protected final FormulaFactory f;
+ protected final OptimizationConfig config;
+
+ OptSolver(final FormulaFactory f, final OptimizationConfig config) {
+ this.f = f;
+ this.config = config;
+ }
+
+ public static OptSolver create(final FormulaFactory f, final OptimizationConfig config) {
+ if (config.getOptimizationType() == OptimizationConfig.OptimizationType.SAT_OPTIMIZATION) {
+ return new SatOptSolver(f, config);
+ } else {
+ return new MaxSatOptSolver(f, config);
+ }
+ }
+
+ abstract void addConstraint(final Formula formula);
+
+ abstract void addConstraint(final Collection formulas);
+
+ abstract boolean sat(final Collection variables);
+
+ abstract void saveState();
+
+ abstract void loadState();
+
+ abstract SortedSet maximize(final Collection targetLiterals);
+
+ SortedSet minimize(final Collection targetLiterals) {
+ return maximize(FormulaHelper.negateLiterals(targetLiterals, TreeSet::new));
+ }
+
+ abstract boolean aborted();
+ }
+
+ private static class SatOptSolver extends OptSolver {
+ private final MiniSat solver;
+ private SolverState state;
+
+ SatOptSolver(final FormulaFactory f, final OptimizationConfig config) {
+ super(f, config);
+ this.solver = MiniSat.miniSat(f);
+ this.state = null;
+ }
+
+ @Override
+ void addConstraint(final Formula formula) {
+ this.solver.add(formula);
+ }
+
+ @Override
+ void addConstraint(final Collection formulas) {
+ this.solver.add(formulas);
+ }
+
+ @Override
+ boolean sat(final Collection variables) {
+ final SATHandler satHandler = this.config.getOptimizationHandler() == null ? null : this.config.getOptimizationHandler().satHandler();
+ return this.solver.sat(satHandler, variables) == Tristate.TRUE;
+ }
+
+ @Override
+ void saveState() {
+ this.state = this.solver.saveState();
+ }
+
+ @Override
+ void loadState() {
+ if (this.state != null) {
+ this.solver.loadState(this.state);
+ this.state = null;
+ }
+ }
+
+ @Override
+ SortedSet maximize(final Collection targetLiterals) {
+ final OptimizationFunction optFunction = OptimizationFunction.builder()
+ .handler(this.config.getOptimizationHandler())
+ .literals(targetLiterals)
+ .maximize().build();
+ final Assignment model = this.solver.execute(optFunction);
+ return model == null || aborted() ? null : new TreeSet<>(model.positiveVariables());
+ }
+
+ @Override
+ boolean aborted() {
+ return Handler.aborted(this.config.getOptimizationHandler());
+ }
+ }
+
+ private static class MaxSatOptSolver extends OptSolver {
+ private List constraints;
+ private int saveIdx;
+
+ public MaxSatOptSolver(final FormulaFactory f, final OptimizationConfig config) {
+ super(f, config);
+ this.constraints = new ArrayList<>();
+ this.saveIdx = -1;
+ }
+
+ @Override
+ void addConstraint(final Formula formula) {
+ this.constraints.add(formula);
+ }
+
+ @Override
+ void addConstraint(final Collection formulas) {
+ this.constraints.addAll(formulas);
+ }
+
+ @Override
+ boolean sat(final Collection variables) {
+ final SATHandler satHandler = this.config.getMaxSATHandler() == null ? null : this.config.getMaxSATHandler().satHandler();
+ final SATSolver satSolver = MiniSat.miniSat(this.f);
+ satSolver.add(this.constraints);
+ return satSolver.sat(satHandler, variables) == Tristate.TRUE;
+ }
+
+ @Override
+ void saveState() {
+ this.saveIdx = this.constraints.size();
+ }
+
+ @Override
+ void loadState() {
+ if (this.saveIdx != -1) {
+ this.constraints = this.constraints.subList(0, this.saveIdx);
+ this.saveIdx = -1;
+ }
+ }
+
+ @Override
+ SortedSet maximize(final Collection targetLiterals) {
+ final MaxSATSolver maxSatSolver = this.config.genMaxSATSolver(this.f);
+ this.constraints.forEach(maxSatSolver::addHardFormula);
+ for (final Literal lit : targetLiterals) {
+ maxSatSolver.addSoftFormula(lit, 1);
+ }
+ final MaxSATHandler handler = this.config.getMaxSATHandler();
+ final MaxSAT.MaxSATResult result = maxSatSolver.solve(handler);
+ return result == MaxSAT.MaxSATResult.UNDEF || result == MaxSAT.MaxSATResult.UNSATISFIABLE || aborted()
+ ? null
+ : new TreeSet<>(maxSatSolver.model().positiveVariables());
+ }
+
+ @Override
+ boolean aborted() {
+ return Handler.aborted(this.config.getMaxSATHandler());
}
}
}
diff --git a/src/main/java/org/logicng/formulas/FormulaFactory.java b/src/main/java/org/logicng/formulas/FormulaFactory.java
index 664df73c..2a082926 100644
--- a/src/main/java/org/logicng/formulas/FormulaFactory.java
+++ b/src/main/java/org/logicng/formulas/FormulaFactory.java
@@ -45,8 +45,6 @@
import org.logicng.formulas.cache.CacheEntry;
import org.logicng.formulas.printer.FormulaStringRepresentation;
import org.logicng.functions.SubNodeFunction;
-import org.logicng.io.parsers.ParserException;
-import org.logicng.io.parsers.PseudoBooleanParser;
import org.logicng.pseudobooleans.PBConfig;
import org.logicng.pseudobooleans.PBEncoder;
import org.logicng.solvers.maxsat.algorithms.MaxSATConfig;
@@ -80,7 +78,7 @@
*
* A formula factory is NOT thread-safe. If you generate formulas from more than one thread you either need to synchronize the formula factory
* yourself or you use a formula factory for each single thread.
- * @version 2.4.0
+ * @version 2.5.0
* @since 1.0
*/
public class FormulaFactory {
@@ -103,7 +101,6 @@ public class FormulaFactory {
private final SubNodeFunction subformulaFunction;
private final PBEncoder pbEncoder;
private final CNFEncoder cnfEncoder;
- private final PseudoBooleanParser parser;
Map posLiterals;
Map negLiterals;
Set generatedVariables;
@@ -155,7 +152,6 @@ public FormulaFactory(final FormulaFactoryConfig config) {
this.cnfPrefix = CNF_PREFIX;
}
this.pbEncoder = new PBEncoder(this);
- this.parser = new PseudoBooleanParser(this);
}
/**
@@ -802,6 +798,84 @@ private Formula constructOr(final LinkedHashSet operandsIn) {
return or;
}
+ /**
+ * Creates a new DNF from an array of terms (conjunctions of literals).
+ *
+ * ATTENTION: it is assumed that the operands are really terms - this is not checked for performance reasons.
+ * Also, no reduction of operands is performed - this method should only be used if you are sure that the DNF is free
+ * of redundant terms.
+ * @param terms the array of terms
+ * @return a new DNF
+ */
+ public Formula dnf(final Formula... terms) {
+ final LinkedHashSet ops = new LinkedHashSet<>(terms.length);
+ Collections.addAll(ops, terms);
+ return this.constructDNF(ops);
+ }
+
+ /**
+ * Creates a new DNF from a collection of terms (conjunctions of literals).
+ *
+ * ATTENTION: it is assumed that the operands are really terms - this is not checked for performance reasons.
+ * Also, no reduction of operands is performed - this method should only be used if you are sure that the DNF is free
+ * of redundant terms.
+ * @param terms the collection of terms
+ * @return a new DNF
+ */
+ public Formula dnf(final Collection terms) {
+ final LinkedHashSet ops = new LinkedHashSet<>(terms);
+ return this.constructDNF(ops);
+ }
+
+ /**
+ * Creates a new DNF.
+ * @param termsIn the terms
+ * @return a new DNF
+ */
+ private Formula constructDNF(final LinkedHashSet termsIn) {
+ final LinkedHashSet terms = importOrPanic(termsIn);
+ if (terms.isEmpty()) {
+ return this.falsum();
+ }
+ if (terms.size() == 1) {
+ return terms.iterator().next();
+ }
+ Map, Or> opOrMap = this.orsN;
+ switch (terms.size()) {
+ case 2:
+ opOrMap = this.ors2;
+ break;
+ case 3:
+ opOrMap = this.ors3;
+ break;
+ case 4:
+ opOrMap = this.ors4;
+ break;
+ default:
+ break;
+ }
+ Or tempOr = opOrMap.get(terms);
+ if (tempOr != null) {
+ return tempOr;
+ }
+ tempOr = new Or(terms, this);
+ setCnfCaches(tempOr, isCnf(termsIn));
+ opOrMap.put(terms, tempOr);
+ return tempOr;
+ }
+
+ private static boolean isCnf(final LinkedHashSet terms) {
+ if (terms.size() <= 1) {
+ return true;
+ }
+ for (final Formula term : terms) {
+ if (term.type() != LITERAL) {
+ return false;
+ }
+ }
+ return true;
+ }
+
/**
* Creates a new clause from an array of literals.
*
@@ -866,6 +940,70 @@ private Formula constructClause(final LinkedHashSet literalsIn) {
return tempOr;
}
+ /**
+ * Creates a new term from an array of literals.
+ *
+ * ATTENTION: No reduction of operands is performed - this method should only be used if you are sure that the term
+ * is free of redundant or contradicting literals.
+ * @param literals the collection of literals
+ * @return a new term
+ */
+ public Formula term(final Literal... literals) {
+ final LinkedHashSet ops = new LinkedHashSet<>(literals.length);
+ Collections.addAll(ops, literals);
+ return this.constructTerm(ops);
+ }
+
+ /**
+ * Creates a new term from a collection of literals.
+ *
+ * ATTENTION: No reduction of operands is performed - this method should only be used if you are sure that the term
+ * is free of contradicting literals.
+ * @param literals the collection of literals
+ * @return a new term
+ */
+ public Formula term(final Collection literals) {
+ final LinkedHashSet ops = new LinkedHashSet<>(literals);
+ return this.constructTerm(ops);
+ }
+
+ /**
+ * Creates a new term.
+ * @param literalsIn the literals
+ * @return a new term
+ */
+ private Formula constructTerm(final LinkedHashSet literalsIn) {
+ final LinkedHashSet literals = importOrPanic(literalsIn);
+ if (literals.isEmpty()) {
+ return this.verum();
+ }
+ if (literals.size() == 1) {
+ return literals.iterator().next();
+ }
+ Map, And> opAndMap = this.andsN;
+ switch (literals.size()) {
+ case 2:
+ opAndMap = this.ands2;
+ break;
+ case 3:
+ opAndMap = this.ands3;
+ break;
+ case 4:
+ opAndMap = this.ands4;
+ break;
+ default:
+ break;
+ }
+ And tempAnd = opAndMap.get(literals);
+ if (tempAnd != null) {
+ return tempAnd;
+ }
+ tempAnd = new And(literals, this);
+ setCnfCaches(tempAnd, true);
+ opAndMap.put(literals, tempAnd);
+ return tempAnd;
+ }
+
private void setCnfCaches(final Formula formula, final boolean isCNF) {
if (isCNF) {
setPredicateCacheEntry(formula, IS_CNF, true);
@@ -1258,16 +1396,6 @@ public long numberOfNodes(final Formula formula) {
return formula.apply(this.subformulaFunction).size();
}
- /**
- * Parses a given string to a formula using a pseudo boolean parser.
- * @param string a string representing the formula
- * @return the formula
- * @throws ParserException if the parser throws an exception
- */
- public Formula parse(final String string) throws ParserException {
- return this.parser.parse(string);
- }
-
/**
* Adds a given formula to a list of operands. If the formula is the neutral element for the respective n-ary
* operation it will be skipped. If a complementary formula is already present in the list of operands or the
diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java b/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java
index df387198..ec114090 100644
--- a/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java
+++ b/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java
@@ -439,22 +439,24 @@ public List getVariableOrder() {
* BDDs, the variables are swapped in all of these BDDs.
* @param first the first variable to swap
* @param second the second variable to swap
+ * @deprecated dangerous API, will be removed in version 3.0, use {@link BDDKernel#swapVariables} instead
*/
+ @Deprecated
public void swapVariables(final Variable first, final Variable second) {
- final int firstVar = this.kernel.getIndexForVariable(first);
- final int secondVar = this.kernel.getIndexForVariable(second);
- if (firstVar < 0) {
- throw new IllegalArgumentException("Unknown variable: " + first);
- } else if (secondVar < 0) {
- throw new IllegalArgumentException("Unknown variable: " + second);
- }
- this.kernel.getReordering().swapVariables(firstVar, secondVar);
+ this.kernel.swapVariables(first, second);
}
/**
* Returns the reordering object for the BDD kernel.
* @return the reordering object
- */
+ * @deprecated the relevant methods should now be access via the {@link #underlyingKernel() kernel}:
+ *
+ * - Add a variable block: {@link BDDKernel#addVariableBlock}
+ * - Add blocks for all variables: {@link BDDKernel#addAllVariablesAsBlock}
+ * - Instant reordering: {@link BDDKernel#reorder}
+ *
+ */
+ @Deprecated
public BDDReordering getReordering() {
return this.kernel.getReordering();
}
diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java
index d036fb76..c6eb639a 100644
--- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java
+++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java
@@ -152,7 +152,7 @@ public BDDKernel(final FormulaFactory f, final int numVars, final int nodeSize,
this.var2idx = new TreeMap<>();
this.idx2var = new TreeMap<>();
this.reordering = new BDDReordering(this);
- this.nodesize = prime.primeGTE(Math.max(nodeSize, 3));
+ this.nodesize = this.prime.primeGTE(Math.max(nodeSize, 3));
this.nodes = new int[this.nodesize * 6];
this.minfreenodes = 20;
for (int n = 0; n < this.nodesize; n++) {
@@ -261,7 +261,16 @@ public FormulaFactory factory() {
/**
* Returns the reordering object for this kernel.
* @return the reordering object
+ * @deprecated the relevant methods of this object are now exposed directly
+ * on this kernel:
+ *
+ * - Reordering during BDD construction: {@link #activateReorderDuringConstruction}
+ * - Instant reordering: {@link #reorder}
+ * - Add a variable block: {@link #addVariableBlock}
+ * - Add blocks for all variables: {@link #addAllVariablesAsBlock}
+ *
*/
+ @Deprecated
public BDDReordering getReordering() {
return this.reordering;
}
@@ -319,6 +328,148 @@ public int[] getCurrentVarOrder() {
return Arrays.copyOf(this.level2var, this.level2var.length - 1); // last var is always 0
}
+ /**
+ * Swaps the variables {@code v1} and {@code v2}. This affects all BDDs
+ * created by this kernel.
+ * @param v1 the first variable to swap
+ * @param v2 the second variable to swap
+ */
+ public void swapVariables(final int v1, final int v2) {
+ this.reordering.swapVariables(v1, v2);
+ }
+
+ /**
+ * Swaps the variables {@code v1} and {@code v2}. This affects all BDDs
+ * created by this kernel.
+ * @param v1 the first variable to swap
+ * @param v2 the second variable to swap
+ */
+ public void swapVariables(final Variable v1, final Variable v2) {
+ swapVariables(getIndexForVariable(v1), getIndexForVariable(v2));
+ }
+
+ /**
+ * Activates or deactivates the automatic reordering during the construction of a BDD.
+ *
+ * Automatic reordering can be deactivated by passing {@link BDDReorderingMethod#BDD_REORDER_NONE}
+ * for the {@code method} parameter, otherwise the reordering is activated with the
+ * given method. The reordering is executed at most {@code num} times.
+ * @param method the method to be used for reordering
+ * @param num the maximum number of reorders to be performed
+ */
+ public void activateReorderDuringConstruction(final BDDReorderingMethod method, final int num) {
+ this.reordering.activateReorderDuringConstruction(method, num);
+ }
+
+ /**
+ * Adds a variable block starting at variable {@code first} and ending in variable
+ * {@code last} (both inclusive).
+ *
+ * Variable blocks are used in the {@link #reorder BDD reordering}
+ * or in the automatic reordering during the construction of the BDD (configured by
+ * {@link #activateReorderDuringConstruction}). Variable blocks can be nested, i.e. one block can
+ * contain an arbitrary number of ("child") blocks. Furthermore, a variable block can also
+ * be a single variable.
+ *
+ * During reordering, the child blocks of a parent block can be reordered, but they are kept
+ * together. So no other block can be moved in between the child blocks. Furthermore,
+ * variables in a block which are not in a child block will be left untouched.
+ *
+ * Example: Lets assume we have a BDD with the variable ordering {@code v1, v2, v3, v4, v5, v6, v7}.
+ * We create the following blocks:
+ *
+ * - {@code A} reaching from {@code v1} to {@code v5}
+ * - {@code B} reaching from {@code v6} to {@code v7}
+ * - {@code A1} reaching from {@code v1} to {@code v2}
+ * - {@code A2} reaching from {@code v3} to {@code v3}
+ * - {@code A3} reaching from {@code v4} to {@code v5}
+ *
+ * This means that the variables of {@code A} and {@code B} can never be mixed up in the order.
+ * So during reordering the variables {@code v6} and {@code v7} can either be moved to the
+ * front (before {@code A}) or remain at their position.
+ * Furthermore, for example {@code v1} and {@code v2} will always stay together and neither
+ * {@code v3} nor any other variable can be moved in between them. On the other hand, the blocks
+ * {@code A1}, {@code A2}, and {@code A3} can be swapped arbitrarily.
+ *
+ * These are valid result of a reordering based on the above blocks:
+ *
+ * - {@code v3, v1, v2, v4, v5, v6, v7}
+ * - {@code v6, v7, v4, v5, v3, v1, v2}
+ * - {@code v6, v7, v1, v2, v3, v4, v5}
+ *
+ * These however would be illegal:
+ *
+ * - {@code v2, v1, v3, v4, v5, v6, v7} (variables in a block which are not in a child block will not be reordered)
+ * - {@code v1, v3, v2, v4, v5, v6, v7} (variables of different block will not be mixed up)
+ *
+ *
+ * If a block is fixed (the example above assumed always blocks which are not fixed), its
+ * immediate child blocks will remain in their order. E.g. if block {@code A} was fixed, the blocks
+ * {@code A1}, {@code A2}, and {@code A3} would not be allowed to be swapped.
+ * Let's assume block {@code A} to be fixed and that we have two other unfixed blocks:
+ *
+ * - {@code A11} reaching from {@code v1} to {@code v1}
+ * - {@code A12} reaching from {@code v2} to {@code v2}
+ *
+ * These are examples for legal reorderings:
+ *
+ * - {@code v2, v1, v3, v4, v5, v6, v7} (block {@code A} is fixed, but "grandchildren" are still allowed to be reordered
+ * - {@code v6, v7, v2, v1, v3, v4, v5}
+ *
+ * These are examples for illegal reorderings:
+ *
+ * - {@code v3, v2, v1, v4, v5, v6, v7} (block {@code A} is fixed, so it's child blocks must be be reordered
+ * - {@code v1, v2, v4, v5, v3, v6, v7}
+ *
+ *
+ * Each block (including all nested blocks) must be defined by a separate call to this method. The blocks
+ * may be added in an arbitrary order, so it is not required to add them top-down or bottom-up.
+ * However, the blocks must not intersect, except of one block containing the other. Furthermore,
+ * both the {@code first} and the {@code last} variable must be known by the kernel and the level {@code first}
+ * must be lower than the level of {@code last}.
+ * @param first the variable at which the block starts (inclusive)
+ * @param last the variable at which the block ends (inclusive)
+ * @param fixed whether the block should be fixed or not
+ */
+ public void addVariableBlock(final int first, final int last, final boolean fixed) {
+ this.reordering.addVariableBlock(first, last, fixed);
+ }
+
+ /**
+ * Adds a variable block starting at variable {@code first} and ending in variable
+ * {@code last} (both inclusive).
+ *
+ * See {@link #addVariableBlock(int, int, boolean)} for details.
+ * @param first the variable at which the block starts (inclusive)
+ * @param last the variable at which the block ends (inclusive)
+ * @param fixed whether the block should be fixed or not
+ * @see #addVariableBlock(int, int, boolean)
+ */
+ public void addVariableBlock(final Variable first, final Variable last, final boolean fixed) {
+ addVariableBlock(getIndexForVariable(first), getIndexForVariable(last), fixed);
+ }
+
+ /**
+ * Adds a single variable block for all variables known by the kernel.
+ */
+ public void addAllVariablesAsBlock() {
+ this.reordering.addAllVariablesAsBlock();
+ }
+
+ /**
+ * Reorders the levels in the kernel using the given reordering method.
+ * Only blocks of variables will be reordered. See the documentation of
+ * {@link #addVariableBlock} to learn more about such variable blocks.
+ * Without the definition of any block, nothing will be reordered.
+ *
+ * If the reordering should be performed without any restrictions,
+ * {@link #addAllVariablesAsBlock()} can be called before this method.
+ * @param method the method to be used for the reordering
+ */
+ public void reorder(final BDDReorderingMethod method) {
+ this.reordering.reorder(method);
+ }
+
protected int doWithPotentialReordering(final BddOperation operation) {
try {
initRef();
@@ -601,7 +752,7 @@ protected void nodeResize(final boolean doRehash) {
if (this.nodesize > oldsize + this.maxnodeincrease) {
this.nodesize = oldsize + this.maxnodeincrease;
}
- this.nodesize = prime.primeLTE(this.nodesize);
+ this.nodesize = this.prime.primeLTE(this.nodesize);
final int[] newnodes = new int[this.nodesize * 6];
System.arraycopy(this.nodes, 0, newnodes, 0, this.nodes.length);
this.nodes = newnodes;
@@ -862,6 +1013,6 @@ protected interface BddOperation {
}
public BDDPrime getPrime() {
- return prime;
+ return this.prime;
}
}
diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java
index 5f0705b8..691f65d0 100644
--- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java
+++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java
@@ -484,7 +484,7 @@ protected Formula toFormulaRec(final int r, final boolean followPathsToTrue) {
if (this.k.isZero(r)) {
return f.constant(!followPathsToTrue);
}
- final Variable var = this.k.idx2var.get(this.k.level(r));
+ final Variable var = this.k.getVariableForIndex(this.k.level2var[this.k.level(r)]);
final int low = this.k.low(r);
final Formula lowFormula = isRelevant(low, followPathsToTrue)
? f.and(var.negate(), toFormulaRec(low, followPathsToTrue))
diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java
index 58fff4f5..9b39324e 100644
--- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java
+++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java
@@ -47,11 +47,11 @@
*
* - Swapping two variables in the kernel can be performed via {@link #swapVariables}
* - Reordering all variables can be performed via {@link #reorder}
- * - Reordering during construction of the BDD can be configured via {@link #setReorderDuringConstruction}
+ * - Reordering during construction of the BDD can be configured via {@link #activateReorderDuringConstruction}
*
* The last two operations only have an effect, if variable blocks were added. {@link #addVariableBlock(int, int, boolean) The docuentation}
* gives more information on variable blocks.
- * To make all variables freely movable, {@link #addVariableBlockAll()} can be used.
+ * To make all variables freely movable, {@link #addAllVariablesAsBlock()} can be used.
* @version 2.0.0
* @since 2.0.0
*/
@@ -101,7 +101,7 @@ protected void init() {
this.reorderDisabled = false;
this.varTree = null;
clrVarBlocks();
- setReorderDuringConstruction(BDDReorderingMethod.BDD_REORDER_NONE, 0);
+ activateReorderDuringConstruction(BDDReorderingMethod.BDD_REORDER_NONE, 0);
this.usednumBefore = this.usednumAfter = 0;
this.blockId = 0;
}
@@ -165,7 +165,7 @@ public void swapVariables(int v1, int v2) {
* Without the definition of any block, nothing will be reordered.
*
* If the reordering should be performed without any restrictions,
- * {@link #addVariableBlockAll()} can be called before this method.
+ * {@link #addAllVariablesAsBlock()} can be called before this method.
* @param method the method to be used for the reordering
*/
public void reorder(final BDDReorderingMethod method) {
@@ -201,8 +201,23 @@ public void reorder(final BDDReorderingMethod method) {
* given method. The reordering is executed at most {@code num} times.
* @param method the method to be used for reordering
* @param num the maximum number of reorders to be performed
+ * @deprecated use {@link BDDKernel#activateReorderDuringConstruction} instead
*/
+ @Deprecated
public void setReorderDuringConstruction(final BDDReorderingMethod method, final int num) {
+ activateReorderDuringConstruction(method, num);
+ }
+
+ /**
+ * Activates or deactivates the automatic reordering during the construction of a BDD.
+ *
+ * Automatic reordering can be deactivated by passing {@link BDDReorderingMethod#BDD_REORDER_NONE}
+ * for the {@code method} parameter, otherwise the reordering is activated with the
+ * given method. The reordering is executed at most {@code num} times.
+ * @param method the method to be used for reordering
+ * @param num the maximum number of reorders to be performed
+ */
+ protected void activateReorderDuringConstruction(final BDDReorderingMethod method, final int num) {
this.reorderMethod = method;
this.bddreorderTimes = num;
}
@@ -213,7 +228,7 @@ public void setReorderDuringConstruction(final BDDReorderingMethod method, final
*
* Variable blocks are used in the {@link #reorder BDD reordering}
* or in the automatic reordering during the construction of the BDD (configured by
- * {@link #setReorderDuringConstruction}). Variable blocks can be nested, i.e. one block can
+ * {@link #activateReorderDuringConstruction}). Variable blocks can be nested, i.e. one block can
* contain an arbitrary number of ("child") blocks. Furthermore, a variable block can also
* be a single variable.
*
@@ -292,12 +307,21 @@ public void addVariableBlock(final int first, final int last, final boolean fixe
/**
* Adds a single variable block for all variables known by the kernel.
*/
- public void addVariableBlockAll() {
+ public void addAllVariablesAsBlock() {
for (int n = 0; n < this.k.varnum; n++) {
addVariableBlock(n, n, false);
}
}
+ /**
+ * Adds a single variable block for all variables known by the kernel.
+ * @deprecated use {@link #addAllVariablesAsBlock()} instead
+ */
+ @Deprecated
+ public void addVariableBlockAll() {
+ addAllVariablesAsBlock();
+ }
+
/**
* IMPORTANT:
* The semantics of the "level" field in the BddNode struct changes during
diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfCompiler.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfCompiler.java
index 493d293a..d8efb8a1 100644
--- a/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfCompiler.java
+++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfCompiler.java
@@ -108,7 +108,7 @@ public Formula compile(final DTreeGenerator generator) {
* Performs the compilation using the given DTree generator and the compilation handler.
* @param generator the DTree generator
* @param handler the compilation handler
- * @return the compiled DNNF
+ * @return the compiled DNNF or {@code null} if the compilation was aborted by the handler
*/
public Formula compile(final DTreeGenerator generator, final DnnfCompilationHandler handler) {
if (!this.cnf.holds(new SATPredicate(this.f))) {
diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java
index b695045a..9de374ca 100644
--- a/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java
+++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java
@@ -30,6 +30,7 @@
import org.logicng.formulas.Formula;
import org.logicng.formulas.Variable;
+import org.logicng.handlers.DnnfCompilationHandler;
import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf;
import org.logicng.knowledgecompilation.dnnf.datastructures.dtree.MinFillDTreeGenerator;
import org.logicng.transformations.cnf.CNFSubsumption;
@@ -57,18 +58,28 @@ public DnnfFactory() {
}
/**
- * Compiles the given formula to a DNNF instance.
+ * Compiles the given formula to a DNNF instance using the given handler.
* @param formula the formula
- * @return the compiled DNNF
+ * @param handler the DNNF handler
+ * @return the compiled DNNF or {@code null} if the computation was aborted by the handler
*/
- public Dnnf compile(final Formula formula) {
+ public Dnnf compile(final Formula formula, final DnnfCompilationHandler handler) {
final SortedSet originalVariables = new TreeSet<>(formula.variables());
final Formula cnf = formula.cnf();
originalVariables.addAll(cnf.variables());
final Formula simplifedFormula = simplifyFormula(cnf);
final DnnfCompiler compiler = new DnnfCompiler(simplifedFormula);
- final Formula dnnf = compiler.compile(new MinFillDTreeGenerator());
- return new Dnnf(originalVariables, dnnf);
+ final Formula dnnf = compiler.compile(new MinFillDTreeGenerator(), handler);
+ return dnnf == null ? null : new Dnnf(originalVariables, dnnf);
+ }
+
+ /**
+ * Compiles the given formula to a DNNF instance.
+ * @param formula the formula
+ * @return the compiled DNNF
+ */
+ public Dnnf compile(final Formula formula) {
+ return compile(formula, null);
}
protected Formula simplifyFormula(final Formula formula) {
diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java
index 9b0f0e0a..1b2f964b 100644
--- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java
+++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java
@@ -37,8 +37,8 @@
/**
* A DNNF - Decomposable Negation Normal Form.
- * @version 2.0.0
- * @since 2.5.0
+ * @version 2.5.0
+ * @since 2.0.0
*/
public final class Dnnf {
diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java
index 0aa2e70c..626fa77f 100644
--- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java
+++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java
@@ -36,8 +36,10 @@
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
+import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
+import java.util.Set;
import java.util.SortedSet;
/**
@@ -73,7 +75,7 @@ public static class Graph {
/**
* The edges of the graph as a list of edges per node ({{2,3},{1},{1}} means that there are the edges 1-2 and 1-3)
*/
- protected final List edgeList;
+ protected final List> edgeList;
/**
* Computes the DTree from the given CNF.
@@ -94,7 +96,7 @@ public Graph(final Formula cnf) {
this.adjMatrix = new boolean[this.numberOfVertices][this.numberOfVertices];
this.edgeList = new ArrayList<>(this.numberOfVertices);
for (int i = 0; i < this.numberOfVertices; i++) {
- this.edgeList.add(new LNGIntVector());
+ this.edgeList.add(new LinkedHashSet<>());
}
for (final Formula clause : cnf) {
@@ -106,8 +108,8 @@ public Graph(final Formula cnf) {
}
for (int i = 0; i < varNums.length; i++) {
for (int j = i + 1; j < varNums.length; j++) {
- this.edgeList.get(varNums[i]).push(varNums[j]);
- this.edgeList.get(varNums[j]).push(varNums[i]);
+ this.edgeList.get(varNums[i]).add(varNums[j]);
+ this.edgeList.get(varNums[j]).add(varNums[i]);
this.adjMatrix[varNums[i]][varNums[j]] = true;
this.adjMatrix[varNums[j]][varNums[i]] = true;
}
@@ -117,8 +119,8 @@ public Graph(final Formula cnf) {
protected List getCopyOfEdgeList() {
final List result = new ArrayList<>();
- for (final LNGIntVector edge : this.edgeList) {
- result.add(new LNGIntVector(edge));
+ for (final Set edge : this.edgeList) {
+ result.add(new LNGIntVector(edge.stream().mapToInt(i -> i).toArray()));
}
return result;
}
@@ -196,7 +198,7 @@ protected List getMinFillOrdering() {
int currentNumberOfEdges = 0;
for (int k = 0; k < this.numberOfVertices; k++) {
- if (fillAdjMatrix[bestVertex][k] && !processed[k]) {
+ if (k != bestVertex && !processed[k] && fillAdjMatrix[bestVertex][k]) {
currentNumberOfEdges++;
}
}
diff --git a/src/main/java/org/logicng/modelcounting/ModelCounter.java b/src/main/java/org/logicng/modelcounting/ModelCounter.java
index 0dccda96..e6561a49 100644
--- a/src/main/java/org/logicng/modelcounting/ModelCounter.java
+++ b/src/main/java/org/logicng/modelcounting/ModelCounter.java
@@ -28,6 +28,8 @@
package org.logicng.modelcounting;
+import static org.logicng.handlers.Handler.aborted;
+
import org.logicng.datastructures.Assignment;
import org.logicng.formulas.FType;
import org.logicng.formulas.Formula;
@@ -38,6 +40,7 @@
import org.logicng.graphs.datastructures.Graph;
import org.logicng.graphs.datastructures.Node;
import org.logicng.graphs.generators.ConstraintGraphGenerator;
+import org.logicng.handlers.DnnfCompilationHandler;
import org.logicng.knowledgecompilation.dnnf.DnnfFactory;
import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf;
import org.logicng.knowledgecompilation.dnnf.functions.DnnfModelCountFunction;
@@ -53,6 +56,7 @@
import java.util.Set;
import java.util.SortedSet;
import java.util.TreeSet;
+import java.util.function.Supplier;
import java.util.stream.Collectors;
/**
@@ -78,6 +82,22 @@ private ModelCounter() {
* @return the model count of the formulas for the variables
*/
public static BigInteger count(final Collection formulas, final SortedSet variables) {
+ return count(formulas, variables, () -> null);
+ }
+
+ /**
+ * Computes the model count for a given set of formulas (interpreted as conjunction)
+ * and a set of relevant variables. This set can only be a superset of the original
+ * formulas' variables. No projected model counting is supported.
+ * @param formulas the list of formulas
+ * @param variables the relevant variables
+ * @param dnnfHandlerSupplier a supplier for a DNNF handler, it may return a new handler on each call or always the same.
+ * Since multiple DNNFs may be computed, the supplier may be called several times. It must not
+ * be {@code null}, but it may return {@code null} (i.e. return no handler).
+ * @return the model count of the formulas for the variables or {@code null} if the DNNF handler aborted the DNNF computation
+ */
+ public static BigInteger count(final Collection formulas, final SortedSet variables,
+ final Supplier dnnfHandlerSupplier) {
if (!variables.containsAll(FormulaHelper.variables(formulas))) {
throw new IllegalArgumentException("Expected variables to contain all of the formulas' variables.");
}
@@ -88,7 +108,10 @@ public static BigInteger count(final Collection formulas, final SortedS
final FormulaFactory f = variables.first().factory();
final List cnfs = encodeAsCnf(formulas, f);
final SimplificationResult simplification = simplify(cnfs);
- final BigInteger count = count(simplification.simplifiedFormulas, f);
+ final BigInteger count = count(simplification.simplifiedFormulas, dnnfHandlerSupplier, f);
+ if (count == null) {
+ return null;
+ }
final SortedSet dontCareVariables = simplification.getDontCareVariables(variables);
return count.multiply(BigInteger.valueOf(2).pow(dontCareVariables.size()));
}
@@ -122,14 +145,18 @@ private static SimplificationResult simplify(final Collection formulas)
return new SimplificationResult(simplified, backboneVariables);
}
- private static BigInteger count(final Collection formulas, final FormulaFactory f) {
+ private static BigInteger count(final Collection formulas, final Supplier dnnfHandlerSupplier, final FormulaFactory f) {
final Graph constraintGraph = ConstraintGraphGenerator.generateFromFormulas(formulas);
final Set>> ccs = ConnectedComponentsComputation.compute(constraintGraph);
final List> components = ConnectedComponentsComputation.splitFormulasByComponent(formulas, ccs);
final DnnfFactory factory = new DnnfFactory();
BigInteger count = BigInteger.ONE;
for (final List component : components) {
- final Dnnf dnnf = factory.compile(f.and(component));
+ final DnnfCompilationHandler handler = dnnfHandlerSupplier.get();
+ final Dnnf dnnf = factory.compile(f.and(component), handler);
+ if (dnnf == null || aborted(handler)) {
+ return null;
+ }
count = count.multiply(dnnf.execute(DnnfModelCountFunction.get()));
}
return count;
diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java
index a3e433af..4eab4d82 100644
--- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java
+++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java
@@ -39,10 +39,14 @@
import org.logicng.formulas.Literal;
import org.logicng.formulas.Variable;
import org.logicng.handlers.OptimizationHandler;
+import org.logicng.handlers.SATHandler;
+import org.logicng.solvers.MaxSATSolver;
import org.logicng.solvers.MiniSat;
import org.logicng.solvers.SATSolver;
import org.logicng.solvers.functions.OptimizationFunction;
-import org.logicng.solvers.sat.MiniSatConfig;
+import org.logicng.solvers.maxsat.OptimizationConfig;
+import org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType;
+import org.logicng.solvers.maxsat.algorithms.MaxSAT;
import org.logicng.transformations.LiteralSubstitution;
import org.logicng.util.FormulaHelper;
import org.logicng.util.Pair;
@@ -69,7 +73,7 @@
* {@link #getWithMaximization()} and another which searches for minimum models
* {@link #getWithMaximization()}. From experience, the one with minimum models usually
* outperforms the one with maximum models.
- * @version 2.1.0
+ * @version 2.6.0
* @since 2.0.0
*/
public final class PrimeCompiler {
@@ -110,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, null);
+ return compute(formula, type, OptimizationConfig.sat(null));
}
/**
@@ -127,12 +131,41 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType
* @param handler an optimization handler, can be {@code null}
* @return the prime result or null if the computation was aborted by the handler
*/
- public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type, final OptimizationHandler handler) {
- start(handler);
+ public PrimeResult compute(
+ final Formula formula,
+ final PrimeResult.CoverageType type,
+ final OptimizationHandler handler) {
+ return compute(formula, type, OptimizationConfig.sat(handler));
+ }
+
+ /**
+ * Computes prime implicants and prime implicates for a given formula.
+ * The coverage type specifies if the implicants or the implicates will
+ * be complete, the other one will still be a cover of the given formula.
+ *
+ * The prime compiler 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 formula the formula
+ * @param type the coverage type
+ * @param cfg the optimization configuration
+ * @return the prime result or null if the computation was aborted by the handler
+ */
+ public PrimeResult compute(
+ final Formula formula,
+ final PrimeResult.CoverageType type,
+ final OptimizationConfig cfg) {
+
final boolean completeImplicants = type == PrimeResult.CoverageType.IMPLICANTS_COMPLETE;
final Formula formulaForComputation = completeImplicants ? formula : formula.negate();
- final Pair>, List>> result = computeGeneric(formulaForComputation, handler);
- if (result == null || aborted(handler)) {
+ final Pair>, List>> result;
+ if (cfg.getOptimizationType() == OptimizationType.SAT_OPTIMIZATION) {
+ result = computeSAT(formulaForComputation, cfg.getOptimizationHandler());
+ } else {
+ result = computeMaxSAT(formulaForComputation, cfg);
+ }
+ if (result == null) {
return null;
}
return new PrimeResult(
@@ -141,12 +174,15 @@ public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType
type);
}
- private Pair>, List>> computeGeneric(final Formula formula, final OptimizationHandler handler) {
+ private Pair>, List>> computeSAT(
+ final Formula formula,
+ final OptimizationHandler handler) {
+ start(handler);
final FormulaFactory f = formula.factory();
final SubstitutionResult sub = createSubstitution(formula);
- final SATSolver hSolver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
+ final SATSolver hSolver = MiniSat.miniSat(f);
hSolver.add(sub.constraintFormula);
- final SATSolver fSolver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
+ final SATSolver fSolver = MiniSat.miniSat(f);
fSolver.add(formula.negate());
final NaivePrimeReduction primeReduction = new NaivePrimeReduction(formula);
final List> primeImplicants = new ArrayList<>();
@@ -167,7 +203,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;
}
@@ -192,6 +230,66 @@ private Pair>, List>> computeGeneric(
}
}
+ private Pair>, List>> computeMaxSAT(
+ final Formula formula,
+ final OptimizationConfig cfg) {
+ start(cfg.getMaxSATHandler());
+ final SATHandler handler = cfg.getMaxSATHandler() == null ? null : cfg.getMaxSATHandler().satHandler();
+ final FormulaFactory f = formula.factory();
+ final SubstitutionResult sub = createSubstitution(formula);
+ final List hSolverConstraints = new ArrayList<>();
+ hSolverConstraints.add(sub.constraintFormula);
+ final SATSolver fSolver = MiniSat.miniSat(f);
+ fSolver.add(formula.negate());
+ final NaivePrimeReduction primeReduction = new NaivePrimeReduction(formula);
+ final List> primeImplicants = new ArrayList<>();
+ final List> primeImplicates = new ArrayList<>();
+ while (true) {
+ final MaxSATSolver hSolver = cfg.genMaxSATSolver(f);
+ hSolverConstraints.forEach(hSolver::addHardFormula);
+ 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 || aborted(cfg.getMaxSATHandler())) {
+ return null;
+ }
+ final Assignment hModel = hSolver.model();
+ if (hModel == null) {
+ return new Pair<>(primeImplicants, primeImplicates);
+ }
+ final Assignment fModel = transformModel(hModel, sub.newVar2oldLit);
+ final Tristate fSat = fSolver.sat(handler, fModel.literals());
+ if (aborted(handler)) {
+ return null;
+ }
+ if (fSat == Tristate.FALSE) {
+ final SortedSet primeImplicant = this.computeWithMaximization
+ ? primeReduction.reduceImplicant(fModel.literals(), handler)
+ : fModel.literals();
+ if (primeImplicant == null || aborted(handler)) {
+ return null;
+ }
+ primeImplicants.add(primeImplicant);
+ final List blockingClause = new ArrayList<>();
+ for (final Literal lit : primeImplicant) {
+ blockingClause.add(((Literal) lit.transform(sub.substitution)).negate());
+ }
+ hSolverConstraints.add(f.or(blockingClause));
+ } else {
+ final SortedSet implicate = new TreeSet<>();
+ for (final Literal lit : (this.computeWithMaximization ? fModel : fSolver.model(formula.variables())).literals()) {
+ implicate.add(lit.negate());
+ }
+ final SortedSet primeImplicate = primeReduction.reduceImplicate(implicate, handler);
+ if (primeImplicate == null || aborted(handler)) {
+ return null;
+ }
+ primeImplicates.add(primeImplicate);
+ hSolverConstraints.add(f.or(primeImplicate).transform(sub.substitution));
+ }
+ }
+ }
+
private SubstitutionResult createSubstitution(final Formula formula) {
final Map newVar2oldLit = new HashMap<>();
final LiteralSubstitution substitution = new LiteralSubstitution();
diff --git a/src/main/java/org/logicng/solvers/MiniSat.java b/src/main/java/org/logicng/solvers/MiniSat.java
index 5b4e8f00..112a2862 100644
--- a/src/main/java/org/logicng/solvers/MiniSat.java
+++ b/src/main/java/org/logicng/solvers/MiniSat.java
@@ -75,10 +75,10 @@ public class MiniSat extends SATSolver {
public enum SolverStyle {MINISAT, GLUCOSE, MINICARD}
protected final MiniSatConfig config;
- protected final MiniSatStyleSolver solver;
- protected final CCEncoder ccEncoder;
- protected final SolverStyle style;
- protected final LNGIntVector validStates;
+ protected MiniSatStyleSolver solver;
+ protected CCEncoder ccEncoder;
+ protected SolverStyle style;
+ protected LNGIntVector validStates;
protected final boolean initialPhase;
protected final boolean incremental;
protected int nextStateId;
@@ -122,6 +122,36 @@ protected MiniSat(final FormulaFactory f, final SolverStyle solverStyle, final M
this.fullPgTransformation = new PlaistedGreenbaumTransformationSolver(false, this.underlyingSolver(), this.initialPhase);
}
+ /**
+ * Constructs a new MiniSat solver with a given underlying solver core. This
+ * method is primarily used for serialization purposes and should not be
+ * required in any other application use case.
+ * @param f the formula factory
+ * @param underlyingSolver the underlying solver core
+ */
+ public MiniSat(final FormulaFactory f, final MiniSatStyleSolver underlyingSolver) {
+ super(f);
+ this.config = underlyingSolver.getConfig();
+ if (underlyingSolver instanceof MiniSat2Solver) {
+ this.style = SolverStyle.MINISAT;
+ } else if (underlyingSolver instanceof MiniCard) {
+ this.style = SolverStyle.MINICARD;
+ } else if (underlyingSolver instanceof GlucoseSyrup) {
+ this.style = SolverStyle.GLUCOSE;
+ } else {
+ throw new IllegalArgumentException("Unknown solver type: " + underlyingSolver.getClass());
+ }
+ this.initialPhase = underlyingSolver.getConfig().initialPhase();
+ this.solver = underlyingSolver;
+ this.result = UNDEF;
+ this.incremental = underlyingSolver.getConfig().incremental();
+ this.validStates = new LNGIntVector();
+ this.nextStateId = 0;
+ this.ccEncoder = new CCEncoder(f);
+ this.pgTransformation = new PlaistedGreenbaumTransformationSolver(true, underlyingSolver, this.initialPhase);
+ this.fullPgTransformation = new PlaistedGreenbaumTransformationSolver(false, underlyingSolver, this.initialPhase);
+ }
+
/**
* Returns a new MiniSat solver with the MiniSat configuration from the formula factory.
* @param f the formula factory
diff --git a/src/main/java/org/logicng/solvers/SATSolver.java b/src/main/java/org/logicng/solvers/SATSolver.java
index 5cd7c6d4..d3cd4348 100644
--- a/src/main/java/org/logicng/solvers/SATSolver.java
+++ b/src/main/java/org/logicng/solvers/SATSolver.java
@@ -234,6 +234,12 @@ public Tristate sat() {
/**
* Returns {@code Tristate.TRUE} if the current formula in the solver and a given literal are satisfiable,
* {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
+ *
+ * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+ * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+ * For example, a subsequent model enumeration call will produce models containing the now known variables.
+ * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+ * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
* @param literal the assumed literal
* @return the satisfiability of the formula in the solver
*/
@@ -246,6 +252,12 @@ public Tristate sat(final Literal literal) {
* are satisfiable, {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
* The assumptions can be seen as an additional conjunction of literals.
* Note: Use ordered collections to ensure determinism in the solving process and thus in the resulting model or conflict.
+ *
+ * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+ * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+ * For example, a subsequent model enumeration call will produce models containing the now known variables.
+ * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+ * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
* @param assumptions a collection of literals
* @return the satisfiability of the formula in the solver
*/
@@ -256,6 +268,12 @@ public Tristate sat(final Collection assumptions) {
/**
* Returns {@code Tristate.TRUE} if the current formula in the solver and a given literal are satisfiable,
* {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
+ *
+ * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+ * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+ * For example, a subsequent model enumeration call will produce models containing the now known variables.
+ * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+ * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
* @param handler the SAT handler
* @param literal the assumed literal
* @return the satisfiability of the formula in the solver
@@ -267,6 +285,12 @@ public Tristate sat(final Collection assumptions) {
* are satisfiable, {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
* The assumptions can be seen as an additional conjunction of literals.
* Note: Use ordered collections to ensure determinism in the solving process and thus in the resulting model or conflict.
+ *
+ * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+ * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+ * For example, a subsequent model enumeration call will produce models containing the now known variables.
+ * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+ * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
* @param handler the SAT handler
* @param assumptions a collection of literals
* @return the satisfiability of the formula in the solver
diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java
index 80db3aee..83c2b343 100644
--- a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java
+++ b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java
@@ -104,6 +104,16 @@ public LNGBoundedIntQueue() {
this.queueSize = 0;
}
+ public LNGBoundedIntQueue(final LNGIntVector elems, final int first, final int last, final long sumOfQueue,
+ final int maxSize, final int queueSize) {
+ this.elems = elems;
+ this.first = first;
+ this.last = last;
+ this.sumOfQueue = sumOfQueue;
+ this.maxSize = maxSize;
+ this.queueSize = queueSize;
+ }
+
/**
* Initializes the size of this queue.
* @param size the size
@@ -154,6 +164,30 @@ private void growTo(final int size) {
this.last = 0;
}
+ public LNGIntVector getElems() {
+ return this.elems;
+ }
+
+ public int getFirst() {
+ return this.first;
+ }
+
+ public int getLast() {
+ return this.last;
+ }
+
+ public long getSumOfQueue() {
+ return this.sumOfQueue;
+ }
+
+ public int getMaxSize() {
+ return this.maxSize;
+ }
+
+ public int getQueueSize() {
+ return this.queueSize;
+ }
+
@Override
public String toString() {
return String.format("LNGBoundedIntQueue{first=%d, last=%d, sumOfQueue=%d, maxSize=%d, queueSize=%d, elems=%s}",
diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java
index b091d5ce..63a1199e 100644
--- a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java
+++ b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java
@@ -104,6 +104,16 @@ public LNGBoundedLongQueue() {
this.queueSize = 0;
}
+ public LNGBoundedLongQueue(final LNGLongVector elems, final int first, final int last, final long sumOfQueue,
+ final int maxSize, final int queueSize) {
+ this.elems = elems;
+ this.first = first;
+ this.last = last;
+ this.sumOfQueue = sumOfQueue;
+ this.maxSize = maxSize;
+ this.queueSize = queueSize;
+ }
+
/**
* Initializes the size of this queue.
* @param size the size
@@ -172,6 +182,30 @@ public void fastClear() {
this.sumOfQueue = 0;
}
+ public LNGLongVector getElems() {
+ return this.elems;
+ }
+
+ public int getFirst() {
+ return this.first;
+ }
+
+ public int getLast() {
+ return this.last;
+ }
+
+ public long getSumOfQueue() {
+ return this.sumOfQueue;
+ }
+
+ public int getMaxSize() {
+ return this.maxSize;
+ }
+
+ public int getQueueSize() {
+ return this.queueSize;
+ }
+
@Override
public String toString() {
return String.format("LNGBoundedLongQueue{first=%d, last=%d, sumOfQueue=%d, maxSize=%d, queueSize=%d, elems=%s}",
diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java b/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java
index 40074a3b..cfbb2a8a 100644
--- a/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java
+++ b/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java
@@ -69,6 +69,18 @@ public LNGHeap(final MiniSatStyleSolver solver) {
this.indices = new LNGIntVector(1000);
}
+ /**
+ * Constructs a new heap for a given solver and content.
+ * @param solver the solver
+ * @param heap the heap content
+ * @param indices the indices content
+ */
+ public LNGHeap(final MiniSatStyleSolver solver, final LNGIntVector heap, final LNGIntVector indices) {
+ this.s = solver;
+ this.heap = heap;
+ this.indices = indices;
+ }
+
/**
* Returns the left position on the heap for a given position.
* @param pos the position
@@ -252,6 +264,14 @@ private void percolateDown(final int pos) {
this.indices.set(y, p);
}
+ public LNGIntVector getHeap() {
+ return this.heap;
+ }
+
+ public LNGIntVector getIndices() {
+ return this.indices;
+ }
+
@Override
public String toString() {
final StringBuilder sb = new StringBuilder("LNGHeap{");
diff --git a/src/main/java/org/logicng/solvers/datastructures/MSClause.java b/src/main/java/org/logicng/solvers/datastructures/MSClause.java
index 1f0d71f3..acc4c633 100644
--- a/src/main/java/org/logicng/solvers/datastructures/MSClause.java
+++ b/src/main/java/org/logicng/solvers/datastructures/MSClause.java
@@ -123,6 +123,21 @@ public MSClause(final LNGIntVector ps, final boolean learnt, final boolean isAtM
this.atMostWatchers = -1;
}
+ public MSClause(final LNGIntVector data, final boolean learnt, final boolean isAtMost, final double activity,
+ final int szWithoutSelectors, final boolean seen, final long lbd, final boolean canBeDel,
+ final boolean oneWatched, final int atMostWatchers) {
+ this.data = data;
+ this.learnt = learnt;
+ this.isAtMost = isAtMost;
+ this.activity = activity;
+ this.szWithoutSelectors = szWithoutSelectors;
+ this.seen = seen;
+ this.lbd = lbd;
+ this.canBeDel = canBeDel;
+ this.oneWatched = oneWatched;
+ this.atMostWatchers = atMostWatchers;
+ }
+
/**
* Returns the size (number of literals) of this clause.
* @return the size
@@ -301,6 +316,10 @@ public int cardinality() {
return this.data.size() - this.atMostWatchers + 1;
}
+ public LNGIntVector getData() {
+ return this.data;
+ }
+
@Override
public int hashCode() {
return this.data.hashCode();
diff --git a/src/main/java/org/logicng/solvers/datastructures/MSVariable.java b/src/main/java/org/logicng/solvers/datastructures/MSVariable.java
index 926d8011..249290b9 100644
--- a/src/main/java/org/logicng/solvers/datastructures/MSVariable.java
+++ b/src/main/java/org/logicng/solvers/datastructures/MSVariable.java
@@ -74,6 +74,16 @@ public MSVariable(final boolean polarity) {
this.decision = false;
}
+ public MSVariable(final Tristate assignment, final int level, final MSClause reason, final double activity,
+ final boolean polarity, final boolean decision) {
+ this.assignment = assignment;
+ this.level = level;
+ this.reason = reason;
+ this.activity = activity;
+ this.polarity = polarity;
+ this.decision = decision;
+ }
+
/**
* Sets the decision level of this variable.
* @param level the decision level
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..5627acb5
--- /dev/null
+++ b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java
@@ -0,0 +1,205 @@
+package org.logicng.solvers.maxsat;
+
+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.
+ *
+ * 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.
+ *
+ * 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,
+ 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;
+
+ private 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;
+ }
+
+ /**
+ * 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);
+ }
+
+ /**
+ * Returns the optimization type.
+ * @return the optimization type
+ */
+ 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
+ */
+ 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:
+ 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);
+ }
+ }
+
+ /**
+ * Starts 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) {
+ 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/solvers/maxsat/algorithms/IncWBO.java b/src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java
index db3e9336..01bfa499 100644
--- a/src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java
+++ b/src/main/java/org/logicng/solvers/maxsat/algorithms/IncWBO.java
@@ -404,7 +404,6 @@ protected MaxSATResult weightSearch() {
}
protected int incComputeCostModel(final LNGBooleanVector currentModel) {
- assert currentModel.size() != 0;
int currentCost = 0;
for (int i = 0; i < nSoft(); i++) {
boolean unsatisfied = true;
@@ -413,7 +412,6 @@ protected int incComputeCostModel(final LNGBooleanVector currentModel) {
unsatisfied = false;
continue;
}
- assert var(this.softClauses.get(i).clause().get(j)) < currentModel.size();
if ((sign(this.softClauses.get(i).clause().get(j)) && !currentModel.get(var(this.softClauses.get(i).clause().get(j)))) ||
(!sign(this.softClauses.get(i).clause().get(j)) && currentModel.get(var(this.softClauses.get(i).clause().get(j))))) {
unsatisfied = false;
diff --git a/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java b/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java
index b0bc8fec..3104dce4 100644
--- a/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java
+++ b/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java
@@ -329,8 +329,6 @@ public MiniSatStyleSolver newSATSolver() {
* @param currentModel the model found by the solver
*/
public void saveModel(final LNGBooleanVector currentModel) {
- assert this.nbInitialVariables != 0;
- assert currentModel.size() != 0;
this.model.clear();
for (int i = 0; i < this.nbInitialVariables; i++) {
this.model.push(currentModel.get(i));
@@ -346,7 +344,6 @@ public void saveModel(final LNGBooleanVector currentModel) {
* @return the cost of the given model
*/
public int computeCostModel(final LNGBooleanVector currentModel, final int weight) {
- assert currentModel.size() != 0;
int currentCost = 0;
for (int i = 0; i < nSoft(); i++) {
boolean unsatisfied = true;
@@ -355,7 +352,6 @@ public int computeCostModel(final LNGBooleanVector currentModel, final int weigh
unsatisfied = false;
continue;
}
- assert var(this.softClauses.get(i).clause().get(j)) < currentModel.size();
if ((sign(this.softClauses.get(i).clause().get(j)) && !currentModel.get(var(this.softClauses.get(i).clause().get(j))))
|| (!sign(this.softClauses.get(i).clause().get(j)) && currentModel.get(var(this.softClauses.get(i).clause().get(j))))) {
unsatisfied = false;
diff --git a/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java b/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java
index 626f96a5..26b41ab1 100644
--- a/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java
+++ b/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java
@@ -81,6 +81,58 @@ public static Builder builder() {
return new Builder();
}
+ public int getLbLBDMinimizingClause() {
+ return this.lbLBDMinimizingClause;
+ }
+
+ public int getLbLBDFrozenClause() {
+ return this.lbLBDFrozenClause;
+ }
+
+ public int getLbSizeMinimizingClause() {
+ return this.lbSizeMinimizingClause;
+ }
+
+ public int getFirstReduceDB() {
+ return this.firstReduceDB;
+ }
+
+ public int getSpecialIncReduceDB() {
+ return this.specialIncReduceDB;
+ }
+
+ public int getIncReduceDB() {
+ return this.incReduceDB;
+ }
+
+ public double getFactorK() {
+ return this.factorK;
+ }
+
+ public double getFactorR() {
+ return this.factorR;
+ }
+
+ public int getSizeLBDQueue() {
+ return this.sizeLBDQueue;
+ }
+
+ public int getSizeTrailQueue() {
+ return this.sizeTrailQueue;
+ }
+
+ public boolean isReduceOnSize() {
+ return this.reduceOnSize;
+ }
+
+ public int getReduceOnSizeSize() {
+ return this.reduceOnSizeSize;
+ }
+
+ public double getMaxVarDecay() {
+ return this.maxVarDecay;
+ }
+
@Override
public String toString() {
final StringBuilder sb = new StringBuilder("GlucoseConfig{").append(System.lineSeparator());
diff --git a/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java b/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java
index 84276b6b..8ba2b44a 100644
--- a/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java
+++ b/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java
@@ -516,14 +516,14 @@ protected MSClause propagate() {
}
@Override
- protected boolean litRedundant(final int p, final int abstractLevels) {
- this.analyzeStack.clear();
- this.analyzeStack.push(p);
- final int top = this.analyzeToClear.size();
- while (this.analyzeStack.size() > 0) {
- assert v(this.analyzeStack.back()).reason() != null;
- final MSClause c = v(this.analyzeStack.back()).reason();
- this.analyzeStack.pop();
+ protected boolean litRedundant(final int p, final int abstractLevels, final LNGIntVector analyzeToClear) {
+ final LNGIntVector analyzeStack = new LNGIntVector();
+ analyzeStack.push(p);
+ final int top = analyzeToClear.size();
+ while (analyzeStack.size() > 0) {
+ assert v(analyzeStack.back()).reason() != null;
+ final MSClause c = v(analyzeStack.back()).reason();
+ analyzeStack.pop();
if (c.size() == 2 && value(c.get(0)) == Tristate.FALSE) {
assert value(c.get(1)) == Tristate.TRUE;
final int tmp = c.get(0);
@@ -535,13 +535,13 @@ protected boolean litRedundant(final int p, final int abstractLevels) {
if (!this.seen.get(var(q)) && v(q).level() > 0) {
if (v(q).reason() != null && (abstractLevel(var(q)) & abstractLevels) != 0) {
this.seen.set(var(q), true);
- this.analyzeStack.push(q);
- this.analyzeToClear.push(q);
+ analyzeStack.push(q);
+ analyzeToClear.push(q);
} else {
- for (int j = top; j < this.analyzeToClear.size(); j++) {
- this.seen.set(var(this.analyzeToClear.get(j)), false);
+ for (int j = top; j < analyzeToClear.size(); j++) {
+ this.seen.set(var(analyzeToClear.get(j)), false);
}
- this.analyzeToClear.removeElements(this.analyzeToClear.size() - top);
+ analyzeToClear.removeElements(analyzeToClear.size() - top);
return false;
}
}
@@ -985,14 +985,14 @@ protected void simplifyClause(final LNGIntVector outLearnt, final LNGIntVector s
for (i = 0; i < selectors.size(); i++) {
outLearnt.push(selectors.get(i));
}
- this.analyzeToClear = new LNGIntVector(outLearnt);
+ final LNGIntVector analyzeToClear = new LNGIntVector(outLearnt);
if (this.ccminMode == MiniSatConfig.ClauseMinimization.DEEP) {
int abstractLevel = 0;
for (i = 1; i < outLearnt.size(); i++) {
abstractLevel |= abstractLevel(var(outLearnt.get(i)));
}
for (i = j = 1; i < outLearnt.size(); i++) {
- if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel)) {
+ if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel, analyzeToClear)) {
outLearnt.set(j++, outLearnt.get(i));
}
}
@@ -1052,8 +1052,8 @@ protected void simplifyClause(final LNGIntVector outLearnt, final LNGIntVector s
}
this.lastDecisionLevel.clear();
}
- for (int m = 0; m < this.analyzeToClear.size(); m++) {
- this.seen.set(var(this.analyzeToClear.get(m)), false);
+ for (int m = 0; m < analyzeToClear.size(); m++) {
+ this.seen.set(var(analyzeToClear.get(m)), false);
}
for (int m = 0; m < selectors.size(); m++) {
this.seen.set(var(selectors.get(m)), false);
@@ -1073,4 +1073,3 @@ protected boolean isRotatable(final int lit) {
return true;
}
}
-
diff --git a/src/main/java/org/logicng/solvers/sat/MiniCard.java b/src/main/java/org/logicng/solvers/sat/MiniCard.java
index 09df3ab4..4e09f3f9 100644
--- a/src/main/java/org/logicng/solvers/sat/MiniCard.java
+++ b/src/main/java/org/logicng/solvers/sat/MiniCard.java
@@ -392,14 +392,14 @@ protected MSClause propagate() {
}
@Override
- protected boolean litRedundant(final int p, final int abstractLevels) {
- this.analyzeStack.clear();
- this.analyzeStack.push(p);
- final int top = this.analyzeToClear.size();
- while (this.analyzeStack.size() > 0) {
- assert v(this.analyzeStack.back()).reason() != null;
- final MSClause c = v(this.analyzeStack.back()).reason();
- this.analyzeStack.pop();
+ protected boolean litRedundant(final int p, final int abstractLevels, final LNGIntVector analyzeToClear) {
+ final LNGIntVector analyzeStack = new LNGIntVector();
+ analyzeStack.push(p);
+ final int top = analyzeToClear.size();
+ while (analyzeStack.size() > 0) {
+ assert v(analyzeStack.back()).reason() != null;
+ final MSClause c = v(analyzeStack.back()).reason();
+ analyzeStack.pop();
if (c.isAtMost()) {
for (int i = 0; i < c.size(); i++) {
if (value(c.get(i)) != Tristate.TRUE) {
@@ -409,13 +409,13 @@ protected boolean litRedundant(final int p, final int abstractLevels) {
if (!this.seen.get(var(q)) && v(q).level() > 0) {
if (v(q).reason() != null && (abstractLevel(var(q)) & abstractLevels) != 0) {
this.seen.set(var(q), true);
- this.analyzeStack.push(q);
- this.analyzeToClear.push(q);
+ analyzeStack.push(q);
+ analyzeToClear.push(q);
} else {
- for (int j = top; j < this.analyzeToClear.size(); j++) {
- this.seen.set(var(this.analyzeToClear.get(j)), false);
+ for (int j = top; j < analyzeToClear.size(); j++) {
+ this.seen.set(var(analyzeToClear.get(j)), false);
}
- this.analyzeToClear.removeElements(this.analyzeToClear.size() - top);
+ analyzeToClear.removeElements(analyzeToClear.size() - top);
return false;
}
}
@@ -426,13 +426,13 @@ protected boolean litRedundant(final int p, final int abstractLevels) {
if (!this.seen.get(var(q)) && v(q).level() > 0) {
if (v(q).reason() != null && (abstractLevel(var(q)) & abstractLevels) != 0) {
this.seen.set(var(q), true);
- this.analyzeStack.push(q);
- this.analyzeToClear.push(q);
+ analyzeStack.push(q);
+ analyzeToClear.push(q);
} else {
- for (int j = top; j < this.analyzeToClear.size(); j++) {
- this.seen.set(var(this.analyzeToClear.get(j)), false);
+ for (int j = top; j < analyzeToClear.size(); j++) {
+ this.seen.set(var(analyzeToClear.get(j)), false);
}
- this.analyzeToClear.removeElements(this.analyzeToClear.size() - top);
+ analyzeToClear.removeElements(analyzeToClear.size() - top);
return false;
}
}
@@ -808,14 +808,14 @@ protected void analyze(final MSClause conflictClause, final LNGIntVector outLear
protected void simplifyClause(final LNGIntVector outLearnt) {
int i;
int j;
- this.analyzeToClear = new LNGIntVector(outLearnt);
+ final LNGIntVector analyzeToClear = new LNGIntVector(outLearnt);
if (this.ccminMode == MiniSatConfig.ClauseMinimization.DEEP) {
int abstractLevel = 0;
for (i = 1; i < outLearnt.size(); i++) {
abstractLevel |= abstractLevel(var(outLearnt.get(i)));
}
for (i = j = 1; i < outLearnt.size(); i++) {
- if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel)) {
+ if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel, analyzeToClear)) {
outLearnt.set(j++, outLearnt.get(i));
}
}
@@ -850,8 +850,8 @@ protected void simplifyClause(final LNGIntVector outLearnt) {
outLearnt.set(1, p);
this.analyzeBtLevel = v(p).level();
}
- for (int l = 0; l < this.analyzeToClear.size(); l++) {
- this.seen.set(var(this.analyzeToClear.get(l)), false);
+ for (int l = 0; l < analyzeToClear.size(); l++) {
+ this.seen.set(var(analyzeToClear.get(l)), false);
}
}
diff --git a/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java b/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java
index 95e64afc..f042cc23 100644
--- a/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java
+++ b/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java
@@ -416,26 +416,26 @@ protected MSClause propagate() {
}
@Override
- protected boolean litRedundant(final int p, final int abstractLevels) {
- this.analyzeStack.clear();
- this.analyzeStack.push(p);
- final int top = this.analyzeToClear.size();
- while (this.analyzeStack.size() > 0) {
- assert v(this.analyzeStack.back()).reason() != null;
- final MSClause c = v(this.analyzeStack.back()).reason();
- this.analyzeStack.pop();
+ protected boolean litRedundant(final int p, final int abstractLevels, final LNGIntVector analyzeToClear) {
+ final LNGIntVector analyzeStack = new LNGIntVector();
+ analyzeStack.push(p);
+ final int top = analyzeToClear.size();
+ while (analyzeStack.size() > 0) {
+ assert v(analyzeStack.back()).reason() != null;
+ final MSClause c = v(analyzeStack.back()).reason();
+ analyzeStack.pop();
for (int i = 1; i < c.size(); i++) {
final int q = c.get(i);
if (!this.seen.get(var(q)) && v(q).level() > 0) {
if (v(q).reason() != null && (abstractLevel(var(q)) & abstractLevels) != 0) {
this.seen.set(var(q), true);
- this.analyzeStack.push(q);
- this.analyzeToClear.push(q);
+ analyzeStack.push(q);
+ analyzeToClear.push(q);
} else {
- for (int j = top; j < this.analyzeToClear.size(); j++) {
- this.seen.set(var(this.analyzeToClear.get(j)), false);
+ for (int j = top; j < analyzeToClear.size(); j++) {
+ this.seen.set(var(analyzeToClear.get(j)), false);
}
- this.analyzeToClear.removeElements(this.analyzeToClear.size() - top);
+ analyzeToClear.removeElements(analyzeToClear.size() - top);
return false;
}
}
@@ -684,14 +684,14 @@ protected void analyze(final MSClause conflictClause, final LNGIntVector outLear
protected void simplifyClause(final LNGIntVector outLearnt) {
int i;
int j;
- this.analyzeToClear = new LNGIntVector(outLearnt);
+ final LNGIntVector analyzeToClear = new LNGIntVector(outLearnt);
if (this.ccminMode == MiniSatConfig.ClauseMinimization.DEEP) {
int abstractLevel = 0;
for (i = 1; i < outLearnt.size(); i++) {
abstractLevel |= abstractLevel(var(outLearnt.get(i)));
}
for (i = j = 1; i < outLearnt.size(); i++) {
- if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel)) {
+ if (v(outLearnt.get(i)).reason() == null || !litRedundant(outLearnt.get(i), abstractLevel, analyzeToClear)) {
outLearnt.set(j++, outLearnt.get(i));
}
}
@@ -726,8 +726,8 @@ protected void simplifyClause(final LNGIntVector outLearnt) {
outLearnt.set(1, p);
this.analyzeBtLevel = v(p).level();
}
- for (int l = 0; l < this.analyzeToClear.size(); l++) {
- this.seen.set(var(this.analyzeToClear.get(l)), false);
+ for (int l = 0; l < analyzeToClear.size(); l++) {
+ this.seen.set(var(analyzeToClear.get(l)), false);
}
}
diff --git a/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java b/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java
index 691fc9a1..f60a9211 100644
--- a/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java
+++ b/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java
@@ -167,6 +167,66 @@ public boolean isAuxiliaryVariablesInModels() {
return this.auxiliaryVariablesInModels;
}
+ public double getVarDecay() {
+ return this.varDecay;
+ }
+
+ public double getVarInc() {
+ return this.varInc;
+ }
+
+ public ClauseMinimization getClauseMin() {
+ return this.clauseMin;
+ }
+
+ public int getRestartFirst() {
+ return this.restartFirst;
+ }
+
+ public double getRestartInc() {
+ return this.restartInc;
+ }
+
+ public double getClauseDecay() {
+ return this.clauseDecay;
+ }
+
+ public boolean isRemoveSatisfied() {
+ return this.removeSatisfied;
+ }
+
+ public double getLearntsizeFactor() {
+ return this.learntsizeFactor;
+ }
+
+ public double getLearntsizeInc() {
+ return this.learntsizeInc;
+ }
+
+ public boolean isIncremental() {
+ return this.incremental;
+ }
+
+ public boolean isInitialPhase() {
+ return this.initialPhase;
+ }
+
+ public boolean isProofGeneration() {
+ return this.proofGeneration;
+ }
+
+ public boolean isBbInitialUBCheckForRotatableLiterals() {
+ return this.bbInitialUBCheckForRotatableLiterals;
+ }
+
+ public boolean isBbCheckForComplementModelLiterals() {
+ return this.bbCheckForComplementModelLiterals;
+ }
+
+ public boolean isBbCheckForRotatableLiterals() {
+ return this.bbCheckForRotatableLiterals;
+ }
+
@Override
public String toString() {
final StringBuilder sb = new StringBuilder("MiniSatConfig{").append(System.lineSeparator());
@@ -346,7 +406,7 @@ public Builder proofGeneration(final boolean proofGeneration) {
/**
* Sets the CNF method for converting formula which are not in CNF for the solver. The default value
- * is {@code FACTORY_CNF}.
+ * is {@code PG_ON_SOLVER}.
* @param cnfMethod the CNF method
* @return the builder
*/
diff --git a/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java b/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java
index ec967348..c65bd45e 100644
--- a/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java
+++ b/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java
@@ -85,7 +85,7 @@ public abstract class MiniSatStyleSolver {
public static final int LIT_UNDEF = -1;
// external solver configuration
- protected final MiniSatConfig config;
+ protected MiniSatConfig config;
// internal solver state
protected boolean ok;
@@ -101,8 +101,6 @@ public abstract class MiniSatStyleSolver {
protected LNGIntVector conflict;
protected LNGIntVector assumptions;
protected LNGBooleanVector seen;
- protected LNGIntVector analyzeStack;
- protected LNGIntVector analyzeToClear;
protected int analyzeBtLevel;
protected double claInc;
protected int simpDBAssigns;
@@ -244,8 +242,6 @@ protected void initialize() {
this.conflict = new LNGIntVector();
this.assumptions = new LNGIntVector();
this.seen = new LNGBooleanVector();
- this.analyzeStack = new LNGIntVector();
- this.analyzeToClear = new LNGIntVector();
this.analyzeBtLevel = 0;
this.claInc = 1;
this.simpDBAssigns = -1;
@@ -633,9 +629,10 @@ protected void claBumpActivity(final MSClause c) {
* Returns {@code true} if a given literal is redundant in the current conflict analysis, {@code false} otherwise.
* @param p the literal
* @param abstractLevels an abstraction of levels
+ * @param analyzeToClear the clear analysis vector
* @return {@code true} if a given literal is redundant in the current conflict analysis
*/
- protected abstract boolean litRedundant(int p, int abstractLevels);
+ protected abstract boolean litRedundant(int p, int abstractLevels, LNGIntVector analyzeToClear);
/**
* Analysis the final conflict if there were assumptions.
@@ -743,8 +740,6 @@ public String toString() {
sb.append("conflict ").append(this.conflict).append(System.lineSeparator());
sb.append("assumptions ").append(this.assumptions).append(System.lineSeparator());
sb.append("#seen ").append(this.seen.size()).append(System.lineSeparator());
- sb.append("#stack ").append(this.analyzeStack.size()).append(System.lineSeparator());
- sb.append("#toclear ").append(this.analyzeToClear.size()).append(System.lineSeparator());
sb.append("claInc ").append(this.claInc).append(System.lineSeparator());
sb.append("simpDBAssigns ").append(this.simpDBAssigns).append(System.lineSeparator());
@@ -1122,4 +1117,12 @@ public void setSelectionOrder(final List selectionOrder) {
public void resetSelectionOrder() {
this.selectionOrder.clear();
}
+
+ /**
+ * Returns the solver config.
+ * @return the solver config
+ */
+ public MiniSatConfig getConfig() {
+ return this.config;
+ }
}
diff --git a/src/main/java/org/logicng/transformations/CanonicalEnumeration.java b/src/main/java/org/logicng/transformations/CanonicalEnumeration.java
index 35b9033a..91188056 100644
--- a/src/main/java/org/logicng/transformations/CanonicalEnumeration.java
+++ b/src/main/java/org/logicng/transformations/CanonicalEnumeration.java
@@ -43,7 +43,7 @@
/**
* Superclass for canonical normal form enumeration (CNF or DNF) via enumeration of the falsifying/satisfying assignments.
- * @version 2.3.0
+ * @version 2.5.0
* @since 2.3.0
*/
public abstract class CanonicalEnumeration {
@@ -65,9 +65,9 @@ protected static Formula compute(final Formula formula, final boolean cnf) {
final List ops = new ArrayList<>();
for (final Assignment a : enumeration) {
final SortedSet literals = a.literals();
- final Formula term = cnf ? f.or(FormulaHelper.negate(literals, ArrayList::new)) : f.and(a.literals());
+ final Formula term = cnf ? f.clause(FormulaHelper.negateLiterals(literals, ArrayList::new)) : f.term(a.literals());
ops.add(term);
}
- return cnf ? f.and(ops) : f.or(ops);
+ return cnf ? f.cnf(ops) : f.dnf(ops);
}
}
diff --git a/src/main/java/org/logicng/transformations/Subsumption.java b/src/main/java/org/logicng/transformations/Subsumption.java
index f7fb6896..9407b236 100644
--- a/src/main/java/org/logicng/transformations/Subsumption.java
+++ b/src/main/java/org/logicng/transformations/Subsumption.java
@@ -30,41 +30,40 @@
import org.logicng.datastructures.ubtrees.UBTree;
import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Literal;
+import org.logicng.formulas.NAryOperator;
import java.util.ArrayList;
import java.util.List;
-import java.util.Map;
-import java.util.SortedMap;
import java.util.SortedSet;
-import java.util.TreeMap;
/**
* A superclass for subsumptions (CNF or DNF).
- * @version 2.0.0
+ * @version 2.5.0
* @since 1.5.0
*/
public abstract class Subsumption {
- /**
- * Generates a UBTree from the formulas operands (clauses in CNF, minterms in DNF)
- * where all subsumed operands are already deleted.
- * @param formula the formula (must be an n-ary operator and CNF or DNF)
- * @return the UBTree with the operands and deleted subsumed operands
- */
- protected static UBTree generateSubsumedUBTree(final Formula formula) {
- final SortedMap>> mapping = new TreeMap<>();
- for (final Formula term : formula) {
- mapping.computeIfAbsent(term.literals().size(), k -> new ArrayList<>()).add(term.literals());
+ protected static Formula compute(final NAryOperator nary, final boolean cnf) {
+ final List> terms = getTerms(nary);
+ final UBTree ubTree = UBTree.generateSubsumedUBTree(terms);
+ return toNormalForm(ubTree, cnf, nary.factory());
+ }
+
+ private static List> getTerms(final NAryOperator nary) {
+ final List> terms = new ArrayList<>();
+ for (final Formula term : nary) {
+ terms.add(term.literals());
}
- final UBTree ubTree = new UBTree<>();
- for (final Map.Entry>> entry : mapping.entrySet()) {
- for (final SortedSet set : entry.getValue()) {
- if (ubTree.firstSubset(set) == null) {
- ubTree.addSet(set);
- }
- }
+ return terms;
+ }
+
+ private static Formula toNormalForm(final UBTree ubTree, final boolean cnf, final FormulaFactory f) {
+ final List terms = new ArrayList<>();
+ for (final SortedSet term : ubTree.allSets()) {
+ terms.add(cnf ? f.clause(term) : f.term(term));
}
- return ubTree;
+ return cnf ? f.cnf(terms) : f.dnf(terms);
}
}
diff --git a/src/main/java/org/logicng/transformations/cnf/CNFSubsumption.java b/src/main/java/org/logicng/transformations/cnf/CNFSubsumption.java
index f84e0f19..f02eaa80 100644
--- a/src/main/java/org/logicng/transformations/cnf/CNFSubsumption.java
+++ b/src/main/java/org/logicng/transformations/cnf/CNFSubsumption.java
@@ -28,23 +28,18 @@
package org.logicng.transformations.cnf;
-import org.logicng.datastructures.ubtrees.UBTree;
+import org.logicng.formulas.And;
import org.logicng.formulas.FType;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaTransformation;
-import org.logicng.formulas.Literal;
import org.logicng.transformations.Subsumption;
-import java.util.ArrayList;
-import java.util.List;
-import java.util.SortedSet;
-
/**
* This transformation performs subsumption on a given CNF and returns a new CNF.
* I.e. performs as many subsumptions as possible. A subsumption in a CNF means,
* that e.g. a clause {@code A | B | C} is subsumed by another clause {@code A | B}
* and can therefore be deleted for an equivalent CNF.
- * @version 2.3.0
+ * @version 2.5.0
* @since 1.5.0
*/
public final class CNFSubsumption extends Subsumption implements FormulaTransformation {
@@ -77,11 +72,6 @@ public Formula apply(final Formula formula, final boolean cache) {
return formula;
}
assert formula.type() == FType.AND;
- final UBTree ubTree = generateSubsumedUBTree(formula);
- final List clauses = new ArrayList<>();
- for (final SortedSet literals : ubTree.allSets()) {
- clauses.add(formula.factory().clause(literals));
- }
- return formula.factory().cnf(clauses);
+ return compute((And) formula, true);
}
}
diff --git a/src/main/java/org/logicng/transformations/dnf/DNFSubsumption.java b/src/main/java/org/logicng/transformations/dnf/DNFSubsumption.java
index 1061438c..1f82653f 100644
--- a/src/main/java/org/logicng/transformations/dnf/DNFSubsumption.java
+++ b/src/main/java/org/logicng/transformations/dnf/DNFSubsumption.java
@@ -28,23 +28,18 @@
package org.logicng.transformations.dnf;
-import org.logicng.datastructures.ubtrees.UBTree;
import org.logicng.formulas.FType;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaTransformation;
-import org.logicng.formulas.Literal;
+import org.logicng.formulas.Or;
import org.logicng.transformations.Subsumption;
-import java.util.ArrayList;
-import java.util.List;
-import java.util.SortedSet;
-
/**
* This transformation performs subsumption on a given DNF and returns a new DNF.
* I.e. performs as many subsumptions as possible. A subsumption in a DNF means,
* that e.g. a minterm {@code A & B & C} is subsumed by another minterm {@code A & B}
* and can therefore be deleted for an equivalent DNF.
- * @version 2.3.0
+ * @version 2.5.0
* @since 1.5.0
*/
public final class DNFSubsumption extends Subsumption implements FormulaTransformation {
@@ -76,11 +71,6 @@ public Formula apply(final Formula formula, final boolean cache) {
return formula;
}
assert formula.type() == FType.OR;
- final UBTree ubTree = generateSubsumedUBTree(formula);
- final List minterms = new ArrayList<>();
- for (final SortedSet literals : ubTree.allSets()) {
- minterms.add(formula.factory().and(literals));
- }
- return formula.factory().or(minterms);
+ return compute((Or) formula, false);
}
}
diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
index 7d57439c..5e28a285 100644
--- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
+++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
@@ -28,10 +28,6 @@
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;
@@ -45,6 +41,7 @@
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;
@@ -72,7 +69,7 @@
*
* 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 {
@@ -126,15 +123,16 @@ 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);
+ final OptimizationConfig cfg = config.optimizationConfig;
+ cfg.startHandler();
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;
+ .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();
@@ -142,18 +140,18 @@ public Formula apply(final Formula formula, final boolean cache) {
backboneLiterals.addAll(backbone.getCompleteBackbone());
simplified = formula.restrict(new Assignment(backboneLiterals));
}
- final Formula simplifyMinDnf = computeMinDnf(f, simplified, config);
- if (simplifyMinDnf == null) {
- return null;
+ if (config.minimalDnfCover) {
+ final Formula simplifyMinDnf = computeMinDnf(f, simplified, config);
+ if (simplifyMinDnf == null) {
+ return config.returnIntermediateResult ? addLiterals(simplified, backboneLiterals) : null;
+ }
+ simplified = simplifyWithRating(simplified, simplifyMinDnf, config);
}
- simplified = simplifyWithRating(simplified, simplifyMinDnf, config);
if (config.factorOut) {
final Formula factoredOut = simplified.transform(new FactorOutSimplifier(config.ratingFunction));
simplified = simplifyWithRating(simplified, factoredOut, config);
}
- if (config.restrictBackbone) {
- simplified = f.and(f.and(backboneLiterals), simplified);
- }
+ simplified = addLiterals(simplified, backboneLiterals);
if (config.simplifyNegations) {
final Formula negationSimplified = simplified.transform(NegationSimplifier.get());
simplified = simplifyWithRating(simplified, negationSimplified, config);
@@ -161,20 +159,24 @@ public Formula apply(final Formula formula, final boolean cache) {
return simplified;
}
- private Formula computeMinDnf(final FormulaFactory f, Formula simplified, final AdvancedSimplifierConfig config) {
+ private static Formula addLiterals(final Formula formula, final SortedSet literals) {
+ final FormulaFactory f = formula.factory();
+ return f.and(f.and(literals), formula);
+ }
+
+ private Formula computeMinDnf(final FormulaFactory f, final Formula simplified, final AdvancedSimplifierConfig config) {
final PrimeResult primeResult =
- PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.handler);
- if (primeResult == null || aborted(config.handler)) {
+ PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.optimizationConfig);
+ if (primeResult == null || config.optimizationConfig.aborted()) {
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)) {
+ Collections.singletonList(simplified), f, config.optimizationConfig);
+ if (minimizedPIs == null || config.optimizationConfig.aborted()) {
return null;
}
- simplified = f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList()));
- return simplified;
+ return f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList()));
}
private List negateAllLiterals(final Collection> literalSets, final FormulaFactory f) {
diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
index f3f1af55..a89733e3 100644
--- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
+++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
@@ -31,29 +31,34 @@
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}.
- * @version 2.3.0
+ * @version 2.6.0
* @since 2.3.0
*/
public class AdvancedSimplifierConfig extends Configuration {
boolean restrictBackbone;
+ boolean minimalDnfCover;
boolean factorOut;
boolean simplifyNegations;
+ boolean returnIntermediateResult;
RatingFunction ratingFunction;
- OptimizationHandler handler;
+ OptimizationConfig optimizationConfig;
@Override
public String toString() {
return "AdvancedSimplifierConfig{" +
"restrictBackbone=" + this.restrictBackbone +
+ ", minimalDnfCover=" + this.minimalDnfCover +
", factorOut=" + this.factorOut +
", simplifyNegations=" + this.simplifyNegations +
+ ", returnIntermediateResult=" + this.returnIntermediateResult +
", ratingFunction=" + this.ratingFunction +
- ", handler=" + this.handler +
+ ", optimizationConfig=" + this.optimizationConfig +
'}';
}
@@ -64,10 +69,12 @@ public String toString() {
private AdvancedSimplifierConfig(final Builder builder) {
super(ConfigurationType.ADVANCED_SIMPLIFIER);
this.restrictBackbone = builder.restrictBackbone;
+ this.minimalDnfCover = builder.minimalDnfCover;
this.factorOut = builder.factorOut;
this.simplifyNegations = builder.simplifyNegations;
+ this.returnIntermediateResult = builder.returnIntermediateResult;
this.ratingFunction = builder.ratingFunction;
- this.handler = builder.handler;
+ this.optimizationConfig = builder.optimizationConfig;
}
/**
@@ -83,18 +90,21 @@ public static Builder builder() {
*/
public static class Builder {
- boolean restrictBackbone = true;
- boolean factorOut = true;
- boolean simplifyNegations = true;
- private RatingFunction ratingFunction = new DefaultRatingFunction();
- private OptimizationHandler handler = null;
+ private boolean restrictBackbone = true;
+ private boolean minimalDnfCover = true;
+ private boolean factorOut = true;
+ private boolean simplifyNegations = true;
+ private boolean returnIntermediateResult = false;
+ private RatingFunction ratingFunction = DefaultRatingFunction.get();
+ private OptimizationConfig optimizationConfig = OptimizationConfig.sat(null);
private Builder() {
// Initialize only via factory
}
/**
- * Sets the flag for whether the formula should be restricted with the backbone. The default is 'true'.
+ * Sets the flag for whether the formula should be restricted with the
+ * backbone. The default is 'true'.
* @param restrictBackbone flag for the restriction
* @return the current builder
*/
@@ -104,7 +114,19 @@ public Builder restrictBackbone(final boolean restrictBackbone) {
}
/**
- * Sets the flag for whether the formula should be factorized. The default is 'true'.
+ * Sets the flag for whether a minimal DNF cover should be computed. The
+ * default is 'true'.
+ * @param minimalDnfCover flag for the minimal DNF cover computation
+ * @return the current builder
+ */
+ public Builder minimalDnfCover(final boolean minimalDnfCover) {
+ this.minimalDnfCover = minimalDnfCover;
+ return this;
+ }
+
+ /**
+ * Sets the flag for whether the formula should be factorized. The
+ * default is 'true'.
* @param factorOut flag for the factorisation
* @return the current builder
*/
@@ -114,7 +136,8 @@ public Builder factorOut(final boolean factorOut) {
}
/**
- * Sets the flag for whether negations shall be simplified. The default is 'true'.
+ * Sets the flag for whether negations shall be simplified. The
+ * default is 'true'.
* @param simplifyNegations flag
* @return the current builder
*/
@@ -124,8 +147,11 @@ public Builder simplifyNegations(final boolean simplifyNegations) {
}
/**
- * Sets the rating function. The aim of the simplification is to minimize the formula with respect to this rating function,
- * e.g. finding a formula with a minimal number of symbols when represented as string. The default is the {@code DefaultRatingFunction}.
+ * Sets the rating function. The aim of the simplification is to
+ * minimize the formula with respect to this rating function,
+ * e.g. finding a formula with a minimal number of symbols when
+ * represented as string. The default is the
+ * {@code DefaultRatingFunction}.
* @param ratingFunction the desired rating function
* @return the current builder
*/
@@ -135,12 +161,37 @@ public Builder ratingFunction(final RatingFunction ratingFunction) {
}
/**
- * Sets the handler to control the computation. The default is 'no handler'.
+ * 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 = OptimizationConfig.sat(handler);
+ return this;
+ }
+
+ /**
+ * Sets the optimization config of the computation. The default is a
+ * config with a SAT based optimization without a handler.
+ * @param config the optimization config
+ * @return the current builder
+ */
+ public Builder optimizationConfig(final OptimizationConfig config) {
+ this.optimizationConfig = config;
+ return this;
+ }
+
+ /**
+ * Sets whether the intermediate result should be returned in case of
+ * a handler abortion. The default is 'false'.
+ * @param returnIntermediateResult the flag
+ * @return the current builder
+ */
+ public Builder returnIntermediateResult(final boolean returnIntermediateResult) {
+ this.returnIntermediateResult = returnIntermediateResult;
return this;
}
diff --git a/src/main/antlr/LogicNGPropositional.g4 b/src/test/antlr/LogicNGPropositional.g4
similarity index 100%
rename from src/main/antlr/LogicNGPropositional.g4
rename to src/test/antlr/LogicNGPropositional.g4
diff --git a/src/main/antlr/LogicNGPseudoBoolean.g4 b/src/test/antlr/LogicNGPseudoBoolean.g4
similarity index 100%
rename from src/main/antlr/LogicNGPseudoBoolean.g4
rename to src/test/antlr/LogicNGPseudoBoolean.g4
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/TestWithExampleFormulas.java b/src/test/java/org/logicng/TestWithExampleFormulas.java
index b6c1fe5f..fb953713 100644
--- a/src/test/java/org/logicng/TestWithExampleFormulas.java
+++ b/src/test/java/org/logicng/TestWithExampleFormulas.java
@@ -34,6 +34,8 @@
import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Literal;
import org.logicng.formulas.Variable;
+import org.logicng.io.parsers.ParserException;
+import org.logicng.io.parsers.PseudoBooleanParser;
public abstract class TestWithExampleFormulas {
protected final FormulaFactory f = new FormulaFactory();
@@ -89,4 +91,12 @@ public abstract class TestWithExampleFormulas {
protected final Formula PBC3 = this.f.pbc(CType.GE, 2, this.literals, this.coefficients);
protected final Formula PBC4 = this.f.pbc(CType.LT, 2, this.literals, this.coefficients);
protected final Formula PBC5 = this.f.pbc(CType.LE, 2, this.literals, this.coefficients);
+
+ public static Formula parse(final FormulaFactory f, final String formula) {
+ try {
+ return new PseudoBooleanParser(f).parse(formula);
+ } catch (final ParserException e) {
+ throw new RuntimeException(e);
+ }
+ }
}
diff --git a/src/test/java/org/logicng/datastructures/AssignmentTest.java b/src/test/java/org/logicng/datastructures/AssignmentTest.java
index 39600551..10121152 100644
--- a/src/test/java/org/logicng/datastructures/AssignmentTest.java
+++ b/src/test/java/org/logicng/datastructures/AssignmentTest.java
@@ -207,7 +207,7 @@ public void testEquals() {
}
@Test
- public void testBlockingClause() throws ParserException {
+ public void testBlockingClause() {
final Assignment ass = new Assignment();
ass.addLiteral(this.A);
ass.addLiteral(this.B);
@@ -215,14 +215,14 @@ public void testBlockingClause() throws ParserException {
ass.addLiteral(this.NY);
final Formula bc01 = ass.blockingClause(this.f);
assertThat(bc01.containsVariable(this.C)).isFalse();
- assertThat(bc01).isEqualTo(this.f.parse("~a | ~b | x | y"));
+ assertThat(bc01).isEqualTo(parse(this.f, "~a | ~b | x | y"));
final Formula bc02 = ass.blockingClause(this.f, null);
assertThat(bc02.containsVariable(this.C)).isFalse();
- assertThat(bc02).isEqualTo(this.f.parse("~a | ~b | x | y"));
+ assertThat(bc02).isEqualTo(parse(this.f, "~a | ~b | x | y"));
final List lits = Arrays.asList(this.A, this.X, this.C);
final Formula bcProjected = ass.blockingClause(this.f, lits);
assertThat(bcProjected.containsVariable(this.C)).isFalse();
- assertThat(bcProjected).isEqualTo(this.f.parse("~a | x"));
+ assertThat(bcProjected).isEqualTo(parse(this.f, "~a | x"));
}
@Test
diff --git a/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java b/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java
index 3bb02d6e..9540af75 100644
--- a/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java
+++ b/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java
@@ -28,26 +28,49 @@
package org.logicng.datastructures.ubtrees;
+import static java.util.Arrays.asList;
+import static java.util.Collections.emptyList;
+import static java.util.Collections.singletonList;
import static org.assertj.core.api.Assertions.assertThat;
import org.junit.jupiter.api.Test;
-import java.util.Arrays;
import java.util.SortedSet;
import java.util.TreeSet;
/**
* Unit tests for {@link UBTree}.
- * @version 2.0.0
+ * @version 2.5.0
* @since 1.5.0
*/
public class UBTreeTest {
+ @Test
+ public void testGenerateSubsumedUBTree() {
+ final SortedSet e0123 = set("e0", "e1", "e2", "e3");
+ final SortedSet e013 = set("e0", "e1", "e3");
+ final SortedSet e012 = set("e0", "e1", "e2");
+ final SortedSet e23 = set("e2", "e3");
+ final SortedSet empty = set();
+ assertThat(UBTree.generateSubsumedUBTree(emptyList()).allSets()).isEmpty();
+ assertThat(UBTree.generateSubsumedUBTree(singletonList(e0123)).allSets()).containsExactlyInAnyOrder(e0123);
+ assertThat(UBTree.generateSubsumedUBTree(asList(e0123, e013, e012, e23)).allSets()).containsExactlyInAnyOrder(e013, e012, e23);
+ assertThat(UBTree.generateSubsumedUBTree(asList(e0123, e013, e012, e23, empty)).allSets()).containsExactlyInAnyOrder(empty);
+ }
+
+ @Test
+ public void testEmtpyUBTree() {
+ final UBTree tree = new UBTree<>();
+ assertThat(tree.rootNodes()).isEmpty();
+ assertThat(tree.rootSet()).isNull();
+ }
+
@Test
public void testEmptySet() {
final UBTree tree = new UBTree<>();
tree.addSet(new TreeSet<>());
assertThat(tree.rootNodes()).isEmpty();
+ assertThat(tree.rootSet()).isEmpty();
}
@Test
@@ -65,6 +88,7 @@ public void testSingleSet() {
assertThat(tree.rootNodes().get("A").children().get("B").children().get("C").isEndOfPath()).isTrue();
assertThat(tree.rootNodes().get("A").children().get("B").children().get("C").set()).isEqualTo(set("A", "B", "C"));
assertThat(tree.rootNodes().get("A").children().get("B").children().get("C").children()).isEmpty();
+ assertThat(tree.rootSet()).isNull();
}
@Test
@@ -76,6 +100,7 @@ public void testExampleFromPaper() {
tree.addSet(set("e2", "e3"));
assertThat(tree.rootNodes()).hasSize(2);
assertThat(tree.rootNodes().keySet()).containsExactly("e0", "e2");
+ assertThat(tree.rootSet()).isNull();
// root nodes
final UBNode e0 = tree.rootNodes().get("e0");
@@ -122,6 +147,7 @@ public void testContainsSubset() {
tree.addSet(e013);
tree.addSet(e012);
tree.addSet(e23);
+ assertThat(tree.firstSubset(set())).isNull();
assertThat(tree.firstSubset(set("e0"))).isNull();
assertThat(tree.firstSubset(set("e1"))).isNull();
assertThat(tree.firstSubset(set("e2"))).isNull();
@@ -154,6 +180,52 @@ public void testContainsSubset() {
assertThat(tree.firstSubset(set("e0", "e1", "e2", "e3", "e4"))).isIn(e0123, e013, e012, e23);
}
+ @Test
+ public void testContainsSubsetWithEmtpySet() {
+ final UBTree tree = new UBTree<>();
+ final SortedSet e0123 = set("e0", "e1", "e2", "e3");
+ final SortedSet e013 = set("e0", "e1", "e3");
+ final SortedSet e012 = set("e0", "e1", "e2");
+ final SortedSet e23 = set("e2", "e3");
+ final SortedSet empty = set();
+ tree.addSet(e0123);
+ tree.addSet(e013);
+ tree.addSet(e012);
+ tree.addSet(e23);
+ tree.addSet(empty);
+ assertThat(tree.firstSubset(set())).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e2"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e2"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1", "e2"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1", "e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e2", "e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1", "e2"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1", "e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e2", "e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1", "e2", "e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1", "e2", "e3"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e2", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e3", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e2", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e3", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1", "e2", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1", "e3", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e2", "e3", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1", "e2", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1", "e3", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e2", "e3", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e1", "e2", "e3", "e4"))).isEqualTo(empty);
+ assertThat(tree.firstSubset(set("e0", "e1", "e2", "e3", "e4"))).isEqualTo(empty);
+ }
+
@Test
public void testAllSubsets() {
final UBTree tree = new UBTree<>();
@@ -165,6 +237,7 @@ public void testAllSubsets() {
tree.addSet(e013);
tree.addSet(e012);
tree.addSet(e23);
+ assertThat(tree.allSubsets(set())).isEmpty();
assertThat(tree.allSubsets(set("e0"))).isEmpty();
assertThat(tree.allSubsets(set("e1"))).isEmpty();
assertThat(tree.allSubsets(set("e2"))).isEmpty();
@@ -197,6 +270,52 @@ public void testAllSubsets() {
assertThat(tree.allSubsets(set("e0", "e1", "e2", "e3", "e4"))).containsExactlyInAnyOrder(e0123, e013, e012, e23);
}
+ @Test
+ public void testAllSubsetsWithEmptySet() {
+ final UBTree tree = new UBTree<>();
+ final SortedSet e0123 = set("e0", "e1", "e2", "e3");
+ final SortedSet e013 = set("e0", "e1", "e3");
+ final SortedSet e012 = set("e0", "e1", "e2");
+ final SortedSet e23 = set("e2", "e3");
+ final SortedSet empty = set();
+ tree.addSet(e0123);
+ tree.addSet(e013);
+ tree.addSet(e012);
+ tree.addSet(e23);
+ tree.addSet(empty);
+ assertThat(tree.allSubsets(set())).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e0"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e1"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e2"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e3"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e0", "e1"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e0", "e2"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e0", "e3"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e1", "e2"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e1", "e3"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e2", "e3"))).containsExactlyInAnyOrder(empty, e23);
+ assertThat(tree.allSubsets(set("e0", "e1", "e2"))).containsExactlyInAnyOrder(empty, e012);
+ assertThat(tree.allSubsets(set("e0", "e1", "e3"))).containsExactlyInAnyOrder(empty, e013);
+ assertThat(tree.allSubsets(set("e0", "e2", "e3"))).containsExactlyInAnyOrder(empty, e23);
+ assertThat(tree.allSubsets(set("e1", "e2", "e3"))).containsExactlyInAnyOrder(empty, e23);
+ assertThat(tree.allSubsets(set("e0", "e1", "e2", "e3"))).containsExactlyInAnyOrder(empty, e0123, e013, e012, e23);
+ assertThat(tree.allSubsets(set("e0", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e1", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e2", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e3", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e0", "e1", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e0", "e2", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e0", "e3", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e1", "e2", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e1", "e3", "e4"))).containsExactlyInAnyOrder(empty);
+ assertThat(tree.allSubsets(set("e2", "e3", "e4"))).containsExactlyInAnyOrder(empty, e23);
+ assertThat(tree.allSubsets(set("e0", "e1", "e2", "e4"))).containsExactlyInAnyOrder(empty, e012);
+ assertThat(tree.allSubsets(set("e0", "e1", "e3", "e4"))).containsExactlyInAnyOrder(empty, e013);
+ assertThat(tree.allSubsets(set("e0", "e2", "e3", "e4"))).containsExactlyInAnyOrder(empty, e23);
+ assertThat(tree.allSubsets(set("e1", "e2", "e3", "e4"))).containsExactlyInAnyOrder(empty, e23);
+ assertThat(tree.allSubsets(set("e0", "e1", "e2", "e3", "e4"))).containsExactlyInAnyOrder(empty, e0123, e013, e012, e23);
+ }
+
@Test
public void testAllSupersets() {
final UBTree tree = new UBTree<>();
@@ -208,6 +327,52 @@ public void testAllSupersets() {
tree.addSet(e013);
tree.addSet(e012);
tree.addSet(e23);
+ assertThat(tree.allSupersets(set())).containsExactlyInAnyOrder(e0123, e013, e012, e23);
+ assertThat(tree.allSupersets(set("e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0"))).containsExactlyInAnyOrder(e0123, e012, e013);
+ assertThat(tree.allSupersets(set("e1"))).containsExactlyInAnyOrder(e0123, e012, e013);
+ assertThat(tree.allSupersets(set("e2"))).containsExactlyInAnyOrder(e0123, e012, e23);
+ assertThat(tree.allSupersets(set("e3"))).containsExactlyInAnyOrder(e0123, e013, e23);
+ assertThat(tree.allSupersets(set("e0", "e1"))).containsExactlyInAnyOrder(e0123, e012, e013);
+ assertThat(tree.allSupersets(set("e0", "e2"))).containsExactlyInAnyOrder(e0123, e012);
+ assertThat(tree.allSupersets(set("e0", "e3"))).containsExactlyInAnyOrder(e0123, e013);
+ assertThat(tree.allSupersets(set("e1", "e2"))).containsExactlyInAnyOrder(e0123, e012);
+ assertThat(tree.allSupersets(set("e1", "e3"))).containsExactlyInAnyOrder(e0123, e013);
+ assertThat(tree.allSupersets(set("e2", "e3"))).containsExactlyInAnyOrder(e0123, e23);
+ assertThat(tree.allSupersets(set("e0", "e1", "e2"))).containsExactlyInAnyOrder(e0123, e012);
+ assertThat(tree.allSupersets(set("e0", "e2", "e3"))).containsExactlyInAnyOrder(e0123);
+ assertThat(tree.allSupersets(set("e0", "e1", "e2", "e3"))).containsExactlyInAnyOrder(e0123);
+ assertThat(tree.allSupersets(set("e0", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e1", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e2", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e3", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0", "e1", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0", "e2", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0", "e3", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e1", "e2", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e1", "e3", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e2", "e3", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0", "e1", "e2", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0", "e1", "e3", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0", "e2", "e3", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e1", "e2", "e3", "e4"))).isEmpty();
+ assertThat(tree.allSupersets(set("e0", "e1", "e2", "e3", "e4"))).isEmpty();
+ }
+
+ @Test
+ public void testAllSupersetsWithEmptySet() {
+ final UBTree tree = new UBTree<>();
+ final SortedSet e0123 = set("e0", "e1", "e2", "e3");
+ final SortedSet e013 = set("e0", "e1", "e3");
+ final SortedSet e012 = set("e0", "e1", "e2");
+ final SortedSet e23 = set("e2", "e3");
+ final SortedSet empty = set();
+ tree.addSet(e0123);
+ tree.addSet(e013);
+ tree.addSet(e012);
+ tree.addSet(e23);
+ tree.addSet(empty);
+ assertThat(tree.allSupersets(set())).containsExactlyInAnyOrder(e0123, e013, e012, e23, empty);
assertThat(tree.allSupersets(set("e4"))).isEmpty();
assertThat(tree.allSupersets(set("e0"))).containsExactlyInAnyOrder(e0123, e012, e013);
assertThat(tree.allSupersets(set("e1"))).containsExactlyInAnyOrder(e0123, e012, e013);
@@ -246,6 +411,7 @@ public void testAllSets() {
final SortedSet e013 = set("e0", "e1", "e3");
final SortedSet e012 = set("e0", "e1", "e2");
final SortedSet e23 = set("e2", "e3");
+ final SortedSet empty = set();
tree.addSet(e0123);
assertThat(tree.allSets()).containsExactlyInAnyOrder(e0123);
tree.addSet(e013);
@@ -254,9 +420,11 @@ public void testAllSets() {
assertThat(tree.allSets()).containsExactlyInAnyOrder(e0123, e013, e012);
tree.addSet(e23);
assertThat(tree.allSets()).containsExactlyInAnyOrder(e0123, e013, e012, e23);
+ tree.addSet(empty);
+ assertThat(tree.allSets()).containsExactlyInAnyOrder(e0123, e013, e012, e23, empty);
}
- private SortedSet set(final String... elements) {
- return new TreeSet<>(Arrays.asList(elements));
+ private static SortedSet set(final String... elements) {
+ return new TreeSet<>(asList(elements));
}
}
diff --git a/src/test/java/org/logicng/explanations/drup/DRUPTest.java b/src/test/java/org/logicng/explanations/drup/DRUPTest.java
index 1c573032..018b4569 100644
--- a/src/test/java/org/logicng/explanations/drup/DRUPTest.java
+++ b/src/test/java/org/logicng/explanations/drup/DRUPTest.java
@@ -29,6 +29,7 @@
package org.logicng.explanations.drup;
import static org.assertj.core.api.Assertions.assertThat;
+import static org.logicng.TestWithExampleFormulas.parse;
import static org.logicng.datastructures.Tristate.FALSE;
import static org.logicng.datastructures.Tristate.TRUE;
@@ -40,7 +41,6 @@
import org.logicng.explanations.UNSATCore;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
-import org.logicng.io.parsers.ParserException;
import org.logicng.io.readers.DimacsReader;
import org.logicng.propositions.ExtendedProposition;
import org.logicng.propositions.Proposition;
@@ -145,16 +145,16 @@ public void testUnsatCoresAimTestset() throws IOException {
}
@Test
- public void testPropositionHandling() throws ParserException {
+ public void testPropositionHandling() {
final List propositions = new ArrayList<>();
- propositions.add(new StandardProposition("P1", this.f.parse("((a & b) => c) & ((a & b) => d)")));
- propositions.add(new StandardProposition("P2", this.f.parse("(c & d) <=> ~e")));
- propositions.add(new StandardProposition("P3", this.f.parse("~e => f | g")));
- propositions.add(new StandardProposition("P4", this.f.parse("(f => ~a) & (g => ~b) & p & q")));
- propositions.add(new StandardProposition("P5", this.f.parse("a => b")));
- propositions.add(new StandardProposition("P6", this.f.parse("a")));
- propositions.add(new StandardProposition("P7", this.f.parse("g | h")));
- propositions.add(new StandardProposition("P8", this.f.parse("(x => ~y | z) & (z | w)")));
+ propositions.add(new StandardProposition("P1", parse(this.f, "((a & b) => c) & ((a & b) => d)")));
+ propositions.add(new StandardProposition("P2", parse(this.f, "(c & d) <=> ~e")));
+ propositions.add(new StandardProposition("P3", parse(this.f, "~e => f | g")));
+ propositions.add(new StandardProposition("P4", parse(this.f, "(f => ~a) & (g => ~b) & p & q")));
+ propositions.add(new StandardProposition("P5", parse(this.f, "a => b")));
+ propositions.add(new StandardProposition("P6", parse(this.f, "a")));
+ propositions.add(new StandardProposition("P7", parse(this.f, "g | h")));
+ propositions.add(new StandardProposition("P8", parse(this.f, "(x => ~y | z) & (z | w)")));
for (final SATSolver solver : this.solvers) {
solver.addPropositions(propositions);
@@ -167,19 +167,19 @@ public void testPropositionHandling() throws ParserException {
}
@Test
- public void testPropositionIncDec() throws ParserException {
+ public void testPropositionIncDec() {
final SATSolver solver = this.solvers[0];
- final StandardProposition p1 = new StandardProposition("P1", this.f.parse("((a & b) => c) & ((a & b) => d)"));
- final StandardProposition p2 = new StandardProposition("P2", this.f.parse("(c & d) <=> ~e"));
- final StandardProposition p3 = new StandardProposition("P3", this.f.parse("~e => f | g"));
- final StandardProposition p4 = new StandardProposition("P4", this.f.parse("(f => ~a) & (g => ~b) & p & q"));
- final StandardProposition p5 = new StandardProposition("P5", this.f.parse("a => b"));
- final StandardProposition p6 = new StandardProposition("P6", this.f.parse("a"));
- final StandardProposition p7 = new StandardProposition("P7", this.f.parse("g | h"));
- final StandardProposition p8 = new StandardProposition("P8", this.f.parse("(x => ~y | z) & (z | w)"));
- final StandardProposition p9 = new StandardProposition("P9", this.f.parse("a & b"));
- final StandardProposition p10 = new StandardProposition("P10", this.f.parse("(p => q) & p"));
- final StandardProposition p11 = new StandardProposition("P11", this.f.parse("a & ~q"));
+ final StandardProposition p1 = new StandardProposition("P1", parse(this.f, "((a & b) => c) & ((a & b) => d)"));
+ final StandardProposition p2 = new StandardProposition("P2", parse(this.f, "(c & d) <=> ~e"));
+ final StandardProposition p3 = new StandardProposition("P3", parse(this.f, "~e => f | g"));
+ final StandardProposition p4 = new StandardProposition("P4", parse(this.f, "(f => ~a) & (g => ~b) & p & q"));
+ final StandardProposition p5 = new StandardProposition("P5", parse(this.f, "a => b"));
+ final StandardProposition p6 = new StandardProposition("P6", parse(this.f, "a"));
+ final StandardProposition p7 = new StandardProposition("P7", parse(this.f, "g | h"));
+ final StandardProposition p8 = new StandardProposition("P8", parse(this.f, "(x => ~y | z) & (z | w)"));
+ final StandardProposition p9 = new StandardProposition("P9", parse(this.f, "a & b"));
+ final StandardProposition p10 = new StandardProposition("P10", parse(this.f, "(p => q) & p"));
+ final StandardProposition p11 = new StandardProposition("P11", parse(this.f, "a & ~q"));
solver.addPropositions(p1, p2, p3, p4);
final SolverState state1 = solver.saveState();
@@ -218,10 +218,10 @@ public void testPropositionIncDec() throws ParserException {
}
@Test
- public void testTrivialCasesPropositions() throws ParserException {
+ public void testTrivialCasesPropositions() {
for (final SATSolver solver : this.solvers) {
assertSolverSat(solver);
- final StandardProposition p1 = new StandardProposition("P1", this.f.parse("$false"));
+ final StandardProposition p1 = new StandardProposition("P1", parse(this.f, "$false"));
solver.add(p1);
assertSolverUnsat(solver);
UNSATCore unsatCore = solver.unsatCore();
@@ -229,10 +229,10 @@ public void testTrivialCasesPropositions() throws ParserException {
solver.reset();
assertSolverSat(solver);
- final StandardProposition p2 = new StandardProposition("P2", this.f.parse("a"));
+ final StandardProposition p2 = new StandardProposition("P2", parse(this.f, "a"));
solver.add(p2);
assertSolverSat(solver);
- final StandardProposition p3 = new StandardProposition("P3", this.f.parse("~a"));
+ final StandardProposition p3 = new StandardProposition("P3", parse(this.f, "~a"));
solver.add(p3);
assertSolverUnsat(solver);
unsatCore = solver.unsatCore();
@@ -241,15 +241,15 @@ public void testTrivialCasesPropositions() throws ParserException {
}
@Test
- public void testCoreAndAssumptions() throws ParserException {
+ public void testCoreAndAssumptions() {
final FormulaFactory f = new FormulaFactory();
final SATSolver[] solvers = new SATSolver[]{
MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()),
MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build())
};
for (final SATSolver solver : solvers) {
- final StandardProposition p1 = new StandardProposition(f.parse("A => B"));
- final StandardProposition p2 = new StandardProposition(f.parse("A & B => G"));
+ final StandardProposition p1 = new StandardProposition(parse(f, "A => B"));
+ final StandardProposition p2 = new StandardProposition(parse(f, "A & B => G"));
final StandardProposition p3 = new StandardProposition(f.or(f.literal("X", false), f.literal("A", true)));
final StandardProposition p4 = new StandardProposition(f.or(f.literal("X", false), f.literal("G", false)));
final StandardProposition p5 = new StandardProposition(f.literal("G", false));
@@ -271,28 +271,28 @@ public void testCoreAndAssumptions() throws ParserException {
}
@Test
- public void testCoreAndAssumptions2() throws ParserException {
+ public void testCoreAndAssumptions2() {
final FormulaFactory f = new FormulaFactory();
final SATSolver[] solvers = new SATSolver[]{
MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()),
MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build())
};
for (final SATSolver solver : solvers) {
- solver.add(f.parse("~C => D"));
- solver.add(f.parse("C => D"));
- solver.add(f.parse("D => B | A"));
- solver.add(f.parse("B => X"));
- solver.add(f.parse("B => ~X"));
+ solver.add(parse(f, "~C => D"));
+ solver.add(parse(f, "C => D"));
+ solver.add(parse(f, "D => B | A"));
+ solver.add(parse(f, "B => X"));
+ solver.add(parse(f, "B => ~X"));
solver.sat(f.literal("A", false));
- solver.add(f.parse("~A"));
+ solver.add(parse(f, "~A"));
solver.sat();
assertThat(solver.unsatCore()).isNotNull();
}
}
@Test
- public void testCoreAndAssumptions3() throws ParserException {
+ public void testCoreAndAssumptions3() {
// Unit test for DRUP issue which led to java.lang.ArrayIndexOutOfBoundsException: -1
final FormulaFactory f = new FormulaFactory();
final SATSolver[] solvers = new SATSolver[]{
@@ -300,21 +300,21 @@ public void testCoreAndAssumptions3() throws ParserException {
MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build())
};
for (final SATSolver solver : solvers) {
- solver.add(f.parse("X => Y"));
- solver.add(f.parse("X => Z"));
- solver.add(f.parse("C => E"));
- solver.add(f.parse("D => ~F"));
- solver.add(f.parse("B => M"));
- solver.add(f.parse("D => N"));
- solver.add(f.parse("G => O"));
- solver.add(f.parse("A => B"));
- solver.add(f.parse("T1 <=> A & K & ~B & ~C"));
- solver.add(f.parse("T2 <=> A & B & C & K"));
- solver.add(f.parse("T1 + T2 = 1"));
+ solver.add(parse(f, "X => Y"));
+ solver.add(parse(f, "X => Z"));
+ solver.add(parse(f, "C => E"));
+ solver.add(parse(f, "D => ~F"));
+ solver.add(parse(f, "B => M"));
+ solver.add(parse(f, "D => N"));
+ solver.add(parse(f, "G => O"));
+ solver.add(parse(f, "A => B"));
+ solver.add(parse(f, "T1 <=> A & K & ~B & ~C"));
+ solver.add(parse(f, "T2 <=> A & B & C & K"));
+ solver.add(parse(f, "T1 + T2 = 1"));
solver.sat(); // required for DRUP issue
- solver.add(f.parse("Y => ~X & D"));
- solver.add(f.parse("X"));
+ solver.add(parse(f, "Y => ~X & D"));
+ solver.add(parse(f, "X"));
solver.sat();
assertThat(solver.unsatCore()).isNotNull();
@@ -322,35 +322,35 @@ public void testCoreAndAssumptions3() throws ParserException {
}
@Test
- public void testCoreAndAssumptions4() throws ParserException {
+ public void testCoreAndAssumptions4() {
final SATSolver[] solvers = new SATSolver[]{
MiniSat.miniSat(this.f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()),
MiniSat.glucose(this.f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build())
};
for (final SATSolver solver : solvers) {
- solver.add(this.f.parse("~X1"));
+ solver.add(parse(this.f, "~X1"));
solver.sat(this.f.variable("X1")); // caused the bug
solver.add(this.f.variable("A1"));
- solver.add(this.f.parse("A1 => A2"));
- solver.add(this.f.parse("R & A2 => A3"));
- solver.add(this.f.parse("L & A2 => A3"));
- solver.add(this.f.parse("R & A3 => A4"));
- solver.add(this.f.parse("L & A3 => A4"));
- solver.add(this.f.parse("~A4"));
- solver.add(this.f.parse("L | R"));
+ solver.add(parse(this.f, "A1 => A2"));
+ solver.add(parse(this.f, "R & A2 => A3"));
+ solver.add(parse(this.f, "L & A2 => A3"));
+ solver.add(parse(this.f, "R & A3 => A4"));
+ solver.add(parse(this.f, "L & A3 => A4"));
+ solver.add(parse(this.f, "~A4"));
+ solver.add(parse(this.f, "L | R"));
solver.sat();
assertThat(solver.unsatCore()).isNotNull();
}
}
@Test
- public void testWithCcPropositions() throws ParserException {
+ public void testWithCcPropositions() {
final FormulaFactory f = new FormulaFactory();
final SATSolver solver = MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
- final ExtendedProposition p1 = new ExtendedProposition<>(new StringBackpack("CC"), f.parse("A + B + C <= 1"));
- final StandardProposition p2 = new StandardProposition(f.parse("A"));
- final StandardProposition p3 = new StandardProposition(f.parse("B"));
- final StandardProposition p4 = new StandardProposition(f.parse("X & Y"));
+ final ExtendedProposition p1 = new ExtendedProposition<>(new StringBackpack("CC"), parse(f, "A + B + C <= 1"));
+ final StandardProposition p2 = new StandardProposition(parse(f, "A"));
+ final StandardProposition p3 = new StandardProposition(parse(f, "B"));
+ final StandardProposition p4 = new StandardProposition(parse(f, "X & Y"));
solver.add(p1);
solver.add(p2);
solver.add(p3);
@@ -360,20 +360,20 @@ public void testWithCcPropositions() throws ParserException {
}
@Test
- public void testWithSpecialUnitCaseMiniSat() throws ParserException {
+ public void testWithSpecialUnitCaseMiniSat() {
final FormulaFactory f = new FormulaFactory();
final SATSolver solver = MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).build());
- final StandardProposition p1 = new StandardProposition(f.parse("a => b"));
- final StandardProposition p2 = new StandardProposition(f.parse("a => c | d"));
- final StandardProposition p3 = new StandardProposition(f.parse("b => c | d"));
- final StandardProposition p4 = new StandardProposition(f.parse("e | f | g | h => i"));
- final StandardProposition p5 = new StandardProposition(f.parse("~j => k | j"));
- final StandardProposition p6 = new StandardProposition(f.parse("b => ~(e | f)"));
- final StandardProposition p7 = new StandardProposition(f.parse("c => ~j"));
- final StandardProposition p8 = new StandardProposition(f.parse("l | m => ~i"));
- final StandardProposition p9 = new StandardProposition(f.parse("j => (f + g + h = 1)"));
- final StandardProposition p10 = new StandardProposition(f.parse("d => (l + m + e + f = 1)"));
- final StandardProposition p11 = new StandardProposition(f.parse("~k"));
+ final StandardProposition p1 = new StandardProposition(parse(f, "a => b"));
+ final StandardProposition p2 = new StandardProposition(parse(f, "a => c | d"));
+ final StandardProposition p3 = new StandardProposition(parse(f, "b => c | d"));
+ final StandardProposition p4 = new StandardProposition(parse(f, "e | f | g | h => i"));
+ final StandardProposition p5 = new StandardProposition(parse(f, "~j => k | j"));
+ final StandardProposition p6 = new StandardProposition(parse(f, "b => ~(e | f)"));
+ final StandardProposition p7 = new StandardProposition(parse(f, "c => ~j"));
+ final StandardProposition p8 = new StandardProposition(parse(f, "l | m => ~i"));
+ final StandardProposition p9 = new StandardProposition(parse(f, "j => (f + g + h = 1)"));
+ final StandardProposition p10 = new StandardProposition(parse(f, "d => (l + m + e + f = 1)"));
+ final StandardProposition p11 = new StandardProposition(parse(f, "~k"));
solver.addPropositions(p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11);
assertThat(solver.sat()).isEqualTo(TRUE);
solver.add(f.variable("a"));
@@ -382,20 +382,20 @@ public void testWithSpecialUnitCaseMiniSat() throws ParserException {
}
@Test
- public void testWithSpecialUnitCaseGlucose() throws ParserException {
+ public void testWithSpecialUnitCaseGlucose() {
final FormulaFactory f = new FormulaFactory();
final SATSolver solver = MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).build(), GlucoseConfig.builder().build());
- final StandardProposition p1 = new StandardProposition(f.parse("a => b"));
- final StandardProposition p2 = new StandardProposition(f.parse("a => c | d"));
- final StandardProposition p3 = new StandardProposition(f.parse("b => c | d"));
- final StandardProposition p4 = new StandardProposition(f.parse("e | f | g | h => i"));
- final StandardProposition p5 = new StandardProposition(f.parse("~j => k | j"));
- final StandardProposition p6 = new StandardProposition(f.parse("b => ~(e | f)"));
- final StandardProposition p7 = new StandardProposition(f.parse("c => ~j"));
- final StandardProposition p8 = new StandardProposition(f.parse("l | m => ~i"));
- final StandardProposition p9 = new StandardProposition(f.parse("j => (f + g + h = 1)"));
- final StandardProposition p10 = new StandardProposition(f.parse("d => (l + m + e + f = 1)"));
- final StandardProposition p11 = new StandardProposition(f.parse("~k"));
+ final StandardProposition p1 = new StandardProposition(parse(f, "a => b"));
+ final StandardProposition p2 = new StandardProposition(parse(f, "a => c | d"));
+ final StandardProposition p3 = new StandardProposition(parse(f, "b => c | d"));
+ final StandardProposition p4 = new StandardProposition(parse(f, "e | f | g | h => i"));
+ final StandardProposition p5 = new StandardProposition(parse(f, "~j => k | j"));
+ final StandardProposition p6 = new StandardProposition(parse(f, "b => ~(e | f)"));
+ final StandardProposition p7 = new StandardProposition(parse(f, "c => ~j"));
+ final StandardProposition p8 = new StandardProposition(parse(f, "l | m => ~i"));
+ final StandardProposition p9 = new StandardProposition(parse(f, "j => (f + g + h = 1)"));
+ final StandardProposition p10 = new StandardProposition(parse(f, "d => (l + m + e + f = 1)"));
+ final StandardProposition p11 = new StandardProposition(parse(f, "~k"));
solver.addPropositions(p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11);
assertThat(solver.sat()).isEqualTo(TRUE);
solver.add(f.variable("a"));
diff --git a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java
index d2553b85..e4a24068 100644
--- a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java
+++ b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java
@@ -29,8 +29,16 @@
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 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,200 +48,225 @@
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() throws ParserException {
+ public static Collection configs() {
+ final List configs = new ArrayList<>();
+ configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"});
+ configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_INCWBO, null, null), "INCWBO"});
+ configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"});
+ configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"});
+ configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"});
+ configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"});
+ configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_WBO, null, null), "WBO"});
+ return configs;
+ }
+
+ @ParameterizedTest
+ @MethodSource("configs")
+ public void testFromPaper(final OptimizationConfig cfg) {
final List
