From d950d8addbecb7d3f922c4c4521e966a26c8a2a5 Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Tue, 20 Aug 2024 12:13:37 +0200 Subject: [PATCH] LNGResults and Events for all DNNF computation steps --- .../events/ComputationStartedEvent.java | 1 + .../logicng/handlers/events/SimpleEvent.java | 3 + .../knowledgecompilation/bdds/BDDFactory.java | 7 +- .../dnnf/DnnfCompiler.java | 125 ++++++++++-------- .../dnnf/DnnfFactory.java | 22 +-- .../datastructures/dtree/DTreeGenerator.java | 18 ++- .../dtree/EliminatingOrderDTreeGenerator.java | 16 ++- .../dtree/MinFillDTreeGenerator.java | 20 ++- .../logicng/modelcounting/ModelCounter.java | 39 +++--- .../primecomputation/NaivePrimeReduction.java | 12 +- .../primecomputation/PrimeCompiler.java | 6 +- .../dnnf/DnnfCompilerTest.java | 51 +++++++ 12 files changed, 217 insertions(+), 103 deletions(-) diff --git a/src/main/java/com/booleworks/logicng/handlers/events/ComputationStartedEvent.java b/src/main/java/com/booleworks/logicng/handlers/events/ComputationStartedEvent.java index 4cbaf622..54577a1c 100644 --- a/src/main/java/com/booleworks/logicng/handlers/events/ComputationStartedEvent.java +++ b/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"); diff --git a/src/main/java/com/booleworks/logicng/handlers/events/SimpleEvent.java b/src/main/java/com/booleworks/logicng/handlers/events/SimpleEvent.java index 7e77d4c9..1dada637 100644 --- a/src/main/java/com/booleworks/logicng/handlers/events/SimpleEvent.java +++ b/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"); diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDFactory.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDFactory.java index ca39659a..fa603e6f 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/BDDFactory.java +++ b/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 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)); } diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompiler.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompiler.java index e9e00924..9d7ca15b 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompiler.java +++ b/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 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 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 initializeClauses() { return new Pair<>(f.and(units), f.and(nonUnits)); } - protected DTree generateDTree(final FormulaFactory f, final DTreeGenerator generator) { + protected LNGResult> 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 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 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 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 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 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 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 conjoin(final Formula implied, final DTreeNode tree, final int currentShannons, final ComputationHandler handler) { + if (implied == f.falsum()) { + return LNGResult.of(f.falsum()); + } + final LNGResult left = cnfAux(tree.left(), currentShannons, handler); + if (left.getResult() == null || left.getResult() == f.falsum()) { + return left; + } + final LNGResult 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 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 dnnf = cnf2Ddnnf(tree, handler); + if (dnnf.getResult() != null && dnnf.getResult() != f.falsum()) { + cache.put((BitSet) key.clone(), dnnf.getResult()); } return dnnf; } diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfFactory.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfFactory.java index b4342eb9..925e1aff 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfFactory.java +++ b/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 compile(final FormulaFactory f, final Formula formula, final ComputationHandler handler) { final SortedSet 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 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 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)); } } diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java index ea948d30..5a03d2c8 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java +++ b/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 generate(final FormulaFactory f, final Formula cnf, ComputationHandler handler); } diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java index 92d7344f..c678a806 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java @@ -4,10 +4,14 @@ package com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.dtree; +import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_DTREE_PROCESSING_NEXT_ORDER_VARIABLE; + import com.booleworks.logicng.formulas.FType; import com.booleworks.logicng.formulas.Formula; 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 java.util.ArrayList; import java.util.Iterator; @@ -29,14 +33,15 @@ public abstract class EliminatingOrderDTreeGenerator implements DTreeGenerator { * @param ordering the variable ordering * @return the DTree */ - public final DTree generateWithEliminatingOrder(final FormulaFactory f, final Formula cnf, - final List ordering) { + public final LNGResult generateWithEliminatingOrder(final FormulaFactory f, final Formula cnf, + final List ordering, + final ComputationHandler handler) { assert cnf.variables(f).size() == ordering.size(); if (!cnf.isCNF(f) || cnf.isAtomicFormula()) { throw new IllegalArgumentException("Cannot generate DTree from a non-cnf formula or atomic formula"); } else if (cnf.type() != FType.AND) { - return new DTreeLeaf(f, 0, cnf); + return LNGResult.of(new DTreeLeaf(f, 0, cnf)); } final List sigma = new ArrayList<>(); @@ -46,6 +51,9 @@ public final DTree generateWithEliminatingOrder(final FormulaFactory f, final Fo } for (final Variable variable : ordering) { + if (!handler.shouldResume(DNNF_DTREE_PROCESSING_NEXT_ORDER_VARIABLE)) { + return LNGResult.aborted(DNNF_DTREE_PROCESSING_NEXT_ORDER_VARIABLE); + } final List gamma = new ArrayList<>(); final Iterator sigmaIterator = sigma.iterator(); while (sigmaIterator.hasNext()) { @@ -60,7 +68,7 @@ public final DTree generateWithEliminatingOrder(final FormulaFactory f, final Fo } } - return compose(f, sigma); + return LNGResult.of(compose(f, sigma)); } protected DTree compose(final FormulaFactory f, final List trees) { diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java index 05e7a388..b3795a1f 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java @@ -4,11 +4,16 @@ package com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.dtree; +import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_DTREE_MIN_FILL_GRAPH_INITIALIZED; +import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_DTREE_MIN_FILL_NEW_ITERATION; + import com.booleworks.logicng.collections.LNGIntVector; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.Variable; +import com.booleworks.logicng.handlers.ComputationHandler; +import com.booleworks.logicng.handlers.LNGResult; import java.util.ArrayList; import java.util.Arrays; @@ -27,10 +32,12 @@ public class MinFillDTreeGenerator extends EliminatingOrderDTreeGenerator { @Override - public DTree generate(final FormulaFactory f, final Formula cnf) { + public LNGResult generate(final FormulaFactory f, final Formula cnf, final ComputationHandler handler) { final Graph graph = new Graph(f, cnf); - final List ordering = graph.getMinFillOrdering(); - return generateWithEliminatingOrder(f, cnf, ordering); + if (!handler.shouldResume(DNNF_DTREE_MIN_FILL_GRAPH_INITIALIZED)) { + return LNGResult.aborted(DNNF_DTREE_MIN_FILL_GRAPH_INITIALIZED); + } + return graph.getMinFillOrdering(handler).flatMap(ordering -> generateWithEliminatingOrder(f, cnf, ordering, handler)); } /** @@ -113,7 +120,7 @@ protected boolean[][] getCopyOfAdjMatrix() { return result; } - protected List getMinFillOrdering() { + protected LNGResult> getMinFillOrdering(final ComputationHandler handler) { final boolean[][] fillAdjMatrix = getCopyOfAdjMatrix(); final List fillEdgeList = getCopyOfEdgeList(); @@ -122,6 +129,9 @@ protected List getMinFillOrdering() { int treewidth = 0; for (int iteration = 0; iteration < numberOfVertices; iteration++) { + if (!handler.shouldResume(DNNF_DTREE_MIN_FILL_NEW_ITERATION)) { + return LNGResult.aborted(DNNF_DTREE_MIN_FILL_NEW_ITERATION); + } final LNGIntVector possiblyBestVertices = new LNGIntVector(); int minEdges = Integer.MAX_VALUE; for (int currentVertex = 0; currentVertex < numberOfVertices; currentVertex++) { @@ -190,7 +200,7 @@ protected List getMinFillOrdering() { processed[bestVertex] = true; ordering[iteration] = vertices.get(bestVertex); } - return Arrays.asList(ordering); + return LNGResult.of(Arrays.asList(ordering)); } } } diff --git a/src/main/java/com/booleworks/logicng/modelcounting/ModelCounter.java b/src/main/java/com/booleworks/logicng/modelcounting/ModelCounter.java index 8f59164c..7c71f3c4 100644 --- a/src/main/java/com/booleworks/logicng/modelcounting/ModelCounter.java +++ b/src/main/java/com/booleworks/logicng/modelcounting/ModelCounter.java @@ -4,8 +4,6 @@ package com.booleworks.logicng.modelcounting; -import static com.booleworks.logicng.handlers.events.SimpleEvent.NO_EVENT; - import com.booleworks.logicng.datastructures.Assignment; import com.booleworks.logicng.formulas.FType; import com.booleworks.logicng.formulas.Formula; @@ -17,6 +15,7 @@ import com.booleworks.logicng.graphs.datastructures.Node; import com.booleworks.logicng.graphs.generators.ConstraintGraphGenerator; import com.booleworks.logicng.handlers.ComputationHandler; +import com.booleworks.logicng.handlers.LNGResult; import com.booleworks.logicng.handlers.NopHandler; import com.booleworks.logicng.knowledgecompilation.dnnf.DnnfFactory; import com.booleworks.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; @@ -58,8 +57,9 @@ private ModelCounter() { * @param variables the relevant variables * @return the model count of the formulas for the variables */ - public static BigInteger count(final FormulaFactory f, final Collection formulas, final SortedSet variables) { - return count(f, formulas, variables, NopHandler.get()); + public static BigInteger count(final FormulaFactory f, final Collection formulas, + final SortedSet variables) { + return count(f, formulas, variables, NopHandler.get()).getResult(); } /** @@ -70,26 +70,27 @@ public static BigInteger count(final FormulaFactory f, final Collection * @param formulas the list of formulas * @param variables the relevant variables * @param handler the computation handler - * @return the model count of the formulas for the variables or {@code null} if the DNNF handler aborted the DNNF computation + * @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 FormulaFactory f, final Collection formulas, final SortedSet variables, - final ComputationHandler handler) { + public static LNGResult count(final FormulaFactory f, final Collection formulas, + final SortedSet variables, final ComputationHandler handler) { if (!variables.containsAll(FormulaHelper.variables(f, formulas))) { throw new IllegalArgumentException("Expected variables to contain all of the formulas' variables."); } if (variables.isEmpty()) { final List remainingConstants = formulas.stream().filter(formula -> formula.type() != FType.TRUE).collect(Collectors.toList()); - return remainingConstants.isEmpty() ? BigInteger.ONE : BigInteger.ZERO; + return LNGResult.of(remainingConstants.isEmpty() ? BigInteger.ONE : BigInteger.ZERO); } final List cnfs = encodeAsCnf(f, formulas); final SimplificationResult simplification = simplify(f, cnfs); - final BigInteger count = count(f, simplification.simplifiedFormulas, handler); - if (count == null) { - return null; + final LNGResult count = count(f, simplification.simplifiedFormulas, handler); + if (!count.isSuccess()) { + return count; } final SortedSet dontCareVariables = simplification.getDontCareVariables(variables); - return count.multiply(BigInteger.valueOf(2).pow(dontCareVariables.size())); + return LNGResult.of(count.getResult().multiply(BigInteger.valueOf(2).pow(dontCareVariables.size()))); } private static List encodeAsCnf(final FormulaFactory f, final Collection formulas) { @@ -124,21 +125,21 @@ private static SimplificationResult simplify(final FormulaFactory f, final Colle return new SimplificationResult(f, backboneVariables, simplified); } - private static BigInteger count(final FormulaFactory f, final Collection formulas, - final ComputationHandler handler) { + private static LNGResult count(final FormulaFactory f, final Collection formulas, + final ComputationHandler handler) { final Graph constraintGraph = ConstraintGraphGenerator.generateFromFormulas(f, formulas); final Set>> ccs = ConnectedComponentsComputation.compute(constraintGraph); final List> components = ConnectedComponentsComputation.splitFormulasByComponent(f, formulas, ccs); final DnnfFactory factory = new DnnfFactory(); BigInteger count = BigInteger.ONE; for (final List component : components) { - final Dnnf dnnf = factory.compile(f, f.and(component), handler); - if (dnnf == null || !handler.shouldResume(NO_EVENT)) { - return null; + final LNGResult dnnf = factory.compile(f, f.and(component), handler); + if (!dnnf.isSuccess()) { + return LNGResult.aborted(dnnf.getAbortionEvent()); } - count = count.multiply(dnnf.execute(new DnnfModelCountFunction(f))); + count = count.multiply(dnnf.getResult().execute(new DnnfModelCountFunction(f))); } - return count; + return LNGResult.of(count); } private static class SimplificationResult { diff --git a/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java b/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java index 601095e9..2bead2f7 100644 --- a/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java +++ b/src/main/java/com/booleworks/logicng/primecomputation/NaivePrimeReduction.java @@ -4,13 +4,15 @@ package com.booleworks.logicng.primecomputation; +import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.IMPLICANT_REDUCTION_STARTED; +import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.IMPLICATE_REDUCTION_STARTED; + 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.solvers.SATSolver; import com.booleworks.logicng.solvers.sat.SATSolverConfig; import com.booleworks.logicng.util.FormulaHelper; @@ -69,7 +71,9 @@ public SortedSet reduceImplicant(final SortedSet implicant) { */ public LNGResult> reduceImplicant(final SortedSet implicant, final ComputationHandler handler) { - handler.shouldResume(ComputationStartedEvent.IMPLICATE_REDUCTION_STARTED); + if (!handler.shouldResume(IMPLICANT_REDUCTION_STARTED)) { + return LNGResult.aborted(IMPLICANT_REDUCTION_STARTED); + } final SortedSet primeImplicant = new TreeSet<>(implicant); for (final Literal lit : implicant) { primeImplicant.remove(lit); @@ -109,7 +113,9 @@ public SortedSet reduceImplicate(final FormulaFactory f, final SortedSe */ public LNGResult> reduceImplicate(final FormulaFactory f, final SortedSet implicate, final ComputationHandler handler) { - handler.shouldResume(ComputationStartedEvent.IMPLICATE_REDUCTION_STARTED); + if (!handler.shouldResume(IMPLICATE_REDUCTION_STARTED)) { + return LNGResult.aborted(IMPLICATE_REDUCTION_STARTED); + } final SortedSet primeImplicate = new TreeSet<>(implicate); for (final Literal lit : implicate) { primeImplicate.remove(lit); diff --git a/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java b/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java index 3fb48a2b..8a49902f 100644 --- a/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/com/booleworks/logicng/primecomputation/PrimeCompiler.java @@ -4,6 +4,8 @@ package com.booleworks.logicng.primecomputation; +import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.*; + import com.booleworks.logicng.datastructures.Assignment; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; @@ -108,7 +110,9 @@ public PrimeResult compute(final FormulaFactory f, final Formula formula, final */ public LNGResult compute(final FormulaFactory f, final Formula formula, final PrimeResult.CoverageType type, final ComputationHandler handler) { - handler.shouldResume(ComputationStartedEvent.PRIME_COMPUTATION_STARTED); + if (!handler.shouldResume(PRIME_COMPUTATION_STARTED)) { + return LNGResult.aborted(PRIME_COMPUTATION_STARTED); + } final boolean completeImplicants = type == PrimeResult.CoverageType.IMPLICANTS_COMPLETE; final Formula formulaForComputation = completeImplicants ? formula : formula.negate(f); final LNGResult>, List>>> genericResult = diff --git a/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java b/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java index 7e56b54e..a57ba732 100644 --- a/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java +++ b/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java @@ -4,7 +4,19 @@ package com.booleworks.logicng.knowledgecompilation.dnnf; +import static com.booleworks.logicng.handlers.events.ComputationFinishedEvent.SAT_CALL_FINISHED; +import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.BACKBONE_COMPUTATION_STARTED; +import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.DNNF_COMPUTATION_STARTED; +import static com.booleworks.logicng.handlers.events.ComputationStartedEvent.SAT_CALL_STARTED; +import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_DTREE_MIN_FILL_GRAPH_INITIALIZED; +import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_DTREE_MIN_FILL_NEW_ITERATION; +import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_DTREE_PROCESSING_NEXT_ORDER_VARIABLE; +import static com.booleworks.logicng.handlers.events.SimpleEvent.DNNF_SHANNON_EXPANSION; +import static com.booleworks.logicng.handlers.events.SimpleEvent.SAT_CONFLICT_DETECTED; +import static com.booleworks.logicng.handlers.events.SimpleEvent.SUBSUMPTION_ADDED_NEW_SET; +import static com.booleworks.logicng.handlers.events.SimpleEvent.SUBSUMPTION_STARTING_UB_TREE_GENERATION; import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.entry; import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.encodings.EncoderConfig; @@ -17,6 +29,9 @@ import com.booleworks.logicng.graphs.datastructures.Graph; import com.booleworks.logicng.graphs.datastructures.Node; import com.booleworks.logicng.graphs.generators.ConstraintGraphGenerator; +import com.booleworks.logicng.handlers.ComputationHandler; +import com.booleworks.logicng.handlers.LNGResult; +import com.booleworks.logicng.handlers.events.LNGEvent; import com.booleworks.logicng.io.parsers.FormulaParser; import com.booleworks.logicng.io.parsers.ParserException; import com.booleworks.logicng.io.parsers.PropositionalParser; @@ -35,7 +50,9 @@ import java.io.IOException; import java.math.BigInteger; import java.util.ArrayList; +import java.util.LinkedHashMap; import java.util.List; +import java.util.Map; import java.util.Set; public class DnnfCompilerTest { @@ -95,6 +112,30 @@ public void testAllSmallFormulas() throws IOException, ParserException { formulas.stream().forEach(op -> testFormula(f, op, false)); } + @Test + public void testDnnfEvents() throws ParserException, IOException { + final FormulaFactory f = FormulaFactory.caching(); + f.putConfiguration(EncoderConfig.builder().amoEncoding(EncoderConfig.AMO_ENCODER.PURE).build()); + final Formula parsed = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/formula1.txt"); + final DnnfFactory dnnfFactory = new DnnfFactory(); + final DnnfComputationHandler handler = new DnnfComputationHandler(); + final LNGResult dnnf = dnnfFactory.compile(f, parsed, handler); + assertThat(dnnf.isSuccess()).isTrue(); + assertThat(handler.eventCounter).containsExactly( + entry(BACKBONE_COMPUTATION_STARTED, 1), + entry(SAT_CALL_STARTED, 125), + entry(SAT_CONFLICT_DETECTED, 51), + entry(SAT_CALL_FINISHED, 125), + entry(SUBSUMPTION_STARTING_UB_TREE_GENERATION, 1), + entry(SUBSUMPTION_ADDED_NEW_SET, 4104), + entry(DNNF_DTREE_MIN_FILL_GRAPH_INITIALIZED, 1), + entry(DNNF_DTREE_MIN_FILL_NEW_ITERATION, 411), + entry(DNNF_DTREE_PROCESSING_NEXT_ORDER_VARIABLE, 411), + entry(DNNF_COMPUTATION_STARTED, 1), + entry(DNNF_SHANNON_EXPANSION, 6866) + ); + } + @Test @LongRunningTag public void testLargeFormula() throws IOException, ParserException { @@ -149,4 +190,14 @@ private BigInteger countWithBdd(final Formula formula) { final BDD bdd = BDDFactory.build(formula.factory(), formula, kernel); return bdd.modelCount(); } + + private static class DnnfComputationHandler implements ComputationHandler { + private final Map eventCounter = new LinkedHashMap<>(); + + @Override + public boolean shouldResume(final LNGEvent event) { + eventCounter.put(event, eventCounter.getOrDefault(event, 0) + 1); + return true; + } + } }