LNGResults and Events for all DNNF computation steps

src/main/java/com/booleworks/logicng/handlers/events/ComputationStartedEvent.java

@@ -25,6 +25,7 @@ public class ComputationStartedEvent implements LNGEvent {
     public static final ComputationStartedEvent BACKBONE_COMPUTATION_STARTED = new ComputationStartedEvent("Backbone Computation");
     public static final ComputationStartedEvent ADVANCED_SIMPLIFICATION_STARTED = new ComputationStartedEvent("Advanced Simplification");
     public static final ComputationStartedEvent PRIME_COMPUTATION_STARTED = new ComputationStartedEvent("Prime Computation");
+    public static final ComputationStartedEvent IMPLICANT_REDUCTION_STARTED = new ComputationStartedEvent("Implicant Reduction");
     public static final ComputationStartedEvent IMPLICATE_REDUCTION_STARTED = new ComputationStartedEvent("Implicate Reduction");
     public static final ComputationStartedEvent MUS_COMPUTATION_STARTED = new ComputationStartedEvent("MUS Computation");
     public static final ComputationStartedEvent SMUS_COMPUTATION_STARTED = new ComputationStartedEvent("SMUS Computation");

src/main/java/com/booleworks/logicng/handlers/events/SimpleEvent.java

@@ -17,6 +17,9 @@ public class SimpleEvent implements LNGEvent {
     public static final SimpleEvent NO_EVENT = new SimpleEvent("No event");
     public static final SimpleEvent DISTRIBUTION_PERFORMED = new SimpleEvent("Distribution performed");
     public static final SimpleEvent BDD_NEW_REF_ADDED = new SimpleEvent("New reference added in BDD");
+    public static final SimpleEvent DNNF_DTREE_MIN_FILL_GRAPH_INITIALIZED = new SimpleEvent("DNNF DTree MinFill Graph initialized");
+    public static final SimpleEvent DNNF_DTREE_MIN_FILL_NEW_ITERATION = new SimpleEvent("DNNF DTree MinFill new iteration");
+    public static final SimpleEvent DNNF_DTREE_PROCESSING_NEXT_ORDER_VARIABLE = new SimpleEvent("DNNF DTree processing next order variable");
     public static final SimpleEvent DNNF_SHANNON_EXPANSION = new SimpleEvent("DNNF Shannon Expansion");
     public static final SimpleEvent SAT_CONFLICT_DETECTED = new SimpleEvent("SAT conflict detected");
     public static final SimpleEvent MODEL_ENUMERATION_COMMIT = new SimpleEvent("Model Enumeration Commit");

src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDFactory.java

@@ -33,6 +33,7 @@
 package com.booleworks.logicng.knowledgecompilation.bdds;
 
 import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.BDD_COMPUTATION_STARTED;
+import static com.booleworks.logicng.handlers.events.SimpleEvent.BDD_NEW_REF_ADDED;
 
 import com.booleworks.logicng.formulas.And;
 import com.booleworks.logicng.formulas.BinaryOperator;
@@ -118,12 +119,14 @@ public static BDD build(final FormulaFactory f, final Formula formula, final BDD
      */
     public static LNGResult<BDD> build(final FormulaFactory f, final Formula formula, final BDDKernel kernel,
                                        final ComputationHandler handler) {
-        handler.shouldResume(BDD_COMPUTATION_STARTED);
+        if (!handler.shouldResume(BDD_COMPUTATION_STARTED)) {
+            return LNGResult.aborted(BDD_COMPUTATION_STARTED);
+        }
         final int varNum = formula.variables(f).size();
         final BDDKernel bddKernel = kernel == null ? new BDDKernel(f, varNum, varNum * 30, varNum * 20) : kernel;
         final int bddIndex = buildRec(f, formula, bddKernel, new BDDConstruction(bddKernel), handler);
         return bddIndex == BDDKernel.BDD_ABORT
-                ? LNGResult.aborted(SimpleEvent.BDD_NEW_REF_ADDED)
+                ? LNGResult.aborted(BDD_NEW_REF_ADDED)
                 : LNGResult.of(new BDD(bddIndex, bddKernel));
     }
 

src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompiler.java

@@ -4,14 +4,15 @@
 
 package com.booleworks.logicng.knowledgecompilation.dnnf;
 
+import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.DNNF_COMPUTATION_STARTED;
 import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_SHANNON_EXPANSION;
 
 import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.Literal;
 import com.booleworks.logicng.handlers.ComputationHandler;
+import com.booleworks.logicng.handlers.LNGResult;
 import com.booleworks.logicng.handlers.NopHandler;
-import com.booleworks.logicng.handlers.events.ComputationStartedEvent;
 import com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.dtree.DTree;
 import com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.dtree.DTreeGenerator;
 import com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.dtree.DTreeLeaf;
@@ -27,7 +28,7 @@
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
-import java.util.concurrent.TimeoutException;
+import java.util.Optional;
 
 /**
  * Implementation of a DNNF compiler based on ideas by Adnan Darwiche in "New
@@ -47,7 +48,6 @@ public class DnnfCompiler {
     protected final int numberOfVariables;
 
     protected final Map<BitSet, Formula> cache;
-    protected ComputationHandler handler;
 
     protected BitSet[][] localCacheKeys;
     protected int[][][] localOccurrences;
@@ -80,7 +80,7 @@ public DnnfCompiler(final FormulaFactory f, final Formula formula) {
      * @return the compiled DNNF
      */
     public Formula compile(final DTreeGenerator generator) {
-        return compile(generator, null);
+        return compile(generator, NopHandler.get()).getResult();
     }
 
     /**
@@ -90,12 +90,11 @@ public Formula compile(final DTreeGenerator generator) {
      * @param handler   the compilation handler
      * @return the compiled DNNF
      */
-    public Formula compile(final DTreeGenerator generator, final ComputationHandler handler) {
+    public LNGResult<Formula> compile(final DTreeGenerator generator, final ComputationHandler handler) {
         if (!cnf.holds(new SATPredicate(f))) {
-            return f.falsum();
+            return LNGResult.of(f.falsum());
         }
-        final DTree dTree = generateDTree(f, generator);
-        return compile(dTree, handler);
+        return generateDTree(f, generator, handler).flatMap(tree -> compile(tree.orElse(null), handler));
     }
 
     protected int computeMaxClauseSize(final Formula cnf) {
@@ -137,34 +136,30 @@ protected Pair<Formula, Formula> initializeClauses() {
         return new Pair<>(f.and(units), f.and(nonUnits));
     }
 
-    protected DTree generateDTree(final FormulaFactory f, final DTreeGenerator generator) {
+    protected LNGResult<Optional<DTree>> generateDTree(final FormulaFactory f, final DTreeGenerator generator, final ComputationHandler handler) {
         if (nonUnitClauses.isAtomicFormula()) {
-            return null;
+            return LNGResult.of(Optional.empty());
         }
-        final DTree tree = generator.generate(f, nonUnitClauses);
-        tree.initialize(solver);
-        return tree;
+        final LNGResult<DTree> tree = generator.generate(f, nonUnitClauses, handler);
+        if (tree.isSuccess()) {
+            tree.getResult().initialize(solver);
+        }
+        return tree.map(Optional::of);
     }
 
-    protected Formula compile(final DTree dTree, final ComputationHandler handler) {
+    protected LNGResult<Formula> compile(final DTree dTree, final ComputationHandler handler) {
         if (nonUnitClauses.isAtomicFormula()) {
-            return cnf;
+            return LNGResult.of(cnf);
         }
         if (!solver.start()) {
-            return f.falsum();
+            return LNGResult.of(f.falsum());
         }
         initializeCaches(dTree);
-        this.handler = handler;
-        handler.shouldResume(ComputationStartedEvent.DNNF_COMPUTATION_STARTED);
-
-        Formula result;
-        try {
-            result = cnf2Ddnnf(dTree);
-        } catch (final TimeoutException e) {
-            result = null;
+        if (!handler.shouldResume(DNNF_COMPUTATION_STARTED)) {
+            return LNGResult.aborted(DNNF_COMPUTATION_STARTED);
         }
-        this.handler = NopHandler.get();
-        return result == null ? null : f.and(unitClauses, result);
+
+        return cnf2Ddnnf(dTree, handler).map(result -> f.and(unitClauses, result));
     }
 
     protected void initializeCaches(final DTree dTree) {
@@ -182,59 +177,71 @@ protected void initializeCaches(final DTree dTree) {
         }
     }
 
-    protected Formula cnf2Ddnnf(final DTree tree) throws TimeoutException {
-        return cnf2Ddnnf(tree, 0);
+    protected LNGResult<Formula> cnf2Ddnnf(final DTree tree, final ComputationHandler handler) {
+        return cnf2Ddnnf(tree, 0, handler);
     }
 
-    protected Formula cnf2Ddnnf(final DTree tree, final int currentShannons) throws TimeoutException {
+    protected LNGResult<Formula> cnf2Ddnnf(final DTree tree, final int currentShannons, final ComputationHandler handler) {
         final BitSet separator = tree.dynamicSeparator();
         final Formula implied = newlyImpliedLiterals(tree.staticVarSet());
 
         if (separator.isEmpty()) {
             if (tree instanceof DTreeLeaf) {
-                return f.and(implied, leaf2Ddnnf((DTreeLeaf) tree));
+                return LNGResult.of(f.and(implied, leaf2Ddnnf((DTreeLeaf) tree)));
             } else {
-                return conjoin(implied, (DTreeNode) tree, currentShannons);
+                return conjoin(implied, (DTreeNode) tree, currentShannons, handler);
             }
         } else {
-            final int var = chooseShannonVariable(tree, separator, currentShannons);
-
             if (!handler.shouldResume(DNNF_SHANNON_EXPANSION)) {
-                throw new TimeoutException();
+                return LNGResult.aborted(DNNF_SHANNON_EXPANSION);
             }
 
+            final int var = chooseShannonVariable(tree, separator, currentShannons);
+
             /* Positive branch */
-            Formula positiveDnnf = f.falsum();
+            final Formula positiveDnnf;
             if (solver.decide(var, true)) {
-                positiveDnnf = cnf2Ddnnf(tree, currentShannons + 1);
+                final LNGResult<Formula> recursivePositive = cnf2Ddnnf(tree, currentShannons + 1, handler);
+                if (!recursivePositive.isSuccess()) {
+                    solver.undoDecide(var);
+                    return recursivePositive;
+                }
+                positiveDnnf = recursivePositive.getResult();
+            } else {
+                positiveDnnf = f.falsum();
             }
             solver.undoDecide(var);
             if (positiveDnnf == f.falsum()) {
                 if (solver.atAssertionLevel() && solver.assertCdLiteral()) {
-                    return cnf2Ddnnf(tree);
+                    return cnf2Ddnnf(tree, handler);
                 } else {
-                    return f.falsum();
+                    return LNGResult.of(f.falsum());
                 }
             }
 
             /* Negative branch */
             Formula negativeDnnf = f.falsum();
             if (solver.decide(var, false)) {
-                negativeDnnf = cnf2Ddnnf(tree, currentShannons + 1);
+                final LNGResult<Formula> recursiveNegative = cnf2Ddnnf(tree, currentShannons + 1, handler);
+                if (!recursiveNegative.isSuccess()) {
+                    solver.undoDecide(var);
+                    return recursiveNegative;
+                }
+                negativeDnnf = recursiveNegative.getResult();
             }
             solver.undoDecide(var);
             if (negativeDnnf == f.falsum()) {
                 if (solver.atAssertionLevel() && solver.assertCdLiteral()) {
-                    return cnf2Ddnnf(tree);
+                    return cnf2Ddnnf(tree, handler);
                 } else {
-                    return f.falsum();
+                    return LNGResult.of(f.falsum());
                 }
             }
 
             final Literal lit = solver.litForIdx(var);
             final Formula positiveBranch = f.and(lit, positiveDnnf);
             final Formula negativeBranch = f.and(lit.negate(f), negativeDnnf);
-            return f.and(implied, f.or(positiveBranch, negativeBranch));
+            return LNGResult.of(f.and(implied, f.or(positiveBranch, negativeBranch)));
         }
     }
 
@@ -257,30 +264,32 @@ protected int chooseShannonVariable(final DTree tree, final BitSet separator, fi
         return max;
     }
 
-    protected Formula conjoin(final Formula implied, final DTreeNode tree, final int currentShannons)
-            throws TimeoutException {
-        final Formula left;
-        final Formula right;
-        if (implied == f.falsum() ||
-                (left = cnfAux(tree.left(), currentShannons)) == f.falsum() ||
-                (right = cnfAux(tree.right(), currentShannons)) == f.falsum()) {
-            return f.falsum();
-        } else {
-            return f.and(implied, left, right);
+    protected LNGResult<Formula> conjoin(final Formula implied, final DTreeNode tree, final int currentShannons, final ComputationHandler handler) {
+        if (implied == f.falsum()) {
+            return LNGResult.of(f.falsum());
+        }
+        final LNGResult<Formula> left = cnfAux(tree.left(), currentShannons, handler);
+        if (left.getResult() == null || left.getResult() == f.falsum()) {
+            return left;
+        }
+        final LNGResult<Formula> right = cnfAux(tree.right(), currentShannons, handler);
+        if (right.getResult() == null || right.getResult() == f.falsum()) {
+            return right;
         }
+        return LNGResult.of(f.and(implied, left.getResult(), right.getResult()));
     }
 
-    protected Formula cnfAux(final DTree tree, final int currentShannons) throws TimeoutException {
+    protected LNGResult<Formula> cnfAux(final DTree tree, final int currentShannons, final ComputationHandler handler) {
         if (tree instanceof DTreeLeaf) {
-            return leaf2Ddnnf((DTreeLeaf) tree);
+            return LNGResult.of(leaf2Ddnnf((DTreeLeaf) tree));
         } else {
             final BitSet key = computeCacheKey((DTreeNode) tree, currentShannons);
             if (cache.containsKey(key)) {
-                return cache.get(key);
+                return LNGResult.of(cache.get(key));
             } else {
-                final Formula dnnf = cnf2Ddnnf(tree);
-                if (dnnf != f.falsum()) {
-                    cache.put((BitSet) key.clone(), dnnf);
+                final LNGResult<Formula> dnnf = cnf2Ddnnf(tree, handler);
+                if (dnnf.getResult() != null && dnnf.getResult() != f.falsum()) {
+                    cache.put((BitSet) key.clone(), dnnf.getResult());
                 }
                 return dnnf;
             }

src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfFactory.java

@@ -8,6 +8,7 @@
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.Variable;
 import com.booleworks.logicng.handlers.ComputationHandler;
+import com.booleworks.logicng.handlers.LNGResult;
 import com.booleworks.logicng.handlers.NopHandler;
 import com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.Dnnf;
 import com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.dtree.MinFillDTreeGenerator;
@@ -30,7 +31,7 @@ public class DnnfFactory {
      * @return the compiled DNNF
      */
     public Dnnf compile(final FormulaFactory f, final Formula formula) {
-        return compile(f, formula, NopHandler.get());
+        return compile(f, formula, NopHandler.get()).getResult();
     }
 
     /**
@@ -40,19 +41,22 @@ public Dnnf compile(final FormulaFactory f, final Formula formula) {
      * @param handler the computation handler
      * @return the compiled DNNF
      */
-    public Dnnf compile(final FormulaFactory f, final Formula formula, final ComputationHandler handler) {
+    public LNGResult<Dnnf> compile(final FormulaFactory f, final Formula formula, final ComputationHandler handler) {
         final SortedSet<Variable> originalVariables = new TreeSet<>(formula.variables(f));
         final Formula cnf = formula.cnf(f);
         originalVariables.addAll(cnf.variables(f));
-        final Formula simplifiedFormula = simplifyFormula(f, cnf, handler);
-        final DnnfCompiler compiler = new DnnfCompiler(f, simplifiedFormula);
-        final Formula dnnf = compiler.compile(new MinFillDTreeGenerator(), handler);
-        return dnnf == null ? null : new Dnnf(originalVariables, dnnf);
+        final LNGResult<Formula> simplifiedFormula = simplifyFormula(f, cnf, handler);
+        if (!simplifiedFormula.isSuccess()) {
+            return LNGResult.aborted(simplifiedFormula.getAbortionEvent());
+        }
+        return new DnnfCompiler(f, simplifiedFormula.getResult())
+                .compile(new MinFillDTreeGenerator(), handler)
+                .map(dnnf -> new Dnnf(originalVariables, dnnf));
     }
 
-    protected Formula simplifyFormula(final FormulaFactory f, final Formula formula, final ComputationHandler handler) {
+    protected LNGResult<Formula> simplifyFormula(final FormulaFactory f, final Formula formula, final ComputationHandler handler) {
         return formula
-                .transform(new BackboneSimplifier(f))
-                .transform(new CNFSubsumption(f));
+                .transform(new BackboneSimplifier(f), handler)
+                .flatMap(res -> res.transform(new CNFSubsumption(f), handler));
     }
 }

src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java

@@ -6,10 +6,13 @@
 
 import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
+import com.booleworks.logicng.handlers.ComputationHandler;
+import com.booleworks.logicng.handlers.LNGResult;
+import com.booleworks.logicng.handlers.NopHandler;
 
 /**
  * A generator for a DTree.
- * @version 2.0.0
+ * @version 3.0.0
  * @since 2.0.0
  */
 public interface DTreeGenerator {
@@ -20,5 +23,16 @@ public interface DTreeGenerator {
      * @param cnf the CNF
      * @return the DTree
      */
-    DTree generate(final FormulaFactory f, final Formula cnf);
+    default DTree generate(final FormulaFactory f, final Formula cnf) {
+        return generate(f, cnf, NopHandler.get()).getResult();
+    }
+
+    /**
+     * Generates a DTree for the given CNF.
+     * @param f       the formula factory
+     * @param cnf     the CNF
+     * @param handler the computation handler
+     * @return the DTree
+     */
+    LNGResult<DTree> generate(final FormulaFactory f, final Formula cnf, ComputationHandler handler);
 }