diff --git a/CHANGELOG.md b/CHANGELOG.md index fefd2d09..7e495903 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -19,6 +19,7 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - `BDDKernel.activateReorderDuringBuild` for activating reordering during build - `BDDKernel.addVariableBlock` for defining a variable block for reordering - `BDDKernel.addAllVariablesAsBlock` for defining one block for each variable (s.t. all variables are allowed to be reordered independently) +- Significant performance improvements in the DTree generation for DNNFs ### Fixed diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java index 0aa2e70c..626fa77f 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java @@ -36,8 +36,10 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; +import java.util.LinkedHashSet; import java.util.List; import java.util.Map; +import java.util.Set; import java.util.SortedSet; /** @@ -73,7 +75,7 @@ public static class Graph { /** * The edges of the graph as a list of edges per node ({{2,3},{1},{1}} means that there are the edges 1-2 and 1-3) */ - protected final List edgeList; + protected final List> edgeList; /** * Computes the DTree from the given CNF. @@ -94,7 +96,7 @@ public Graph(final Formula cnf) { this.adjMatrix = new boolean[this.numberOfVertices][this.numberOfVertices]; this.edgeList = new ArrayList<>(this.numberOfVertices); for (int i = 0; i < this.numberOfVertices; i++) { - this.edgeList.add(new LNGIntVector()); + this.edgeList.add(new LinkedHashSet<>()); } for (final Formula clause : cnf) { @@ -106,8 +108,8 @@ public Graph(final Formula cnf) { } for (int i = 0; i < varNums.length; i++) { for (int j = i + 1; j < varNums.length; j++) { - this.edgeList.get(varNums[i]).push(varNums[j]); - this.edgeList.get(varNums[j]).push(varNums[i]); + this.edgeList.get(varNums[i]).add(varNums[j]); + this.edgeList.get(varNums[j]).add(varNums[i]); this.adjMatrix[varNums[i]][varNums[j]] = true; this.adjMatrix[varNums[j]][varNums[i]] = true; } @@ -117,8 +119,8 @@ public Graph(final Formula cnf) { protected List getCopyOfEdgeList() { final List result = new ArrayList<>(); - for (final LNGIntVector edge : this.edgeList) { - result.add(new LNGIntVector(edge)); + for (final Set edge : this.edgeList) { + result.add(new LNGIntVector(edge.stream().mapToInt(i -> i).toArray())); } return result; } @@ -196,7 +198,7 @@ protected List getMinFillOrdering() { int currentNumberOfEdges = 0; for (int k = 0; k < this.numberOfVertices; k++) { - if (fillAdjMatrix[bestVertex][k] && !processed[k]) { + if (k != bestVertex && !processed[k] && fillAdjMatrix[bestVertex][k]) { currentNumberOfEdges++; } }