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 4a2dea46..9b0f0e0a 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java @@ -32,12 +32,13 @@ import org.logicng.formulas.Variable; import org.logicng.knowledgecompilation.dnnf.functions.DnnfFunction; +import java.util.Objects; import java.util.SortedSet; /** * A DNNF - Decomposable Negation Normal Form. * @version 2.0.0 - * @since 2.0.0 + * @since 2.5.0 */ public final class Dnnf { @@ -79,4 +80,21 @@ public Formula formula() { public SortedSet getOriginalVariables() { return this.originalVariables; } + + @Override + public boolean equals(final Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + final Dnnf dnnf = (Dnnf) o; + return Objects.equals(this.originalVariables, dnnf.originalVariables) && Objects.equals(this.formula, dnnf.formula); + } + + @Override + public int hashCode() { + return Objects.hash(this.originalVariables, this.formula); + } } diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelEnumerationFunction.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelEnumerationFunction.java index 0f79053f..fd5cf16b 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelEnumerationFunction.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelEnumerationFunction.java @@ -29,26 +29,40 @@ package org.logicng.knowledgecompilation.dnnf.functions; import static java.util.Collections.emptyList; -import static java.util.Collections.emptySet; import static java.util.Collections.singleton; import org.logicng.datastructures.Assignment; import org.logicng.formulas.Formula; import org.logicng.formulas.Literal; import org.logicng.formulas.Variable; +import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; +import org.logicng.util.CollectionHelper; +import org.logicng.util.Pair; import java.util.ArrayList; import java.util.Arrays; +import java.util.BitSet; import java.util.Collection; +import java.util.HashMap; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; import java.util.stream.Collectors; /** - * A DNNF function which counts models. + * A DNNF function for (projected) model enumeration. + *

+ * This function does not require a deterministic DNNF. + *

+ * The enumeration requires a set of variables which the formula is projected + * to. Variables which are not known by the DNNF will be added negatively to + * all models. + *

+ * Note that an enumeration over {@code n} variables can have up to {@code 2^n} + * models, so the number of variables must be chosen carefully. * @version 2.5.0 * @since 2.5.0 */ @@ -56,48 +70,62 @@ public final class DnnfModelEnumerationFunction implements DnnfFunction variables; + /** + * Creates a new DNNF model enumeration function over the given set of + * variables. + * @param variables the variables, must not be {@code null} + */ public DnnfModelEnumerationFunction(final Collection variables) { - this.variables = variables == null ? null : new TreeSet<>(variables); + this.variables = new TreeSet<>(variables); } @Override public List apply(final SortedSet originalVariables, final Formula formula) { - final Formula projectedFormula = this.variables == null ? formula : new DnnfProjectionFunction(this.variables).apply(originalVariables, formula).formula(); - final Set> partialModels = applyRec(projectedFormula); - final SortedSet globalDontCares = originalVariables.stream() - .filter(v -> !formula.variables().contains(v) && (this.variables == null || this.variables.contains(v))) + final Dnnf projectedDnnf = this.variables.equals(originalVariables) + ? new Dnnf(this.variables, formula) + : new DnnfProjectionFunction(this.variables).apply(originalVariables, formula); + final Formula projectedFormula = projectedDnnf.formula(); + final SortedSet projectedVariables = projectedDnnf.getOriginalVariables(); + final Pair, Map> mapping = createVarMapping(projectedVariables); + final List intToVar = mapping.first(); + final Map varToInt = mapping.second(); + + final Set partialModels = computePartialModels(projectedFormula, varToInt); + + final SortedSet globalDontCares = projectedVariables.stream() + .filter(v -> !projectedFormula.variables().contains(v)) .collect(Collectors.toCollection(TreeSet::new)); - final List invalidVars = this.variables == null - ? emptyList() - : this.variables.stream().filter(v -> !originalVariables.contains(v)).collect(Collectors.toList()); - final Set> partialDontCareModels = getCartesianProduct(globalDontCares); - final Set> partialModelsWithGlobalDontCares = combineDisjointModels(Arrays.asList(partialModels, partialDontCareModels)); - final Set> result = expandModelsWithMissingVars(partialModelsWithGlobalDontCares, this.variables); - addInvalidVars(result, invalidVars); - final List resultAssignments = new ArrayList<>(); - for (final Set model : result) { - resultAssignments.add(new Assignment(model)); - } - return resultAssignments; + final Set partialDontCareModels = getCartesianProduct(globalDontCares.stream().map(varToInt::get).collect(Collectors.toList()), projectedVariables.size()); + final Set partialModelsWithGlobalDontCares = combineDisjointModels(Arrays.asList(partialModels, partialDontCareModels)); + + final Set expandedModels = expandModelsWithMissingVars(partialModelsWithGlobalDontCares, projectedVariables.size()); + + final SortedSet invalidVars = CollectionHelper.difference(this.variables, originalVariables, TreeSet::new); + return translateBitSetsToAssignments(expandedModels, intToVar, invalidVars); } - private Set> applyRec(final Formula formula) { + private static Set computePartialModels(final Formula formula, final Map varToInt) { switch (formula.type()) { case FALSE: return new HashSet<>(); - case LITERAL: case TRUE: - return singleton(formula.literals()); + return singleton(new BitSet(varToInt.size() * 2)); + case LITERAL: + final BitSet newBitSet = new BitSet(varToInt.size() * 2); + for (final Literal lit : formula.literals()) { + newBitSet.set(2 * varToInt.get(lit.variable()) + (lit.phase() ? 0 : 1)); + } + return singleton(newBitSet); case AND: - final List>> opResults = new ArrayList<>(); + final List> opResults = new ArrayList<>(); for (final Formula op : formula) { - opResults.add(applyRec(op)); + opResults.add(computePartialModels(op, varToInt)); } return combineDisjointModels(opResults); case OR: - final Set> allModels = new HashSet<>(); + final Set allModels = new HashSet<>(); for (final Formula op : formula) { - allModels.addAll(applyRec(op)); + allModels.addAll(computePartialModels(op, varToInt)); } return allModels; default: @@ -105,27 +133,47 @@ private Set> applyRec(final Formula formula) { } } - private Set> expandModelsWithMissingVars(final Set> partialModels, final SortedSet allVariables) { - final Set> result = new HashSet<>(); - for (final Set partialModel : partialModels) { - final Set missingVariables = new HashSet<>(allVariables); - for (final Literal lit : partialModel) { - missingVariables.remove(lit.variable()); - } + private static Set expandModelsWithMissingVars(final Set partialModels, final int numVars) { + final Set result = new HashSet<>(); + for (final BitSet partialModel : partialModels) { + final List missingVariables = findMissingVars(partialModel, numVars); if (missingVariables.isEmpty()) { result.add(partialModel); } else { - result.addAll(combineDisjointModels(Arrays.asList(singleton(partialModel), getCartesianProduct(missingVariables)))); + result.addAll(combineDisjointModels(Arrays.asList(singleton(partialModel), getCartesianProduct(missingVariables, numVars)))); } } return result; } - private static void addInvalidVars(final Set> models, final List invalidVars) { - final List negated = invalidVars.stream().map(Variable::negate).collect(Collectors.toList()); - for (final Set model : models) { - model.addAll(negated); + private static List findMissingVars(final BitSet partialModel, final int numVars) { + final int cardinality = partialModel.cardinality(); + if (cardinality == numVars) { + return emptyList(); } + final List missing = new ArrayList<>(numVars - cardinality); + for (int i = 0; i < numVars; i++) { + if (!partialModel.get(2 * i) && !partialModel.get(2 * i + 1)) { + missing.add(i); + } + } + return missing; + } + + private static List translateBitSetsToAssignments(final Set models, final List intToVar, final SortedSet invalidVars) { + final List result = new ArrayList<>(models.size()); + for (final BitSet model : models) { + final Assignment assignment = new Assignment(); + for (int i = model.nextSetBit(0); i >= 0; i = model.nextSetBit(i + 1)) { + final Variable variable = intToVar.get(i / 2); + assignment.addLiteral(i % 2 == 0 ? variable : variable.negate()); + } + for (final Variable invalidVar : invalidVars) { + assignment.addLiteral(invalidVar.negate()); + } + result.add(assignment); + } + return result; } /** @@ -141,14 +189,14 @@ private static void addInvalidVars(final Set> models, final List> combineDisjointModels(final List>> modelLists) { - Set> currentModels = modelLists.get(0); + private static Set combineDisjointModels(final List> modelLists) { + Set currentModels = modelLists.get(0); for (int i = 1; i < modelLists.size(); i++) { - final Set> additionalModels = modelLists.get(i); - final Set> newModels = new HashSet<>(); - for (final Set currentModel : currentModels) { - for (final Set additionalModel : additionalModels) { - newModels.add(setAdd(currentModel, additionalModel)); + final Set additionalModels = modelLists.get(i); + final Set newModels = new HashSet<>(); + for (final BitSet currentModel : currentModels) { + for (final BitSet additionalModel : additionalModels) { + newModels.add(combineBitSets(currentModel, additionalModel)); } } currentModels = newModels; @@ -156,6 +204,12 @@ private static Set> combineDisjointModels(final List> combineDisjointModels(final List> getCartesianProduct(final Collection variables) { - Set> result = singleton(emptySet()); - for (final Variable var : variables) { - final Set> extended = new HashSet<>(result.size() * 2); - for (final Set literals : result) { - extended.add(extendedByLiteral(literals, var)); - extended.add(extendedByLiteral(literals, var.negate())); + private static Set getCartesianProduct(final Collection variables, final int numVars) { + Set result = singleton(new BitSet(numVars * 2)); + for (final int var : variables) { + final Set extended = new HashSet<>(result.size() * 2); + for (final BitSet current : result) { + extended.add(extendedByLiteral(current, 2 * var)); + extended.add(extendedByLiteral(current, 2 * var + 1)); } result = extended; } return result; } - private static Set extendedByLiteral(final Set literals, final Literal lit) { - final Set extended = new HashSet<>(literals); - extended.add(lit); + private static BitSet extendedByLiteral(final BitSet current, final int lit) { + final BitSet extended = (BitSet) current.clone(); + extended.set(lit); return extended; } - private static Set setAdd(final Set first, final Set second) { - final Set result = new HashSet<>(); - result.addAll(first); - result.addAll(second); - return result; + private static Pair, Map> createVarMapping(final SortedSet originalVariables) { + final List intToVariable = new ArrayList<>(originalVariables); + final Map variableToInt = new HashMap<>(); + for (int i = 0; i < intToVariable.size(); i++) { + variableToInt.put(intToVariable.get(i), i); + } + return new Pair<>(intToVariable, variableToInt); } } diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfProjectionFunction.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfProjectionFunction.java index 49113236..7f2635f9 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfProjectionFunction.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfProjectionFunction.java @@ -32,15 +32,22 @@ import org.logicng.formulas.Literal; import org.logicng.formulas.Variable; import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; +import org.logicng.util.CollectionHelper; import java.util.ArrayList; import java.util.Collection; +import java.util.HashMap; import java.util.List; +import java.util.Map; import java.util.SortedSet; import java.util.TreeSet; /** - * A DNNF function which counts models. + * A DNNF function which projects the DNNF to a given set of variables. + *

+ * Not the resulting DNNF does NOT have deterministic property, and + * thus, it must not be used for model counting or other DNNF operations + * requiring a d-DNNF. * @version 2.5.0 * @since 2.5.0 */ @@ -48,36 +55,52 @@ public final class DnnfProjectionFunction implements DnnfFunction { private final SortedSet variables; + /** + * Creates a new DNNF function to project a DNNF to the given set of + * variables. + * @param variables the variables to project to + */ public DnnfProjectionFunction(final Collection variables) { this.variables = new TreeSet<>(variables); } @Override public Dnnf apply(final SortedSet originalVariables, final Formula formula) { - return new Dnnf(originalVariables, applyRec(formula)); + return new Dnnf(CollectionHelper.intersection(this.variables, originalVariables, TreeSet::new), applyRec(formula, new HashMap<>())); } - private Formula applyRec(final Formula formula) { + private Formula applyRec(final Formula formula, final Map cache) { + final Formula cached = cache.get(formula); + if (cached != null) { + return cached; + } + final Formula result; switch (formula.type()) { case TRUE: case FALSE: - return formula; + result = formula; + break; case LITERAL: - return this.variables.contains(((Literal) formula).variable()) ? formula : formula.factory().verum(); + result = this.variables.contains(((Literal) formula).variable()) ? formula : formula.factory().verum(); + break; case OR: final List newOrOps = new ArrayList<>(); for (final Formula op : formula) { - newOrOps.add(applyRec(op)); + newOrOps.add(applyRec(op, cache)); } - return formula.factory().or(newOrOps); + result = formula.factory().or(newOrOps); + break; case AND: final List newAndOps = new ArrayList<>(); for (final Formula op : formula) { - newAndOps.add(applyRec(op)); + newAndOps.add(applyRec(op, cache)); } - return formula.factory().and(newAndOps); + result = formula.factory().and(newAndOps); + break; default: throw new IllegalArgumentException("Unexpected formula type: " + formula.type()); } + cache.put(formula, result); + return result; } } diff --git a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfModelEnumerationTest.java b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfModelEnumerationTest.java index 78947638..03a09a14 100644 --- a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfModelEnumerationTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfModelEnumerationTest.java @@ -1,59 +1,154 @@ package org.logicng.knowledgecompilation.dnnf; +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 org.logicng.LongRunningTag; +import org.logicng.RandomTag; +import org.logicng.TestWithExampleFormulas; import org.logicng.datastructures.Assignment; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; +import org.logicng.formulas.Literal; import org.logicng.formulas.Variable; +import org.logicng.handlers.NumberOfModelsHandler; import org.logicng.io.parsers.ParserException; -import org.logicng.io.readers.DimacsReader; import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; import org.logicng.knowledgecompilation.dnnf.functions.DnnfModelEnumerationFunction; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; import org.logicng.solvers.functions.ModelEnumerationFunction; +import org.logicng.util.CollectionHelper; +import org.logicng.util.FormulaRandomizer; +import org.logicng.util.FormulaRandomizerConfig; import java.io.IOException; import java.util.ArrayList; +import java.util.Collection; import java.util.Collections; import java.util.List; -import java.util.Random; +import java.util.SortedSet; +import java.util.TreeSet; +import java.util.stream.Collectors; +import java.util.stream.IntStream; -public class DnnfModelEnumerationTest { +public class DnnfModelEnumerationTest extends TestWithExampleFormulas { - private final FormulaFactory f = new FormulaFactory(); + @Test + public void testCornerCases() throws ParserException, IOException { + final Formula contradiction = this.f.parse("(A | B) & ~A & ~B"); + compareModels(this.f.verum(), Collections.emptyList(), 1); + compareModels(this.A, Collections.emptyList(), 1); + compareModels(this.AND1, Collections.emptyList(), 1); + compareModels(contradiction, Collections.emptyList(), 0); + compareModels(this.f.falsum(), Collections.emptyList(), 0); + + compareModels(this.A, Collections.singletonList(this.A), 1); + compareModels(this.AND1, Collections.singletonList(this.A), 1); + compareModels(this.NA, Collections.singletonList(this.A), 1); + compareModels(this.AND2, Collections.singletonList(this.A), 1); + compareModels(contradiction, Collections.singletonList(this.A), 0); + + // Dnnf Model Enumeration adds unknown variables negatively, Solver Model enumeration ignores them + compareModelsDnnfOnly(this.f.verum(), Collections.singletonList(this.A), 1); + compareModelsDnnfOnly(this.A, Collections.singletonList(this.C), 1); + compareModelsDnnfOnly(this.AND1, Collections.singletonList(this.C), 1); + compareModelsDnnfOnly(this.NA, Collections.singletonList(this.C), 1); + compareModelsDnnfOnly(this.AND2, Collections.singletonList(this.C), 1); + compareModelsDnnfOnly(contradiction, Collections.singletonList(this.C), 0); + compareModelsDnnfOnly(this.f.falsum(), Collections.singletonList(this.A), 0); + } @Test - public void test() throws ParserException, IOException { - final Formula formula = this.f.and(DimacsReader.readCNF("src/test/resources/dnnf/both_bdd_dnnf_1.cnf", this.f)); - final Random random = new Random(42); - for (int i = 0; i < 10; i++) { - final List shuffledVars = new ArrayList<>(formula.variables()); - Collections.shuffle(shuffledVars, random); - final List vars = shuffledVars.subList(0, 30); - final long startDnnfComp = System.currentTimeMillis(); - final DnnfFactory dnnfFactory = new DnnfFactory(); - final Dnnf dnnf = dnnfFactory.compile(formula); - final long endDnnfComp = System.currentTimeMillis(); - System.out.printf("Dnnf Compilation: %5dms%n", endDnnfComp - startDnnfComp); - final List dnnfModels = dnnf.execute(new DnnfModelEnumerationFunction(vars)); - final long endDnnfEnum = System.currentTimeMillis(); - System.out.printf("Dnnf Enumeration: %5dms%n", endDnnfEnum - endDnnfComp); - final List solverModels = enumerateWithSolver(formula, vars); - final long endSolverEnum = System.currentTimeMillis(); - System.out.printf("Solver Enumeration: %5dms%n", endSolverEnum - endDnnfEnum); -// assertThat(dnnfModels).containsExactlyInAnyOrderElementsOf(solverModels); - assertThat(dnnfModels).hasSameSizeAs(solverModels); - System.out.println("Models: " + dnnfModels.size()); - System.out.println(); + @RandomTag + @LongRunningTag + public void randomTests() { + for (int i = 0; i < 100; i++) { + final FormulaFactory f = new FormulaFactory(); + final FormulaRandomizerConfig config = FormulaRandomizerConfig.builder() + .numVars(12) + .weightAmo(5) + .weightExo(5) + .seed((i + 1) * 42).build(); + final FormulaRandomizer randomizer = new FormulaRandomizer(f, config); + + Formula formula; + do { + formula = f.and(IntStream.range(1, 5).mapToObj(j -> randomizer.formula(4)).collect(Collectors.toList())); + } while (!hasMoreThanOneModel(formula)); + compareModels(formula, formula.variables()); } } - private List enumerateWithSolver(final Formula formula, final List vars) { + private void compareModels(final Formula formula, final Collection vars) { + compareModels(formula, vars, null); + } + + private void compareModels(final Formula formula, final Collection vars, final Integer expectedSize) { + final List solverModels = enumerateWithSolver(formula, vars); + final List dnnfModels = enumerateWithDnnf(formula, vars); + if (expectedSize != null) { + assertThat(dnnfModels).hasSize(expectedSize); + } + assertThat(dnnfModels).containsExactlyInAnyOrderElementsOf(solverModels); + } + + private void compareModelsDnnfOnly(final Formula formula, final List vars, final Integer expectedSize) { + final List dnnfModels = enumerateWithDnnf(formula, vars); + assertThat(dnnfModels).hasSize(expectedSize); + } + + private List enumerateWithSolver(final Formula formula, final Collection vars) { + final SATSolver solver = MiniSat.miniSat(this.f); + solver.add(formula); + final List result = solver.execute(ModelEnumerationFunction.builder().variables(vars).build()); + final SortedSet missingVars = CollectionHelper.difference(vars, solver.knownVariables(), TreeSet::new); + return missingVars.isEmpty() ? result : fixSolverModels(result, missingVars); + } + + private List enumerateWithDnnf(final Formula formula, final Collection vars) { + final DnnfFactory dnnfFactory = new DnnfFactory(); + final Dnnf dnnf = dnnfFactory.compile(formula); + return dnnf.execute(new DnnfModelEnumerationFunction(vars)); + } + + private boolean hasMoreThanOneModel(final Formula formula) { final SATSolver solver = MiniSat.miniSat(this.f); solver.add(formula); - return solver.execute(ModelEnumerationFunction.builder().variables(vars).build()); + final List result = solver.execute(ModelEnumerationFunction.builder().variables(formula.variables()).handler(new NumberOfModelsHandler(3)).build()); + return result.size() >= 2; + } + + private List fixSolverModels(final List assignments, final SortedSet missingVars) { + final List result = new ArrayList<>(); + for (final List additional : getCartesianProduct(missingVars)) { + for (final Assignment assignment : assignments) { + final Assignment newAssignment = new Assignment(assignment.literals()); + additional.forEach(newAssignment::addLiteral); + result.add(newAssignment); + } + } + return result; + } + + static List> getCartesianProduct(final SortedSet variables) { + List> result = singletonList(emptyList()); + for (final Variable var : variables) { + final List> extended = new ArrayList<>(result.size() * 2); + for (final List literals : result) { + extended.add(extendedByLiteral(literals, var)); + extended.add(extendedByLiteral(literals, var.negate())); + } + result = extended; + } + return result; + } + + private static List extendedByLiteral(final List literals, final Literal lit) { + final ArrayList extended = new ArrayList<>(literals); + extended.add(lit); + return extended; } } diff --git a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfProjectionFunctionTest.java b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfProjectionFunctionTest.java new file mode 100644 index 00000000..e5706bc4 --- /dev/null +++ b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfProjectionFunctionTest.java @@ -0,0 +1,49 @@ +package org.logicng.knowledgecompilation.dnnf; + +import static org.assertj.core.api.Assertions.assertThat; + +import org.junit.jupiter.api.Test; +import org.logicng.formulas.Formula; +import org.logicng.formulas.FormulaFactory; +import org.logicng.formulas.Variable; +import org.logicng.io.parsers.ParserException; +import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; +import org.logicng.knowledgecompilation.dnnf.functions.DnnfProjectionFunction; +import org.logicng.util.CollectionHelper; + +import java.util.Arrays; +import java.util.Collections; +import java.util.SortedSet; +import java.util.TreeSet; + +public class DnnfProjectionFunctionTest { + + @Test + public void test() throws ParserException { + final FormulaFactory f = new FormulaFactory(); + final Formula formula = f.parse("((A1 | ~A2 & A3) & (~B1 & B2 | ~B3 | B4) | (~A1 | A2 | A4 & ~A5) & B1) " + + "& ((C1 & C2 | ~C1 & C3 | C4) & (D1 | D2 | D3) | (~C1 | ~C2) & (D1 | D2 & D3))"); + final Dnnf dnnf = new Dnnf(formula.variables(), formula); + + final Dnnf projectAll = dnnf.execute(new DnnfProjectionFunction(formula.variables())); + assertThat(projectAll).isEqualTo(dnnf); + + final Dnnf projectNone = dnnf.execute(new DnnfProjectionFunction(Collections.emptyList())); + assertThat(projectNone).isEqualTo(new Dnnf(Collections.emptySortedSet(), f.verum())); + + final SortedSet elimA1Vars = CollectionHelper.difference(formula.variables(), Collections.singletonList(f.variable("A1")), TreeSet::new); + final Dnnf elimA1 = dnnf.execute(new DnnfProjectionFunction(elimA1Vars)); + assertThat(elimA1).isEqualTo(new Dnnf(elimA1Vars, f.parse("(~B1 & B2 | ~B3 | B4 | B1) " + + "& ((C1 & C2 | ~C1 & C3 | C4) & (D1 | D2 | D3) | (~C1 | ~C2) & (D1 | D2 & D3))"))); + + final SortedSet elimA2C1Vars = CollectionHelper.difference(formula.variables(), Arrays.asList(f.variable("A2"), f.variable("C1")), TreeSet::new); + final Dnnf elimA2C1 = dnnf.execute(new DnnfProjectionFunction(elimA2C1Vars)); + assertThat(elimA2C1).isEqualTo(new Dnnf(elimA2C1Vars, f.parse("((A1 | A3) & (~B1 & B2 | ~B3 | B4) | B1) " + + "& ((C2 | C3 | C4) & (D1 | D2 | D3) | (D1 | D2 & D3))"))); + + final SortedSet elimA3B3C4D2Vars = CollectionHelper.difference(formula.variables(), + Arrays.asList(f.variable("A3"), f.variable("B3"), f.variable("C4"), f.variable("D2")), TreeSet::new); + final Dnnf elimA3B3C4D2 = dnnf.execute(new DnnfProjectionFunction(elimA3B3C4D2Vars)); + assertThat(elimA3B3C4D2).isEqualTo(new Dnnf(elimA3B3C4D2Vars, f.parse("((A1 | ~A2) | (~A1 | A2 | A4 & ~A5) & B1)"))); + } +}