From fedef469123666d1eb0fe653afab6a3495d2bd82 Mon Sep 17 00:00:00 2001 From: Steffen Hildebrandt Date: Tue, 12 Mar 2024 10:43:59 +0100 Subject: [PATCH] BDD reordering refactoring --- CHANGELOG.md | 10 +- .../knowledgecompilation/bdds/BDD.java | 20 ++- .../bdds/jbuddy/BDDKernel.java | 157 +++++++++++++++++- .../bdds/jbuddy/BDDReordering.java | 36 +++- .../bdds/BDDReorderingTest.java | 47 +++--- 5 files changed, 226 insertions(+), 44 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 21fa545b..bd115890 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,11 +11,18 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### Changed - UBTree data structure now supports empty sets. -- Added side effect note in `SATSolver` for the four assumption solving methods. +- Added side effect note in `SATSolver` for the four assumption solving methods. +- Methods for reordering and swapping variables on BDD were refactored: `BDD.getReordering`, `BDDKernel.getReordering`, and `BDD.swapVariables` are now deprecated and should not be used anymore. Instead, there are new methods on the `BDDKernel`. Note that these actions affect all BDDs generated by the kernel. + - `BDDKernel.swapVariables` for swapping two variables (or variable indices) + - `BDDKernel.reorder` for automatically reordering the BDD + - `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) ### Fixed - Fixed edge case in method `add(Formula formula, Proposition proposition)` in `MiniSat`. If a formula is added to the SAT solver, it can happen that a variable is not added to the solver because it was removed during the CNF transformation. A `model()` call or model enumeration will not produce models containing this variable since it was not added to the solver. The fix ensures that all variables of the original formula are added to the solver and thus, a found model includes the variable. +- The formula generation on BDDs was broken when the ordering was changed by `BDDKernel.reorder` or `BDDKernel.swapVariables`. This is now fixed. ## [2.4.1] - 2022-12-01 @@ -374,4 +381,3 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### Added - Initial Release of LogicNG - diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java b/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java index df387198..ec114090 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/BDD.java @@ -439,22 +439,24 @@ public List getVariableOrder() { * BDDs, the variables are swapped in all of these BDDs. * @param first the first variable to swap * @param second the second variable to swap + * @deprecated dangerous API, will be removed in version 3.0, use {@link BDDKernel#swapVariables} instead */ + @Deprecated public void swapVariables(final Variable first, final Variable second) { - final int firstVar = this.kernel.getIndexForVariable(first); - final int secondVar = this.kernel.getIndexForVariable(second); - if (firstVar < 0) { - throw new IllegalArgumentException("Unknown variable: " + first); - } else if (secondVar < 0) { - throw new IllegalArgumentException("Unknown variable: " + second); - } - this.kernel.getReordering().swapVariables(firstVar, secondVar); + this.kernel.swapVariables(first, second); } /** * Returns the reordering object for the BDD kernel. * @return the reordering object - */ + * @deprecated the relevant methods should now be access via the {@link #underlyingKernel() kernel}: + * + */ + @Deprecated public BDDReordering getReordering() { return this.kernel.getReordering(); } diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java index d036fb76..c6eb639a 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java @@ -152,7 +152,7 @@ public BDDKernel(final FormulaFactory f, final int numVars, final int nodeSize, this.var2idx = new TreeMap<>(); this.idx2var = new TreeMap<>(); this.reordering = new BDDReordering(this); - this.nodesize = prime.primeGTE(Math.max(nodeSize, 3)); + this.nodesize = this.prime.primeGTE(Math.max(nodeSize, 3)); this.nodes = new int[this.nodesize * 6]; this.minfreenodes = 20; for (int n = 0; n < this.nodesize; n++) { @@ -261,7 +261,16 @@ public FormulaFactory factory() { /** * Returns the reordering object for this kernel. * @return the reordering object + * @deprecated the relevant methods of this object are now exposed directly + * on this kernel: + * */ + @Deprecated public BDDReordering getReordering() { return this.reordering; } @@ -319,6 +328,148 @@ public int[] getCurrentVarOrder() { return Arrays.copyOf(this.level2var, this.level2var.length - 1); // last var is always 0 } + /** + * Swaps the variables {@code v1} and {@code v2}. This affects all BDDs + * created by this kernel. + * @param v1 the first variable to swap + * @param v2 the second variable to swap + */ + public void swapVariables(final int v1, final int v2) { + this.reordering.swapVariables(v1, v2); + } + + /** + * Swaps the variables {@code v1} and {@code v2}. This affects all BDDs + * created by this kernel. + * @param v1 the first variable to swap + * @param v2 the second variable to swap + */ + public void swapVariables(final Variable v1, final Variable v2) { + swapVariables(getIndexForVariable(v1), getIndexForVariable(v2)); + } + + /** + * Activates or deactivates the automatic reordering during the construction of a BDD. + *

+ * Automatic reordering can be deactivated by passing {@link BDDReorderingMethod#BDD_REORDER_NONE} + * for the {@code method} parameter, otherwise the reordering is activated with the + * given method. The reordering is executed at most {@code num} times. + * @param method the method to be used for reordering + * @param num the maximum number of reorders to be performed + */ + public void activateReorderDuringConstruction(final BDDReorderingMethod method, final int num) { + this.reordering.activateReorderDuringConstruction(method, num); + } + + /** + * Adds a variable block starting at variable {@code first} and ending in variable + * {@code last} (both inclusive). + *

+ * Variable blocks are used in the {@link #reorder BDD reordering} + * or in the automatic reordering during the construction of the BDD (configured by + * {@link #activateReorderDuringConstruction}). Variable blocks can be nested, i.e. one block can + * contain an arbitrary number of ("child") blocks. Furthermore, a variable block can also + * be a single variable. + *

+ * During reordering, the child blocks of a parent block can be reordered, but they are kept + * together. So no other block can be moved in between the child blocks. Furthermore, + * variables in a block which are not in a child block will be left untouched. + *

+ * Example: Lets assume we have a BDD with the variable ordering {@code v1, v2, v3, v4, v5, v6, v7}. + * We create the following blocks: + *

+ * This means that the variables of {@code A} and {@code B} can never be mixed up in the order. + * So during reordering the variables {@code v6} and {@code v7} can either be moved to the + * front (before {@code A}) or remain at their position. + * Furthermore, for example {@code v1} and {@code v2} will always stay together and neither + * {@code v3} nor any other variable can be moved in between them. On the other hand, the blocks + * {@code A1}, {@code A2}, and {@code A3} can be swapped arbitrarily. + *

+ * These are valid result of a reordering based on the above blocks: + *

+ * These however would be illegal: + * + *

+ * If a block is fixed (the example above assumed always blocks which are not fixed), its + * immediate child blocks will remain in their order. E.g. if block {@code A} was fixed, the blocks + * {@code A1}, {@code A2}, and {@code A3} would not be allowed to be swapped. + * Let's assume block {@code A} to be fixed and that we have two other unfixed blocks: + *

+ * These are examples for legal reorderings: + * + * These are examples for illegal reorderings: + * + *

+ * Each block (including all nested blocks) must be defined by a separate call to this method. The blocks + * may be added in an arbitrary order, so it is not required to add them top-down or bottom-up. + * However, the blocks must not intersect, except of one block containing the other. Furthermore, + * both the {@code first} and the {@code last} variable must be known by the kernel and the level {@code first} + * must be lower than the level of {@code last}. + * @param first the variable at which the block starts (inclusive) + * @param last the variable at which the block ends (inclusive) + * @param fixed whether the block should be fixed or not + */ + public void addVariableBlock(final int first, final int last, final boolean fixed) { + this.reordering.addVariableBlock(first, last, fixed); + } + + /** + * Adds a variable block starting at variable {@code first} and ending in variable + * {@code last} (both inclusive). + *

+ * See {@link #addVariableBlock(int, int, boolean)} for details. + * @param first the variable at which the block starts (inclusive) + * @param last the variable at which the block ends (inclusive) + * @param fixed whether the block should be fixed or not + * @see #addVariableBlock(int, int, boolean) + */ + public void addVariableBlock(final Variable first, final Variable last, final boolean fixed) { + addVariableBlock(getIndexForVariable(first), getIndexForVariable(last), fixed); + } + + /** + * Adds a single variable block for all variables known by the kernel. + */ + public void addAllVariablesAsBlock() { + this.reordering.addAllVariablesAsBlock(); + } + + /** + * Reorders the levels in the kernel using the given reordering method. + * Only blocks of variables will be reordered. See the documentation of + * {@link #addVariableBlock} to learn more about such variable blocks. + * Without the definition of any block, nothing will be reordered. + *

+ * If the reordering should be performed without any restrictions, + * {@link #addAllVariablesAsBlock()} can be called before this method. + * @param method the method to be used for the reordering + */ + public void reorder(final BDDReorderingMethod method) { + this.reordering.reorder(method); + } + protected int doWithPotentialReordering(final BddOperation operation) { try { initRef(); @@ -601,7 +752,7 @@ protected void nodeResize(final boolean doRehash) { if (this.nodesize > oldsize + this.maxnodeincrease) { this.nodesize = oldsize + this.maxnodeincrease; } - this.nodesize = prime.primeLTE(this.nodesize); + this.nodesize = this.prime.primeLTE(this.nodesize); final int[] newnodes = new int[this.nodesize * 6]; System.arraycopy(this.nodes, 0, newnodes, 0, this.nodes.length); this.nodes = newnodes; @@ -862,6 +1013,6 @@ protected interface BddOperation { } public BDDPrime getPrime() { - return prime; + return this.prime; } } diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java index 58fff4f5..9b39324e 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java @@ -47,11 +47,11 @@ *

* The last two operations only have an effect, if variable blocks were added. {@link #addVariableBlock(int, int, boolean) The docuentation} * gives more information on variable blocks. - * To make all variables freely movable, {@link #addVariableBlockAll()} can be used. + * To make all variables freely movable, {@link #addAllVariablesAsBlock()} can be used. * @version 2.0.0 * @since 2.0.0 */ @@ -101,7 +101,7 @@ protected void init() { this.reorderDisabled = false; this.varTree = null; clrVarBlocks(); - setReorderDuringConstruction(BDDReorderingMethod.BDD_REORDER_NONE, 0); + activateReorderDuringConstruction(BDDReorderingMethod.BDD_REORDER_NONE, 0); this.usednumBefore = this.usednumAfter = 0; this.blockId = 0; } @@ -165,7 +165,7 @@ public void swapVariables(int v1, int v2) { * Without the definition of any block, nothing will be reordered. *

* If the reordering should be performed without any restrictions, - * {@link #addVariableBlockAll()} can be called before this method. + * {@link #addAllVariablesAsBlock()} can be called before this method. * @param method the method to be used for the reordering */ public void reorder(final BDDReorderingMethod method) { @@ -201,8 +201,23 @@ public void reorder(final BDDReorderingMethod method) { * given method. The reordering is executed at most {@code num} times. * @param method the method to be used for reordering * @param num the maximum number of reorders to be performed + * @deprecated use {@link BDDKernel#activateReorderDuringConstruction} instead */ + @Deprecated public void setReorderDuringConstruction(final BDDReorderingMethod method, final int num) { + activateReorderDuringConstruction(method, num); + } + + /** + * Activates or deactivates the automatic reordering during the construction of a BDD. + *

+ * Automatic reordering can be deactivated by passing {@link BDDReorderingMethod#BDD_REORDER_NONE} + * for the {@code method} parameter, otherwise the reordering is activated with the + * given method. The reordering is executed at most {@code num} times. + * @param method the method to be used for reordering + * @param num the maximum number of reorders to be performed + */ + protected void activateReorderDuringConstruction(final BDDReorderingMethod method, final int num) { this.reorderMethod = method; this.bddreorderTimes = num; } @@ -213,7 +228,7 @@ public void setReorderDuringConstruction(final BDDReorderingMethod method, final *

* Variable blocks are used in the {@link #reorder BDD reordering} * or in the automatic reordering during the construction of the BDD (configured by - * {@link #setReorderDuringConstruction}). Variable blocks can be nested, i.e. one block can + * {@link #activateReorderDuringConstruction}). Variable blocks can be nested, i.e. one block can * contain an arbitrary number of ("child") blocks. Furthermore, a variable block can also * be a single variable. *

@@ -292,12 +307,21 @@ public void addVariableBlock(final int first, final int last, final boolean fixe /** * Adds a single variable block for all variables known by the kernel. */ - public void addVariableBlockAll() { + public void addAllVariablesAsBlock() { for (int n = 0; n < this.k.varnum; n++) { addVariableBlock(n, n, false); } } + /** + * Adds a single variable block for all variables known by the kernel. + * @deprecated use {@link #addAllVariablesAsBlock()} instead + */ + @Deprecated + public void addVariableBlockAll() { + addAllVariablesAsBlock(); + } + /** * IMPORTANT: * The semantics of the "level" field in the BddNode struct changes during diff --git a/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java b/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java index 142325ed..858f8f6d 100644 --- a/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java @@ -105,15 +105,15 @@ public void testSwapping() throws ParserException { final Formula formula = this.f.parse("a | b | c"); final BDD bdd = BDDFactory.build(formula, kernel); assertThat(bdd.getVariableOrder()).containsExactly(this.A, this.B, this.C); - bdd.swapVariables(this.A, this.B); + kernel.swapVariables(this.A, this.B); assertThat(bdd.getVariableOrder()).containsExactly(this.B, this.A, this.C); - bdd.swapVariables(this.A, this.B); + kernel.swapVariables(this.A, this.B); assertThat(bdd.getVariableOrder()).containsExactly(this.A, this.B, this.C); - bdd.swapVariables(this.A, this.A); + kernel.swapVariables(this.A, this.A); assertThat(bdd.getVariableOrder()).containsExactly(this.A, this.B, this.C); - bdd.swapVariables(this.A, this.C); + kernel.swapVariables(this.A, this.C); assertThat(bdd.getVariableOrder()).containsExactly(this.C, this.B, this.A); - bdd.swapVariables(this.B, this.C); + kernel.swapVariables(this.B, this.C); assertThat(bdd.getVariableOrder()).containsExactly(this.B, this.C, this.A); assertThat(this.f.equivalence(formula, bdd.cnf()).holds(new TautologyPredicate(this.f))).isTrue(); assertThat(bdd.apply(LngBDDFunction.get())).isEqualTo( @@ -122,7 +122,7 @@ public void testSwapping() throws ParserException { new BDDInnerNode(this.A, BDDConstant.getFalsumNode(this.f), BDDConstant.getVerumNode(this.f)), BDDConstant.getVerumNode(this.f)), BDDConstant.getVerumNode(this.f))); - assertThatThrownBy(() -> bdd.swapVariables(this.B, this.X)).isInstanceOf(IllegalArgumentException.class); + assertThatThrownBy(() -> kernel.swapVariables(this.B, this.X)).isInstanceOf(IllegalArgumentException.class); } @Test @@ -137,7 +137,7 @@ public void testSwappingMultipleBdds() throws ParserException { assertThat(bdd2.apply(LngBDDFunction.get())).isEqualTo( new BDDInnerNode(this.A, BDDConstant.getFalsumNode(this.f), new BDDInnerNode(this.B, BDDConstant.getFalsumNode(this.f), BDDConstant.getVerumNode(this.f)))); - bdd1.swapVariables(this.A, this.B); + kernel.swapVariables(this.A, this.B); assertThat(bdd1.getVariableOrder()).containsExactly(this.B, this.A, this.C); assertThat(bdd2.getVariableOrder()).containsExactly(this.B, this.A, this.C); assertThat(bdd2.apply(LngBDDFunction.get())).isEqualTo( @@ -156,8 +156,8 @@ public void testReorderingAndFormulaGeneration() throws ParserException { final BDDKernel kernel = new BDDKernel(this.f, order, 100, 100); final BDD bdd1 = BDDFactory.build(formula1, kernel); final BDD bdd2 = BDDFactory.build(formula2, kernel); - kernel.getReordering().addVariableBlockAll(); - kernel.getReordering().reorder(method); + kernel.addAllVariablesAsBlock(); + kernel.reorder(method); final BDD bdd3 = BDDFactory.build(formula3, kernel); assertThat(bdd1.toFormula().isEquivalentTo(formula1)).isTrue(); @@ -180,7 +180,7 @@ public void testSwappingAndFormulaGeneration() throws ParserException { assertThat(bdd1.toFormula()).isEqualTo(this.f.parse("~a & (~b & c | b) | a")); assertThat(bdd2.toFormula()).isEqualTo(this.f.parse("~a | a & (~b & ~d | b & (~c | c & ~d))")); - bdd1.swapVariables(this.f.variable("a"), this.f.variable("b")); // also affects bdd2 and upcoming bdd3 + kernel.swapVariables(this.f.variable("a"), this.f.variable("b")); // also affects bdd2 and upcoming bdd3 assertThat(bdd1.toFormula()).isEqualTo(this.f.parse("~b & (~a & c | a) | b")); assertThat(bdd2.toFormula()).isEqualTo(this.f.parse("~b & (~a | a & ~d) | b & (~a | a & (~c | c & ~d))")); @@ -188,7 +188,7 @@ public void testSwappingAndFormulaGeneration() throws ParserException { final BDD bdd3 = BDDFactory.build(formula3, kernel); assertThat(bdd3.toFormula()).isEqualTo(this.f.parse("~b & (~c & ~f | c & (~d | d & ~f)) | b & (~a & (~c & ~f | c & (~d | d & ~f)) | a & (~c & f | c & d & f))")); - bdd3.swapVariables(this.f.variable("a"), this.f.variable("d")); + kernel.swapVariables(this.f.variable("a"), this.f.variable("d")); assertThat(bdd1.toFormula()).isEqualTo(this.f.parse("~b & (~c & a | c) | b")); assertThat(bdd2.toFormula()).isEqualTo(this.f.parse("~b & (~d | d & ~a) | b & (~d | d & (~c | c & ~a))")); @@ -251,7 +251,7 @@ private void performReorder(final FormulaFactory f, final Formula formula, final final int usedBefore = new BDDOperations(kernel).nodeCount(bdd.index()); final long start = System.currentTimeMillis(); addVariableBlocks(formula.variables().size(), withBlocks, kernel); - kernel.getReordering().reorder(reorderMethod); + kernel.reorder(reorderMethod); final long duration = System.currentTimeMillis() - start; final int usedAfter = new BDDOperations(kernel).nodeCount(bdd.index()); assertThat(verifyBddConsistency(f, formula, bdd, count)).isTrue(); @@ -266,21 +266,20 @@ private void performReorder(final FormulaFactory f, final Formula formula, final } private void addVariableBlocks(final int numVars, final boolean withBlocks, final BDDKernel kernel) { - final BDDReordering reordering = kernel.getReordering(); if (withBlocks) { - reordering.addVariableBlockAll(); - reordering.addVariableBlock(0, 20, true); - reordering.addVariableBlock(0, 10, false); - reordering.addVariableBlock(11, 20, false); - reordering.addVariableBlock(15, 19, false); - reordering.addVariableBlock(15, 17, true); - reordering.addVariableBlock(18, 19, false); - reordering.addVariableBlock(21, numVars - 1, false); + kernel.addAllVariablesAsBlock(); + kernel.addVariableBlock(0, 20, true); + kernel.addVariableBlock(0, 10, false); + kernel.addVariableBlock(11, 20, false); + kernel.addVariableBlock(15, 19, false); + kernel.addVariableBlock(15, 17, true); + kernel.addVariableBlock(18, 19, false); + kernel.addVariableBlock(21, numVars - 1, false); if (numVars > 33) { - reordering.addVariableBlock(30, 33, false); + kernel.addVariableBlock(30, 33, false); } } else { - reordering.addVariableBlockAll(); + kernel.addAllVariablesAsBlock(); } } @@ -310,7 +309,7 @@ private void reorderOnBuild(final FormulaFactory f, final Formula formula, final final boolean verbose) { final BDDKernel kernel = new BDDKernel(f, new ArrayList<>(formula.variables()), 1000, 10000); addVariableBlocks(formula.variables().size(), withBlocks, kernel); - kernel.getReordering().setReorderDuringConstruction(method, 10000); + kernel.activateReorderDuringConstruction(method, 10000); final long start = System.currentTimeMillis(); final BDD bdd = BDDFactory.build(formula, kernel); final long duration = System.currentTimeMillis() - start;