From 87da23b9c1458dbd728b8385c2271e5eaa2912e0 Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Fri, 15 Mar 2024 17:02:34 +0100 Subject: [PATCH] added possibility to pass a DNNF handler to the model counter --- CHANGELOG.md | 1 + .../logicng/modelcounting/ModelCounter.java | 33 +++++++++++++++++-- .../modelcounting/ModelCounterTest.java | 27 +++++++++++++++ 3 files changed, 58 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7e495903..60568f49 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - Class `UBTree` offers new method `generateSubsumedUBTree` to directly generate a subsumed UBTree for the given sets. - The `DnnfFactory` now offers a method to compile a DNNF with a `DnnfCompilationHandler` +- The `ModelCounter` now offers a method to pass a `DnnfCompilationHandler` in order to control long-running computations ### Changed 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/test/java/org/logicng/modelcounting/ModelCounterTest.java b/src/test/java/org/logicng/modelcounting/ModelCounterTest.java index f735a2f4..f74ef892 100644 --- a/src/test/java/org/logicng/modelcounting/ModelCounterTest.java +++ b/src/test/java/org/logicng/modelcounting/ModelCounterTest.java @@ -41,7 +41,9 @@ import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.PBConstraint; import org.logicng.formulas.Variable; +import org.logicng.handlers.DnnfCompilationHandler; import org.logicng.io.parsers.ParserException; +import org.logicng.io.readers.DimacsReader; import org.logicng.knowledgecompilation.bdds.orderings.VariableOrdering; import org.logicng.solvers.MiniSat; import org.logicng.testutils.NQueensGenerator; @@ -51,6 +53,7 @@ import org.logicng.util.FormulaRandomizer; import org.logicng.util.FormulaRandomizerConfig; +import java.io.IOException; import java.math.BigInteger; import java.util.Arrays; import java.util.Collections; @@ -164,6 +167,16 @@ public void testCornerCases() { } } + @Test + public void testCompilationHandler() throws IOException { + final FormulaFactory f = new FormulaFactory(); + final Formula formula = f.and(DimacsReader.readCNF("src/test/resources/dnnf/both_bdd_dnnf_1.cnf", f)); + final BigInteger countSuccessful = ModelCounter.count(Collections.singletonList(formula), formula.variables(), () -> new MaxShannonHandler(100)); + assertThat(countSuccessful).isNotNull(); + final BigInteger countAborted = ModelCounter.count(Collections.singletonList(formula), formula.variables(), () -> new MaxShannonHandler(50)); + assertThat(countAborted).isNull(); + } + @Test @RandomTag public void testRandom() { @@ -249,4 +262,18 @@ private static BigInteger modelCount(final List models, final Sorted return BigInteger.valueOf(models.size()).multiply(BigInteger.valueOf(2).pow(dontCareVars.size())); } } + + private static class MaxShannonHandler implements DnnfCompilationHandler { + private int currentShannons = 0; + private final int maxShannons; + + private MaxShannonHandler(final int maxShannons) { + this.maxShannons = maxShannons; + } + + @Override + public boolean shannonExpansion() { + return ++this.currentShannons <= this.maxShannons; + } + } }