added possibility to pass a DNNF handler to the model counter

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
 

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<Formula> formulas, final SortedSet<Variable> 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<Formula> formulas, final SortedSet<Variable> variables,
+                                   final Supplier<DnnfCompilationHandler> 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<Formula> formulas, final SortedS
         final FormulaFactory f = variables.first().factory();
         final List<Formula> 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<Variable> dontCareVariables = simplification.getDontCareVariables(variables);
         return count.multiply(BigInteger.valueOf(2).pow(dontCareVariables.size()));
     }
@@ -122,14 +145,18 @@ private static SimplificationResult simplify(final Collection<Formula> formulas)
         return new SimplificationResult(simplified, backboneVariables);
     }
 
-    private static BigInteger count(final Collection<Formula> formulas, final FormulaFactory f) {
+    private static BigInteger count(final Collection<Formula> formulas, final Supplier<DnnfCompilationHandler> dnnfHandlerSupplier, final FormulaFactory f) {
         final Graph<Variable> constraintGraph = ConstraintGraphGenerator.generateFromFormulas(formulas);
         final Set<Set<Node<Variable>>> ccs = ConnectedComponentsComputation.compute(constraintGraph);
         final List<List<Formula>> components = ConnectedComponentsComputation.splitFormulasByComponent(formulas, ccs);
         final DnnfFactory factory = new DnnfFactory();
         BigInteger count = BigInteger.ONE;
         for (final List<Formula> 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;

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<Assignment> 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;
+        }
+    }
 }