diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelEnumerationFunction.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelEnumerationFunction.java new file mode 100644 index 00000000..0f79053f --- /dev/null +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelEnumerationFunction.java @@ -0,0 +1,191 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +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 java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeSet; +import java.util.stream.Collectors; + +/** + * A DNNF function which counts models. + * @version 2.5.0 + * @since 2.5.0 + */ +public final class DnnfModelEnumerationFunction implements DnnfFunction> { + + private final SortedSet variables; + + public DnnfModelEnumerationFunction(final Collection variables) { + this.variables = variables == null ? null : 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))) + .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; + } + + private Set> applyRec(final Formula formula) { + switch (formula.type()) { + case FALSE: + return new HashSet<>(); + case LITERAL: + case TRUE: + return singleton(formula.literals()); + case AND: + final List>> opResults = new ArrayList<>(); + for (final Formula op : formula) { + opResults.add(applyRec(op)); + } + return combineDisjointModels(opResults); + case OR: + final Set> allModels = new HashSet<>(); + for (final Formula op : formula) { + allModels.addAll(applyRec(op)); + } + return allModels; + default: + throw new IllegalArgumentException("Unexpected formula type: " + formula.type()); + } + } + + 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()); + } + if (missingVariables.isEmpty()) { + result.add(partialModel); + } else { + result.addAll(combineDisjointModels(Arrays.asList(singleton(partialModel), getCartesianProduct(missingVariables)))); + } + } + 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); + } + } + + /** + * Combines a list of a model-sets (a model-set is a set of models). + * The variables of the model-sets in the list must be disjoint + * (i.e. a variable in a model-set must not occur in any other + * model-set, but it will usually, but not necessarily, occur + * in all models of the model-set). + *

+ * Basically the models of each model-set are combined with every + * other model of the other set. Since the variables are disjoint, + * the models can just be combined into one model for each combination. + * @param modelLists the list of sets of models + * @return the combined model-set list + */ + 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)); + } + } + currentModels = newModels; + } + return currentModels; + } + + /** + * Returns the Cartesian product for the given variables, i.e. all + * combinations of literals are generated with each variable occurring + * positively and negatively. + * @param variables the variables, must not be {@code null} + * @return the Cartesian product + */ + private static Set> 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())); + } + result = extended; + } + return result; + } + + private static Set extendedByLiteral(final Set literals, final Literal lit) { + final Set extended = new HashSet<>(literals); + extended.add(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; + } +} diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfProjectionFunction.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfProjectionFunction.java new file mode 100644 index 00000000..49113236 --- /dev/null +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfProjectionFunction.java @@ -0,0 +1,83 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.knowledgecompilation.dnnf.functions; + +import org.logicng.formulas.Formula; +import org.logicng.formulas.Literal; +import org.logicng.formulas.Variable; +import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import java.util.SortedSet; +import java.util.TreeSet; + +/** + * A DNNF function which counts models. + * @version 2.5.0 + * @since 2.5.0 + */ +public final class DnnfProjectionFunction implements DnnfFunction { + + private final SortedSet variables; + + 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)); + } + + private Formula applyRec(final Formula formula) { + switch (formula.type()) { + case TRUE: + case FALSE: + return formula; + case LITERAL: + return this.variables.contains(((Literal) formula).variable()) ? formula : formula.factory().verum(); + case OR: + final List newOrOps = new ArrayList<>(); + for (final Formula op : formula) { + newOrOps.add(applyRec(op)); + } + return formula.factory().or(newOrOps); + case AND: + final List newAndOps = new ArrayList<>(); + for (final Formula op : formula) { + newAndOps.add(applyRec(op)); + } + return formula.factory().and(newAndOps); + default: + throw new IllegalArgumentException("Unexpected formula type: " + formula.type()); + } + } +} diff --git a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfModelEnumerationTest.java b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfModelEnumerationTest.java new file mode 100644 index 00000000..78947638 --- /dev/null +++ b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfModelEnumerationTest.java @@ -0,0 +1,59 @@ +package org.logicng.knowledgecompilation.dnnf; + +import static org.assertj.core.api.Assertions.assertThat; + +import org.junit.jupiter.api.Test; +import org.logicng.datastructures.Assignment; +import org.logicng.formulas.Formula; +import org.logicng.formulas.FormulaFactory; +import org.logicng.formulas.Variable; +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 java.io.IOException; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; +import java.util.Random; + +public class DnnfModelEnumerationTest { + + private final FormulaFactory f = new FormulaFactory(); + + @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(); + } + } + + private List enumerateWithSolver(final Formula formula, final List vars) { + final SATSolver solver = MiniSat.miniSat(this.f); + solver.add(formula); + return solver.execute(ModelEnumerationFunction.builder().variables(vars).build()); + } +}