nodes();
+}
diff --git a/src/main/java/org/logicng/bdds/io/BDDDotFileWriter.java b/src/main/java/org/logicng/bdds/io/BDDDotFileWriter.java
new file mode 100644
index 00000000..217c659d
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/io/BDDDotFileWriter.java
@@ -0,0 +1,101 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2018 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.io;
+
+import org.logicng.bdds.BDDFactory;
+import org.logicng.bdds.datastructures.BDD;
+
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileOutputStream;
+import java.io.IOException;
+import java.io.OutputStreamWriter;
+import java.nio.charset.Charset;
+
+/**
+ * A dot file writer for BDDs. Writes the internal data structure of a BDD to a dot file.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public final class BDDDotFileWriter {
+
+ /**
+ * Private constructor.
+ */
+ private BDDDotFileWriter() {
+ // Intentionally left empty.
+ }
+
+ /**
+ * Writes a given BDD as a dot file.
+ * @param fileName the file name of the dot file to write
+ * @param bdd the BDD
+ * @throws IOException if there was a problem writing the file
+ */
+ public static void write(final String fileName, final BDD bdd) throws IOException {
+ write(new File(fileName.endsWith(".dot") ? fileName : fileName + ".dot"), bdd);
+ }
+
+ /**
+ * Writes a given formula's internal data structure as a dot file.
+ * @param file the file of the dot file to write
+ * @param bdd the BDD
+ * @throws IOException if there was a problem writing the file
+ */
+ public static void write(final File file, final BDD bdd) throws IOException {
+ final StringBuilder sb = new StringBuilder("digraph G {\n");
+ if (!bdd.isContradiction()) {
+ sb.append(" const_true [shape=box, label=\"$true\", style = bold, color = darkgreen];\n");
+ }
+ if (!bdd.isTautology()) {
+ sb.append(" const_false [shape=box, label=\"$false\", style = bold, color = red];\n");
+ }
+ for (final BDDFactory.InternalBDDNode internalNode : bdd.internalNodes()) {
+ sb.append(String.format(" id_%d [shape=ellipse, label=\"%s\"];%n", internalNode.nodenum(), internalNode.label()));
+ sb.append(String.format(" id_%d -> %s [style = dotted, color = red];%n", internalNode.nodenum(), getNodeString(internalNode.low())));
+ sb.append(String.format(" id_%d -> %s [color = darkgreen];%n", internalNode.nodenum(), getNodeString(internalNode.high())));
+ }
+ sb.append("}\n");
+ try (final BufferedWriter writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), Charset.forName("UTF-8")))) {
+ writer.append(sb);
+ writer.flush();
+ }
+ }
+
+ private static String getNodeString(final int i) {
+ switch (i) {
+ case 0:
+ return "const_false";
+ case 1:
+ return "const_true";
+ default:
+ return "id_" + i;
+ }
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/jbuddy/BDDCache.java b/src/main/java/org/logicng/bdds/jbuddy/BDDCache.java
new file mode 100644
index 00000000..839722e5
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/jbuddy/BDDCache.java
@@ -0,0 +1,106 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2018 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+/*========================================================================
+ Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+ All rights reserved
+
+Permission is hereby granted, without written agreement and without
+license or royalty fees, to use, reproduce, prepare derivative
+works, distribute, and display this software and its documentation
+for any purpose, provided that (1) the above copyright notice and
+the following two paragraphs appear in all copies of the source code
+and (2) redistributions, including without limitation binaries,
+reproduce these notices in the supporting documentation. Substantial
+modifications to this software may be copyrighted by their authors
+and need not follow the licensing terms described here, provided
+that the new terms are clearly indicated in all files where they apply.
+
+IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+MODIFICATIONS.
+========================================================================*/
+
+package org.logicng.bdds.jbuddy;
+
+/**
+ * BDD Cache.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+final class BDDCache {
+ private BDDCacheEntry[] table;
+
+ /**
+ * Constructs a new BDD cache of a given size (number of entries in the cache).
+ * @param cs the cache size
+ */
+ BDDCache(final int cs) {
+ resize(cs);
+ }
+
+ /**
+ * Resizes the cache to a new number of entries. The old cache entries are removed in this process.
+ * @param ns the new number of entries
+ */
+ private void resize(final int ns) {
+ final int size = BDDPrime.primeGTE(ns);
+ this.table = new BDDCacheEntry[size];
+ for (int n = 0; n < size; n++)
+ this.table[n] = new BDDCacheEntry();
+ }
+
+ /**
+ * Resets (clears) the cache.
+ */
+ void reset() {
+ for (final BDDCacheEntry ce : this.table)
+ ce.reset();
+ }
+
+ /**
+ * Looks up a given hash value in the cache and returns the respective cache entry.
+ *
+ * The return value is guaranteed to be non-null since every entry in the cache is always a {@link BDDCacheEntry}
+ * object.
+ * @param hash the hash value.
+ * @return the respective entry in the cache
+ */
+ BDDCacheEntry lookup(final int hash) {
+ return this.table[Math.abs(hash % this.table.length)];
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/jbuddy/BDDCacheEntry.java b/src/main/java/org/logicng/bdds/jbuddy/BDDCacheEntry.java
new file mode 100644
index 00000000..9e0e8ed5
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/jbuddy/BDDCacheEntry.java
@@ -0,0 +1,87 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2018 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+/*========================================================================
+ Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+ All rights reserved
+
+Permission is hereby granted, without written agreement and without
+license or royalty fees, to use, reproduce, prepare derivative
+works, distribute, and display this software and its documentation
+for any purpose, provided that (1) the above copyright notice and
+the following two paragraphs appear in all copies of the source code
+and (2) redistributions, including without limitation binaries,
+reproduce these notices in the supporting documentation. Substantial
+modifications to this software may be copyrighted by their authors
+and need not follow the licensing terms described here, provided
+that the new terms are clearly indicated in all files where they apply.
+
+IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+MODIFICATIONS.
+========================================================================*/
+
+package org.logicng.bdds.jbuddy;
+
+import java.math.BigDecimal;
+
+/**
+ * An entry in the BDD cache.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+final class BDDCacheEntry {
+ int a;
+ int b;
+ int c;
+ BigDecimal bdres;
+ int res;
+
+ /**
+ * Constructs a new BDD cache entry.
+ */
+ BDDCacheEntry() {
+ this.reset();
+ }
+
+ /**
+ * Resets this BDD cache entry.
+ */
+ void reset() {
+ this.a = -1;
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/jbuddy/BDDKernel.java b/src/main/java/org/logicng/bdds/jbuddy/BDDKernel.java
new file mode 100644
index 00000000..7d3e0dd2
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/jbuddy/BDDKernel.java
@@ -0,0 +1,1258 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2018 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+/*========================================================================
+ Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+ All rights reserved
+
+Permission is hereby granted, without written agreement and without
+license or royalty fees, to use, reproduce, prepare derivative
+works, distribute, and display this software and its documentation
+for any purpose, provided that (1) the above copyright notice and
+the following two paragraphs appear in all copies of the source code
+and (2) redistributions, including without limitation binaries,
+reproduce these notices in the supporting documentation. Substantial
+modifications to this software may be copyrighted by their authors
+and need not follow the licensing terms described here, provided
+that the new terms are clearly indicated in all files where they apply.
+
+IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+MODIFICATIONS.
+========================================================================*/
+
+package org.logicng.bdds.jbuddy;
+
+import java.math.BigDecimal;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.LinkedList;
+import java.util.List;
+
+/**
+ * The jBuddy kernel.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public final class BDDKernel {
+
+ public static final int BDD_TRUE = 1;
+ public static final int BDD_FALSE = 0;
+
+ private static final int MAXVAR = 0x1FFFFF;
+ private static final int MAXREF = 0x3FF;
+ private static final int MARKON = 0x200000;
+ private static final int MARKOFF = 0x1FFFFF;
+
+ private byte[] allunsatProfile;
+
+ private enum Operand {
+ AND(0, new int[]{0, 0, 0, 1}),
+ OR(2, new int[]{0, 1, 1, 1}),
+ IMP(5, new int[]{1, 1, 0, 1}),
+ EQUIV(6, new int[]{1, 0, 0, 1}),
+ NOT(10, new int[]{1, 1, 0, 0});
+
+ private final int v;
+ private final int[] tt;
+
+ Operand(final int value, final int[] truthTable) {
+ this.v = value;
+ this.tt = truthTable;
+ }
+ }
+
+ private static final int CACHEID_RESTRICT = 0x1;
+ private static final int CACHEID_SATCOU = 0x2;
+ private static final int CACHEID_PATHCOU_ONE = 0x4;
+ private static final int CACHEID_PATHCOU_ZERO = 0x8;
+ private static final int CACHEID_FORALL = 0x1;
+
+ private BddNode[] nodes; // All of the bdd nodes
+ private int[] vars; // Set of defined BDD variables
+ private final int minfreenodes; // Minimal % of nodes that has to be left after a garbage collection
+ private int gbcollectnum; // Number of garbage collections
+ private final int cachesize; // Size of the operator caches
+ private int nodesize; // Number of allocated nodes
+ private final int maxnodeincrease; // Max. # of nodes used to inc. table
+ private int freepos; // First free node
+ private int freenum; // Number of free nodes
+ private long produced; // Number of new nodes ever produced
+ private int varnum; // Number of defined BDD variables
+ private int[] refstack; // Internal node reference stack
+ private int refstacktop; // Internal node reference stack top
+ private int[] level2var; // Level -> variable table
+
+ private int[] quantvarset; // Current variable set for quant.
+ private int quantvarsetID; // Current id used in quantvarset
+ private int quantlast; // Current last variable to be quant.
+ private int supportID; // Current ID (true value) for support
+ private int supportMax; // Max. used level in support calc.
+ private int[] supportSet; // The found support set
+
+ private BDDCache applycache; // Cache for apply results
+ private BDDCache itecache; // Cache for ITE results
+ private BDDCache quantcache; // Cache for exist/forall results
+ private BDDCache appexcache; // Cache for appex/appall results
+ private BDDCache replacecache; // Cache for replace results
+ private BDDCache misccache; // Cache for other results
+
+ /**
+ * Constructor for the BDD kernel.
+ * @param initialSize the initial number of nodes in the nodetable
+ * @param cs the fixed size of the internal caches
+ */
+ public BDDKernel(final int initialSize, final int cs) {
+ this.nodesize = BDDPrime.primeGTE(initialSize);
+ this.nodes = new BddNode[this.nodesize];
+ this.minfreenodes = 20;
+ for (int n = 0; n < this.nodesize; n++) {
+ this.nodes[n] = new BddNode();
+ this.nodes[n].refcou = 0;
+ this.nodes[n].low = -1;
+ this.nodes[n].hash = 0;
+ this.nodes[n].level = 0;
+ this.nodes[n].next = n + 1;
+ }
+ this.nodes[this.nodesize - 1].next = 0;
+ this.nodes[0].refcou = MAXREF;
+ this.nodes[1].refcou = MAXREF;
+ this.nodes[0].low = 0;
+ this.nodes[0].high = 0;
+ this.nodes[1].low = 1;
+ this.nodes[1].high = 1;
+ initOperators(cs);
+ this.freepos = 2;
+ this.freenum = this.nodesize - 2;
+ this.varnum = 0;
+ this.gbcollectnum = 0;
+ this.cachesize = cs;
+ this.maxnodeincrease = 50000;
+ // bdd_fdd_init();
+ }
+
+ /**
+ * Sets the number of variables to use. It may be called more than one time, but only
+ * to increase the number of variables.
+ * @param num the number of variables to use
+ */
+ public void setNumberOfVars(final int num) {
+ if (this.varnum != 0)
+ throw new UnsupportedOperationException("Variable number is already set. Resetting it is not supported");
+ if (num < 1 || num > MAXVAR)
+ throw new IllegalArgumentException("Invalid variable number: " + num);
+ this.vars = new int[num * 2];
+ this.level2var = new int[num + 1];
+ this.refstack = new int[num * 2 + 4];
+ this.refstacktop = 0;
+ while (this.varnum < num) {
+ this.vars[this.varnum * 2] = pushRef(makeNode(this.varnum, 0, 1));
+ this.vars[this.varnum * 2 + 1] = makeNode(this.varnum, 1, 0);
+ popref(1);
+ this.nodes[this.vars[this.varnum * 2]].refcou = MAXREF;
+ this.nodes[this.vars[this.varnum * 2 + 1]].refcou = MAXREF;
+ this.level2var[this.varnum] = this.varnum;
+ this.varnum++;
+ }
+ this.nodes[0].level = num;
+ this.nodes[1].level = num;
+ this.level2var[num] = num;
+ varResize();
+ }
+
+ /**
+ * Returns a BDD representing the i-th variable (one node with the children true and false).
+ * @param i the index i
+ * @return the BDD representing the i-th variable
+ * @throws IllegalArgumentException if the index is not within the range of variables
+ */
+ public int ithVar(final int i) {
+ if (i < 0 || i >= this.varnum)
+ throw new IllegalArgumentException("Illegal variable number: " + i);
+ return this.vars[i * 2];
+ }
+
+ /**
+ * Returns a BDD representing the negation of the i-th variable (one node with the children true and false).
+ * @param i the index i
+ * @return the BDD representing the negated i-th variable
+ * @throws IllegalArgumentException if the index is not within the range of variables
+ */
+ public int nithVar(final int i) {
+ if (i < 0 || i >= this.varnum)
+ throw new IllegalArgumentException("Illegal variable number: " + i);
+ return this.vars[i * 2 + 1];
+ }
+
+ /**
+ * Returns the variable index labeling the given root node.
+ * @param root the root node of the BDD
+ * @return the variable index
+ */
+ public int bddVar(final int root) {
+ if (root < 2)
+ throw new IllegalArgumentException("Illegal node number: " + root);
+ return (this.level2var[level(root)]);
+ }
+
+ /**
+ * Returns the false branch of the given root node.
+ * @param root the root node of the BDD
+ * @return the false branch
+ */
+ public int bddLow(final int root) {
+ if (root < 2)
+ throw new IllegalArgumentException("Illegal node number: " + root);
+ return (low(root));
+ }
+
+ /**
+ * Returns the true branch of the given root node.
+ * @param root the root node of the BDD
+ * @return the true branch
+ */
+ public int bddHigh(final int root) {
+ if (root < 2)
+ throw new IllegalArgumentException("Illegal node number: " + root);
+ return (high(root));
+ }
+
+ /**
+ * Returns the conjunction of two BDDs.
+ * @param l the first BDD
+ * @param r the second BDD
+ * @return the conjunction of the two BDDs
+ */
+ public int and(final int l, final int r) {
+ return apply(l, r, Operand.AND);
+ }
+
+ /**
+ * Returns the disjunction of two BDDs.
+ * @param l the first BDD
+ * @param r the second BDD
+ * @return the disjunction of the two BDDs
+ */
+ public int or(final int l, final int r) {
+ return apply(l, r, Operand.OR);
+ }
+
+ /**
+ * Returns the implication of two BDDs.
+ * @param l the first BDD
+ * @param r the second BDD
+ * @return the implication of the two BDDs
+ */
+ public int implication(final int l, final int r) {
+ return apply(l, r, Operand.IMP);
+ }
+
+ /**
+ * Returns the equivalence of two BDDs.
+ * @param l the first BDD
+ * @param r the second BDD
+ * @return the equivalence of the two BDDs
+ */
+ public int equivalence(final int l, final int r) {
+ return apply(l, r, Operand.EQUIV);
+ }
+
+ private int apply(final int l, final int r, final Operand op) {
+ final int res;
+ initRef();
+ res = applyRec(l, r, op);
+ return res;
+ }
+
+ private int applyRec(final int l, final int r, final Operand op) {
+ final int res;
+ switch (op) {
+ case AND:
+ if (l == r)
+ return l;
+ if (isZero(l) || isZero(r))
+ return 0;
+ if (isOne(l))
+ return r;
+ if (isOne(r))
+ return l;
+ break;
+ case OR:
+ if (l == r)
+ return l;
+ if (isOne(l) || isOne(r))
+ return 1;
+ if (isZero(l))
+ return r;
+ if (isZero(r))
+ return l;
+ break;
+ case IMP:
+ if (isZero(l))
+ return 1;
+ if (isOne(l))
+ return r;
+ if (isOne(r))
+ return 1;
+ break;
+ }
+ if (isConst(l) && isConst(r))
+ res = op.tt[l << 1 | r];
+ else {
+ final BDDCacheEntry entry = this.applycache.lookup(triple(l, r, op.v));
+ if (entry.a == l && entry.b == r && entry.c == op.v)
+ return entry.res;
+ if (level(l) == level(r)) {
+ pushRef(applyRec(low(l), low(r), op));
+ pushRef(applyRec(high(l), high(r), op));
+ res = makeNode(level(l), readRef(2), readRef(1));
+ } else if (level(l) < level(r)) {
+ pushRef(applyRec(low(l), r, op));
+ pushRef(applyRec(high(l), r, op));
+ res = makeNode(level(l), readRef(2), readRef(1));
+ } else {
+ pushRef(applyRec(l, low(r), op));
+ pushRef(applyRec(l, high(r), op));
+ res = makeNode(level(r), readRef(2), readRef(1));
+ }
+ popref(2);
+ entry.a = l;
+ entry.b = r;
+ entry.c = op.v;
+ entry.res = res;
+ }
+ return res;
+ }
+
+ /**
+ * Returns the negation of a BDD.
+ * @param r the BDD
+ * @return the negation of the BDD
+ */
+ public int not(final int r) {
+ final int res;
+ initRef();
+ res = notRec(r);
+ return res;
+ }
+
+ private int notRec(final int r) {
+ if (isZero(r))
+ return BDDKernel.BDD_TRUE;
+ if (isOne(r))
+ return BDDKernel.BDD_FALSE;
+ final BDDCacheEntry entry = this.applycache.lookup(r);
+ if (entry.a == r && entry.c == Operand.NOT.v)
+ return entry.res;
+ pushRef(notRec(low(r)));
+ pushRef(notRec(high(r)));
+ final int res = makeNode(level(r), readRef(2), readRef(1));
+ popref(2);
+ entry.a = r;
+ entry.c = Operand.NOT.v;
+ entry.res = res;
+ return res;
+ }
+
+ /**
+ * Adds a reference for a given node. Reference counting is done on externally referenced nodes only and the count for
+ * a specific node {@code r} can and must be increased using this function to avoid loosing the node in the next
+ * garbage collection.
+ * @param root the node
+ * @return return the node
+ * @throws IllegalArgumentException if the root node was invalid
+ */
+ public int addRef(final int root) {
+ if (root < 2)
+ return root;
+ if (root >= this.nodesize)
+ throw new IllegalArgumentException("Not a valid BDD root node: " + root);
+ if (low(root) == -1)
+ throw new IllegalArgumentException("Not a valid BDD root node: " + root);
+ incRef(root);
+ return root;
+ }
+
+ /**
+ * Deletes a reference for a given node.
+ * @param root the node
+ * @throws IllegalArgumentException if the root node was invalid
+ */
+ private void delRef(final int root) {
+ if (root < 2)
+ return;
+ if (root >= this.nodesize)
+ throw new IllegalStateException("Cannot dereference a variable > varnum");
+ if (this.low(root) == -1)
+ throw new IllegalStateException("Cannot dereference variable -1");
+ if (!this.hasref(root))
+ throw new IllegalStateException("Cannot dereference a variable which has no reference");
+ this.decRef(root);
+ }
+
+ private void decRef(final int n) {
+ if (this.nodes[n].refcou != MAXREF && this.nodes[n].refcou > 0)
+ this.nodes[n].refcou--;
+ }
+
+ private void incRef(final int n) {
+ if (this.nodes[n].refcou < MAXREF)
+ this.nodes[n].refcou++;
+ }
+
+ /**
+ * Returns all nodes for a given root node in their internal representation. The internal representation is stored
+ * in an array: {@code [node number, variable, low, high]}
+ * @param r the BDD root node
+ * @return all Nodes in their internal representation
+ */
+ public List allNodes(final int r) {
+ final List result = new ArrayList<>();
+ if (r < 2)
+ return result;
+ mark(r);
+ for (int n = 0; n < this.nodesize; n++) {
+ if ((level(n) & MARKON) != 0) {
+ final BddNode node = this.nodes[n];
+ node.level &= MARKOFF;
+ result.add(new int[]{n, this.level2var[node.level], node.low, node.high});
+ }
+ }
+ return result;
+ }
+
+ private int makeNode(final int level, final int low, final int high) {
+ final BddNode node;
+ if (low == high)
+ return low;
+ int hash = nodehash(level, low, high);
+ int res = this.nodes[hash].hash;
+ while (res != 0) {
+ if (level(res) == level && low(res) == low && high(res) == high)
+ return res;
+ res = this.nodes[res].next;
+ }
+ if (this.freepos == 0) {
+ gbc();
+ if ((this.freenum * 100) / this.nodesize <= this.minfreenodes) {
+ nodeResize();
+ hash = nodehash(level, low, high);
+ }
+ if (this.freepos == 0)
+ throw new IllegalStateException("Cannot allocate more space for more nodes.");
+ }
+ res = this.freepos;
+ this.freepos = this.nodes[this.freepos].next;
+ this.freenum--;
+ this.produced++;
+ node = this.nodes[res];
+ node.level = level;
+ node.low = low;
+ node.high = high;
+ node.next = this.nodes[hash].hash;
+ this.nodes[hash].hash = res;
+ return res;
+ }
+
+ private void unmark(final int i) {
+ if (i < 2)
+ return;
+ final BddNode node = this.nodes[i];
+ if (!markedNode(node) || node.low == -1)
+ return;
+ unmarkNode(node);
+ unmark(node.low);
+ unmark(node.high);
+ }
+
+ private int markCount(final int i) {
+ if (i < 2)
+ return 0;
+ final BddNode node = this.nodes[i];
+ if (markedNode(node) || node.low == -1)
+ return 0;
+ setMarkNode(node);
+ int count = 1;
+ count += markCount(node.low);
+ count += markCount(node.high);
+ return count;
+ }
+
+ private void gbc() {
+ int r;
+ for (r = 0; r < this.refstacktop; r++)
+ mark(this.refstack[r]);
+ for (int n = 0; n < this.nodesize; n++) {
+ if (this.nodes[n].refcou > 0)
+ mark(n);
+ this.nodes[n].hash = 0;
+ }
+ this.freepos = 0;
+ this.freenum = 0;
+ for (int n = this.nodesize - 1; n >= 2; n--) {
+ final BddNode node = this.nodes[n];
+ if ((node.level & MARKON) != 0 && node.low != -1) {
+ node.level &= MARKOFF;
+ final int hash = nodehash(node.level, node.low, node.high);
+ node.next = this.nodes[hash].hash;
+ this.nodes[hash].hash = n;
+ } else {
+ node.low = -1;
+ node.next = this.freepos;
+ this.freepos = n;
+ this.freenum++;
+ }
+ }
+ resetCaches();
+ this.gbcollectnum++;
+ }
+
+ private void gbcRehash() {
+ this.freepos = 0;
+ this.freenum = 0;
+ for (int n = this.nodesize - 1; n >= 2; n--) {
+ final BddNode node = this.nodes[n];
+ if (node.low != -1) {
+ final int hash = nodehash(node.level, node.low, node.high);
+ node.next = this.nodes[hash].hash;
+ this.nodes[hash].hash = n;
+ } else {
+ node.next = this.freepos;
+ this.freepos = n;
+ this.freenum++;
+ }
+ }
+ }
+
+ private void mark(final int i) {
+ if (i < 2)
+ return;
+ if ((level(i) & MARKON) != 0 || low(i) == -1)
+ return;
+ this.nodes[i].level |= MARKON;
+ mark(low(i));
+ mark(high(i));
+ }
+
+ private void nodeResize() {
+ final int oldsize = this.nodesize;
+ int n;
+ this.nodesize = this.nodesize << 1;
+ if (this.nodesize > oldsize + this.maxnodeincrease)
+ this.nodesize = oldsize + this.maxnodeincrease;
+ this.nodesize = BDDPrime.primeLTE(this.nodesize);
+ final BddNode[] newnodes = new BddNode[this.nodesize];
+ System.arraycopy(this.nodes, 0, newnodes, 0, this.nodes.length);
+ for (int i = oldsize; i < newnodes.length; i++)
+ newnodes[i] = new BddNode();
+ this.nodes = newnodes;
+ for (n = 0; n < oldsize; n++)
+ this.nodes[n].hash = 0;
+ for (n = oldsize; n < this.nodesize; n++) {
+ final BddNode nn = this.nodes[n];
+ nn.refcou = 0;
+ nn.hash = 0;
+ nn.level = 0;
+ nn.low = -1;
+ nn.next = n + 1;
+ }
+ this.nodes[this.nodesize - 1].next = this.freepos;
+ this.freepos = oldsize;
+ this.freenum += this.nodesize - oldsize;
+ gbcRehash();
+ }
+
+ private void initRef() {
+ this.refstacktop = 0;
+ }
+
+ private int pushRef(final int a) {
+ this.refstack[this.refstacktop++] = a;
+ return a;
+ }
+
+ private int readRef(final int a) {
+ return this.refstack[this.refstacktop - a];
+ }
+
+ private void popref(final int a) {
+ this.refstacktop -= a;
+ }
+
+ private boolean hasref(final int n) {
+ return this.nodes[n].refcou > 0;
+ }
+
+ private boolean isConst(final int a) {
+ return a < 2;
+ }
+
+ private boolean isOne(final int a) {
+ return a == 1;
+ }
+
+ private boolean isZero(final int a) {
+ return a == 0;
+ }
+
+ private int level(final int a) {
+ return this.nodes[a].level;
+ }
+
+ private int low(final int a) {
+ return this.nodes[a].low;
+ }
+
+ private int high(final int a) {
+ return this.nodes[a].high;
+ }
+
+ private void setMarkNode(final BddNode p) {
+ p.level |= MARKON;
+ }
+
+ private void unmarkNode(final BddNode p) {
+ p.level &= MARKOFF;
+ }
+
+ private boolean markedNode(final BddNode p) {
+ return (p.level & MARKON) != 0;
+ }
+
+ private int nodehash(final int lvl, final int l, final int h) {
+ return Math.abs(triple(lvl, l, h) % this.nodesize);
+ }
+
+ private int pair(final int a, final int b) {
+ return (a + b) * (a + b + 1) / 2 + a;
+ }
+
+ private int triple(final int a, final int b, final int c) {
+ return pair(c, pair(a, b));
+ }
+
+ private void initOperators(final int cachesize) {
+ this.applycache = new BDDCache(cachesize);
+ this.itecache = new BDDCache(cachesize);
+ this.quantcache = new BDDCache(cachesize);
+ this.appexcache = new BDDCache(cachesize);
+ this.replacecache = new BDDCache(cachesize);
+ this.misccache = new BDDCache(cachesize);
+ this.quantvarsetID = 0;
+ this.quantvarset = null;
+ this.supportSet = null;
+ }
+
+ private void resetCaches() {
+ this.applycache.reset();
+ this.itecache.reset();
+ this.quantcache.reset();
+ this.appexcache.reset();
+ this.replacecache.reset();
+ this.misccache.reset();
+ }
+
+ private void varResize() {
+ this.quantvarset = new int[this.varnum];
+ this.quantvarsetID = 0;
+ }
+
+ /**
+ * Restricts the variables in the BDD {@code r} to constants true or false. The restriction is submitted in the BDD
+ * {@code var}.
+ * @param r the BDD to be restricted
+ * @param var the variable mapping as a BDD
+ * @return the restricted BDD
+ */
+ public int restrict(final int r, final int var) {
+ final int res;
+ if (var < 2)
+ return r;
+ varset2svartable(var);
+ initRef();
+ res = restrictRec(r, (var << 3) | CACHEID_RESTRICT);
+ return res;
+ }
+
+ private int restrictRec(final int r, final int miscid) {
+ final int res;
+ if (isConst(r) || level(r) > this.quantlast)
+ return r;
+ final BDDCacheEntry entry = this.misccache.lookup(pair(r, miscid));
+ if (entry.a == r && entry.c == miscid)
+ return entry.res;
+ if (insvarset(level(r))) {
+ if (this.quantvarset[level(r)] > 0)
+ res = restrictRec(high(r), miscid);
+ else
+ res = restrictRec(low(r), miscid);
+ } else {
+ pushRef(restrictRec(low(r), miscid));
+ pushRef(restrictRec(high(r), miscid));
+ res = makeNode(level(r), readRef(2), readRef(1));
+ popref(2);
+ }
+ entry.a = r;
+ entry.c = miscid;
+ entry.res = res;
+ return res;
+ }
+
+ /**
+ * Existential quantifier elimination for the variables in {@code var}.
+ * @param r the BDD root node
+ * @param var the variables to eliminate
+ * @return the BDD with the eliminated variables
+ */
+ public int exists(final int r, final int var) {
+ final int res;
+ if (var < 2)
+ return r;
+ varset2vartable(var);
+ initRef();
+ res = quantRec(r, Operand.OR, var << 3);
+ return res;
+ }
+
+ /**
+ * Universal quantifier elimination for the variables in {@code var}.
+ * @param r the BDD root node
+ * @param var the variables to eliminate
+ * @return the BDD with the eliminated variables
+ */
+ public int forAll(final int r, final int var) {
+ final int res;
+ if (var < 2)
+ return r;
+ varset2vartable(var);
+ initRef();
+ res = quantRec(r, Operand.AND, (var << 3) | CACHEID_FORALL);
+ return res;
+ }
+
+ private int quantRec(final int r, final Operand op, final int quantid) {
+ final int res;
+ if (r < 2 || level(r) > this.quantlast)
+ return r;
+ final BDDCacheEntry entry = this.quantcache.lookup(r);
+ if (entry.a == r && entry.c == quantid)
+ return entry.res;
+ pushRef(quantRec(low(r), op, quantid));
+ pushRef(quantRec(high(r), op, quantid));
+ if (invarset(level(r)))
+ res = applyRec(readRef(2), readRef(1), op);
+ else
+ res = makeNode(level(r), readRef(2), readRef(1));
+ popref(2);
+ entry.a = r;
+ entry.c = quantid;
+ entry.res = res;
+ return res;
+ }
+
+ /**
+ * Finds one satisfying variable assignment and returns it as BDD.
+ * @param r the BDD root node
+ * @return the satisfying variable assignment of the BDD as a BDD itself
+ */
+ public int satOne(final int r) {
+ if (r < 2)
+ return r;
+ initRef();
+ return satOneRec(r);
+ }
+
+ private int satOneRec(final int r) {
+ if (isConst(r))
+ return r;
+ if (isZero(low(r))) {
+ final int res = satOneRec(high(r));
+ return pushRef(makeNode(level(r), BDDKernel.BDD_FALSE, res));
+ } else {
+ final int res = satOneRec(low(r));
+ return pushRef(makeNode(level(r), res, BDDKernel.BDD_FALSE));
+ }
+ }
+
+ /**
+ * Returns an arbitrary model for a given BDD or {@code null} which contains at least the given variables. If a variable
+ * is a don't care variable, it will be assigned with the given default value.
+ * @param r the BDD root node
+ * @param var the set of variable which has to be contained in the model as a BDD
+ * @param pol the default value for don't care variables as a BDD
+ * @return an arbitrary model of this BDD
+ */
+ public int satOneSet(final int r, final int var, final int pol) {
+ if (isZero(r))
+ return r;
+ if (!isConst(pol))
+ throw new IllegalArgumentException("polarity for satOneSet must be a constant");
+ initRef();
+ return satOneSetRec(r, var, pol);
+ }
+
+ private int satOneSetRec(final int r, final int var, final int satPolarity) {
+ if (isConst(r) && isConst(var))
+ return r;
+ if (level(r) < level(var)) {
+ if (isZero(low(r))) {
+ final int res = satOneSetRec(high(r), var, satPolarity);
+ return pushRef(makeNode(level(r), BDDKernel.BDD_FALSE, res));
+ } else {
+ final int res = satOneSetRec(low(r), var, satPolarity);
+ return pushRef(makeNode(level(r), res, BDDKernel.BDD_FALSE));
+ }
+ } else if (level(var) < level(r)) {
+ final int res = satOneSetRec(r, high(var), satPolarity);
+ if (satPolarity == BDDKernel.BDD_TRUE)
+ return pushRef(makeNode(level(var), BDDKernel.BDD_FALSE, res));
+ else
+ return pushRef(makeNode(level(var), res, BDDKernel.BDD_FALSE));
+ } else {
+ if (isZero(low(r))) {
+ final int res = satOneSetRec(high(r), high(var), satPolarity);
+ return pushRef(makeNode(level(r), BDDKernel.BDD_FALSE, res));
+ } else {
+ final int res = satOneSetRec(low(r), high(var), satPolarity);
+ return pushRef(makeNode(level(r), res, BDDKernel.BDD_FALSE));
+ }
+ }
+ }
+
+ /**
+ * Returns a full model in all variables for the given BDD.
+ * @param r the BDD root node
+ * @return a full model of this BDD
+ */
+ public int fullSatOne(final int r) {
+ if (r == 0)
+ return 0;
+ initRef();
+ int res = fullSatOneRec(r);
+ for (int v = level(r) - 1; v >= 0; v--)
+ res = pushRef(makeNode(v, res, 0));
+ return res;
+ }
+
+ private int fullSatOneRec(final int r) {
+ if (r < 2)
+ return r;
+ if (low(r) != 0) {
+ int res = fullSatOneRec(low(r));
+ for (int v = level(low(r)) - 1; v > level(r); v--)
+ res = pushRef(makeNode(v, res, 0));
+ return pushRef(makeNode(level(r), res, 0));
+ } else {
+ int res = fullSatOneRec(high(r));
+ for (int v = level(high(r)) - 1; v > level(r); v--)
+ res = pushRef(makeNode(v, res, 0));
+ return pushRef(makeNode(level(r), 0, res));
+ }
+ }
+
+ /**
+ * Returns all models for a given BDD.
+ * @param r the BDD root node
+ * @return all models for the BDD
+ */
+ public List allSat(final int r) {
+ final byte[] allsatProfile = new byte[this.varnum];
+ for (int v = level(r) - 1; v >= 0; --v)
+ allsatProfile[this.level2var[v]] = -1;
+ initRef();
+ final List allSat = new LinkedList<>();
+ allSatRec(r, allSat, allsatProfile);
+ return allSat;
+ }
+
+ private void allSatRec(final int r, final List models, final byte[] allsatProfile) {
+ if (isOne(r)) {
+ models.add(Arrays.copyOf(allsatProfile, allsatProfile.length));
+ return;
+ }
+ if (isZero(r))
+ return;
+ if (!isZero(low(r))) {
+ allsatProfile[this.level2var[level(r)]] = 0;
+ for (int v = level(low(r)) - 1; v > level(r); --v)
+ allsatProfile[this.level2var[v]] = -1;
+ allSatRec(low(r), models, allsatProfile);
+ }
+ if (!isZero(high(r))) {
+ allsatProfile[this.level2var[level(r)]] = 1;
+ for (int v = level(high(r)) - 1; v > level(r); --v) {
+ allsatProfile[this.level2var[v]] = -1;
+ }
+ allSatRec(high(r), models, allsatProfile);
+ }
+ }
+
+ /**
+ * Returns the model count for the given BDD.
+ * @param r the BDD root node
+ * @return the model count for the BDD
+ */
+ public BigDecimal satCount(final int r) {
+ final BigDecimal size = new BigDecimal(2).pow(level(r));
+ return satCountRec(r, CACHEID_SATCOU).multiply(size);
+ }
+
+ private BigDecimal satCountRec(final int root, final int miscid) {
+ if (root < 2)
+ return new BigDecimal(root);
+ final BDDCacheEntry entry = this.misccache.lookup(root);
+ if (entry.a == root && entry.c == miscid)
+ return entry.bdres;
+ final BDDKernel.BddNode node = this.nodes[root];
+ BigDecimal size = BigDecimal.ZERO;
+ BigDecimal s = BigDecimal.ONE;
+ s = s.multiply(new BigDecimal(2).pow(level(node.low) - node.level - 1));
+ size = size.add(s.multiply(satCountRec(node.low, miscid)));
+ s = BigDecimal.ONE;
+ s = s.multiply(new BigDecimal(2).pow(level(node.high) - node.level - 1));
+ size = size.add(s.multiply(satCountRec(node.high, miscid)));
+ entry.a = root;
+ entry.c = miscid;
+ entry.bdres = size;
+ return size;
+ }
+
+ /**
+ * Returns the number of paths to the terminal node 'one'.
+ * @param r the BDD root node
+ * @return the number of paths to the terminal node 'one'
+ */
+ public BigDecimal pathCountOne(final int r) {
+ return pathCountRecOne(r, CACHEID_PATHCOU_ONE);
+ }
+
+ private BigDecimal pathCountRecOne(final int r, final int miscid) {
+ final BigDecimal size;
+ if (isZero(r))
+ return BigDecimal.ZERO;
+ if (isOne(r))
+ return BigDecimal.ONE;
+ final BDDCacheEntry entry = this.misccache.lookup(r);
+ if (entry.a == r && entry.c == miscid)
+ return entry.bdres;
+ size = pathCountRecOne(low(r), miscid).add(pathCountRecOne(high(r), miscid));
+ entry.a = r;
+ entry.c = miscid;
+ entry.bdres = size;
+ return size;
+ }
+
+ /**
+ * Returns the number of paths to the terminal node 'zero'.
+ * @param r the BDD root node
+ * @return the number of paths to the terminal node 'zero'
+ */
+ public BigDecimal pathCountZero(final int r) {
+ return pathCountRecZero(r, CACHEID_PATHCOU_ZERO);
+ }
+
+ private BigDecimal pathCountRecZero(final int r, final int miscid) {
+ final BigDecimal size;
+ if (isZero(r))
+ return BigDecimal.ONE;
+ if (isOne(r))
+ return BigDecimal.ZERO;
+ final BDDCacheEntry entry = this.misccache.lookup(r);
+ if (entry.a == r && entry.c == miscid)
+ return entry.bdres;
+ size = pathCountRecZero(low(r), miscid).add(pathCountRecZero(high(r), miscid));
+ entry.a = r;
+ entry.c = miscid;
+ entry.bdres = size;
+ return size;
+ }
+
+ /**
+ * Returns all unsatisfiable assignments for a given BDD.
+ * @param r the BDD root node
+ * @return all unsatisfiable assignments for the BDD
+ */
+ public List allUnsat(final int r) {
+ this.allunsatProfile = new byte[this.varnum];
+ for (int v = level(r) - 1; v >= 0; --v)
+ this.allunsatProfile[this.level2var[v]] = -1;
+ initRef();
+ final List allUnsat = new LinkedList<>();
+ allUnsatRec(r, allUnsat);
+ return allUnsat;
+ }
+
+ private void allUnsatRec(final int r, final List models) {
+ if (isZero(r)) {
+ models.add(Arrays.copyOf(this.allunsatProfile, this.allunsatProfile.length));
+ return;
+ }
+ if (isOne(r))
+ return;
+ if (!isOne(low(r))) {
+ this.allunsatProfile[this.level2var[level(r)]] = 0;
+ for (int v = level(low(r)) - 1; v > level(r); --v)
+ this.allunsatProfile[this.level2var[v]] = -1;
+ allUnsatRec(low(r), models);
+ }
+ if (!isOne(high(r))) {
+ this.allunsatProfile[this.level2var[level(r)]] = 1;
+ for (int v = level(high(r)) - 1; v > level(r); --v)
+ this.allunsatProfile[this.level2var[v]] = -1;
+ allUnsatRec(high(r), models);
+ }
+ }
+
+ /**
+ * Returns all the variables that a given BDD depends on.
+ * @param r the BDD root node
+ * @return all the variables that the BDD depends on
+ */
+ public int support(final int r) {
+ final int supportSize = 0;
+ int res = 1;
+ if (r < 2)
+ return BDDKernel.BDD_FALSE;
+ if (supportSize < this.varnum) {
+ this.supportSet = new int[this.varnum];
+ this.supportID = 0;
+ }
+ if (this.supportID == 0x0FFFFFFF)
+ this.supportID = 0;
+ ++this.supportID;
+ final int supportMin = level(r);
+ this.supportMax = supportMin;
+ supportRec(r, this.supportSet);
+ unmark(r);
+
+ for (int n = this.supportMax; n >= supportMin; --n)
+ if (this.supportSet[n] == this.supportID) {
+ addRef(res);
+ final int tmp = makeNode(n, 0, res);
+ delRef(res);
+ res = tmp;
+ }
+ return res;
+ }
+
+ private void supportRec(final int r, final int[] support) {
+ if (r < 2)
+ return;
+ final BDDKernel.BddNode node = this.nodes[r];
+ if ((node.level & BDDKernel.MARKON) != 0 || node.low == -1)
+ return;
+ support[node.level] = this.supportID;
+ if (node.level > this.supportMax)
+ this.supportMax = node.level;
+ node.level |= BDDKernel.MARKON;
+ supportRec(node.low, support);
+ supportRec(node.high, support);
+ }
+
+ /**
+ * Returns the number of nodes for a given BDD.
+ * @param r the BDD root node
+ * @return the number of nodes for the BDD
+ */
+ public int nodeCount(final int r) {
+ final int count = markCount(r);
+ unmark(r);
+ return count;
+ }
+
+ /**
+ * Returns how often each variable occurs in the given BDD.
+ * @param r the BDD root node
+ * @return how often each variable occurs in the BDD
+ */
+ public int[] varProfile(final int r) {
+ final int[] varprofile = new int[this.varnum];
+ varProfileRec(r, varprofile);
+ unmark(r);
+ return varprofile;
+ }
+
+ private void varProfileRec(final int r, final int[] varprofile) {
+ if (r < 2)
+ return;
+ final BDDKernel.BddNode node = this.nodes[r];
+ if ((node.level & BDDKernel.MARKON) != 0)
+ return;
+ varprofile[this.level2var[node.level]]++;
+ node.level |= BDDKernel.MARKON;
+ varProfileRec(node.low, varprofile);
+ varProfileRec(node.high, varprofile);
+ }
+
+ private void varset2svartable(final int r) {
+ if (r < 2)
+ throw new IllegalArgumentException("Illegal variable: " + r);
+ this.quantvarsetID++;
+ if (this.quantvarsetID == Integer.MAX_VALUE / 2) {
+ this.quantvarset = new int[this.varnum];
+ this.quantvarsetID = 1;
+ }
+ for (int n = r; !isConst(n); ) {
+ if (isZero(low(n))) {
+ this.quantvarset[level(n)] = this.quantvarsetID;
+ n = high(n);
+ } else {
+ this.quantvarset[level(n)] = -this.quantvarsetID;
+ n = low(n);
+ }
+ this.quantlast = level(n);
+ }
+ }
+
+ private void varset2vartable(final int r) {
+ if (r < 2)
+ throw new IllegalArgumentException("Illegal variable: " + r);
+ this.quantvarsetID++;
+ if (this.quantvarsetID == Integer.MAX_VALUE) {
+ this.quantvarset = new int[this.varnum];
+ this.quantvarsetID = 1;
+ }
+ for (int n = r; n > 1; n = high(n)) {
+ this.quantvarset[level(n)] = this.quantvarsetID;
+ this.quantlast = level(n);
+ }
+ }
+
+ private boolean insvarset(final int a) {
+ return Math.abs(this.quantvarset[a]) == this.quantvarsetID;
+ }
+
+ private boolean invarset(final int a) {
+ return this.quantvarset[a] == this.quantvarsetID;
+ }
+
+ /**
+ * Returns the statistics for this BDD Kernel.
+ * @return the statistics
+ */
+ public BDDStatistics statistics() {
+ final BDDStatistics statistics = new BDDStatistics();
+ statistics.produced = this.produced;
+ statistics.nodesize = this.nodesize;
+ statistics.freenum = this.freenum;
+ statistics.varnum = this.varnum;
+ statistics.cachesize = this.cachesize;
+ statistics.gbcollectnum = this.gbcollectnum;
+ return statistics;
+ }
+
+ /**
+ * A class for BDD statistics.
+ */
+ public static final class BDDStatistics {
+ private long produced;
+ private int nodesize;
+ private int freenum;
+ private int varnum;
+ private int cachesize;
+ private int gbcollectnum;
+
+ /**
+ * Returns the number of produced nodes.
+ * @return the number of produced nodes
+ */
+ public long produced() {
+ return this.produced;
+ }
+
+ /**
+ * Returns the number of allocated nodes.
+ * @return the number of allocated nodes
+ */
+ public int nodesize() {
+ return this.nodesize;
+ }
+
+ /**
+ * Returns the number of free nodes.
+ * @return the number of free nodes
+ */
+ public int freenum() {
+ return this.freenum;
+ }
+
+ /**
+ * Returns the number of variables.
+ * @return the number of variables
+ */
+ public int varnum() {
+ return this.varnum;
+ }
+
+ /**
+ * Returns the cache size.
+ * @return the cache size
+ */
+ public int cachesize() {
+ return this.cachesize;
+ }
+
+ /**
+ * Returns the number of garbage collections.
+ * @return the number of garbage collections
+ */
+ public int gbcollectnum() {
+ return this.gbcollectnum;
+ }
+
+ @Override
+ public String toString() {
+ return "BDDStatistics{" +
+ "produced nodes=" + this.produced +
+ ", allocated nodes=" + this.nodesize +
+ ", free nodes=" + this.freenum +
+ ", variables=" + this.varnum +
+ ", cache size=" + this.cachesize +
+ ", garbage collections=" + this.gbcollectnum +
+ '}';
+ }
+ }
+
+ private static final class BddNode {
+ int refcou = 10;
+ int level = 22;
+ int low;
+ int high;
+ int hash;
+ int next;
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/jbuddy/BDDPrime.java b/src/main/java/org/logicng/bdds/jbuddy/BDDPrime.java
new file mode 100644
index 00000000..e50dae5c
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/jbuddy/BDDPrime.java
@@ -0,0 +1,162 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2018 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+/*========================================================================
+ Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+ All rights reserved
+
+Permission is hereby granted, without written agreement and without
+license or royalty fees, to use, reproduce, prepare derivative
+works, distribute, and display this software and its documentation
+for any purpose, provided that (1) the above copyright notice and
+the following two paragraphs appear in all copies of the source code
+and (2) redistributions, including without limitation binaries,
+reproduce these notices in the supporting documentation. Substantial
+modifications to this software may be copyrighted by their authors
+and need not follow the licensing terms described here, provided
+that the new terms are clearly indicated in all files where they apply.
+
+IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+MODIFICATIONS.
+========================================================================*/
+
+package org.logicng.bdds.jbuddy;
+
+import java.util.Random;
+
+/**
+ * Prime number calculations
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+final class BDDPrime {
+
+ private static final int CHECKTIMES = 20;
+ private static final Random rng = new Random();
+
+ /**
+ * Returns the next prime greater than the given number.
+ * @param num the number
+ * @return the next prime greater than the given number
+ */
+ static int primeGTE(int num) {
+ if (isEven(num))
+ ++num;
+ while (!isPrime(num))
+ num += 2;
+ return num;
+ }
+
+ /**
+ * Returns the next prime less than the given number.
+ * @param num the number
+ * @return the next prime less than the given number
+ */
+ static int primeLTE(int num) {
+ if (isEven(num))
+ --num;
+ while (!isPrime(num))
+ num -= 2;
+ return num;
+ }
+
+ private static int numberOfBits(final int src) {
+ int b;
+ if (src == 0)
+ return 0;
+ for (b = 31; b > 0; --b)
+ if (bitIsSet(src, b))
+ return b + 1;
+ return 1;
+ }
+
+ private static boolean isWitness(final int witness, final int src) {
+ final int bitNum = numberOfBits(src - 1) - 1;
+ int d = 1;
+ for (int i = bitNum; i >= 0; --i) {
+ final int x = d;
+ d = mulmod(d, d, src);
+ if (d == 1 && x != 1 && x != src - 1)
+ return true;
+ if (bitIsSet(src - 1, i))
+ d = mulmod(d, witness, src);
+ }
+ return d != 1;
+ }
+
+ private static boolean isMillerRabinPrime(final int src) {
+ for (int n = 0; n < CHECKTIMES; ++n) {
+ final int witness = random(src - 1);
+ if (isWitness(witness, src))
+ return false;
+ }
+ return true;
+ }
+
+ private static boolean hasEasyFactors(final int src) {
+ return hasFactor(src, 3)
+ || hasFactor(src, 5)
+ || hasFactor(src, 7)
+ || hasFactor(src, 11)
+ || hasFactor(src, 13);
+ }
+
+ private static boolean isPrime(final int src) {
+ return !hasEasyFactors(src) && isMillerRabinPrime(src);
+ }
+
+ private static boolean bitIsSet(final int src, final int b) {
+ return (src & (1 << b)) != 0;
+ }
+
+ private static int mulmod(final int a, final int b, final int c) {
+ return (int) (((long) a * (long) b) % (long) c);
+ }
+
+ private static int random(final int i) {
+ return rng.nextInt(i) + 1;
+ }
+
+ private static boolean hasFactor(final int src, final int n) {
+ return (src != n) && (src % n == 0);
+ }
+
+ private static boolean isEven(final int src) {
+ return (src & 0x1) == 0;
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/orderings/BFSOrdering.java b/src/main/java/org/logicng/bdds/orderings/BFSOrdering.java
new file mode 100644
index 00000000..98559d22
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/orderings/BFSOrdering.java
@@ -0,0 +1,94 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.orderings;
+
+import org.logicng.formulas.BinaryOperator;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Literal;
+import org.logicng.formulas.Not;
+import org.logicng.formulas.PBConstraint;
+import org.logicng.formulas.Variable;
+
+import java.util.ArrayList;
+import java.util.LinkedHashSet;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Queue;
+
+/**
+ * A breadth-first-search BDD variable ordering. Traverses the formula in a BFS manner
+ * and gathers all variables in the occurrence.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class BFSOrdering implements VariableOrderingProvider {
+
+ @Override
+ public List getOrder(final Formula formula) {
+ return new ArrayList<>(bfs(formula));
+ }
+
+ private LinkedHashSet bfs(final Formula formula) {
+ final LinkedHashSet variables = new LinkedHashSet<>();
+ final Queue queue = new LinkedList<>();
+ queue.add(formula);
+ while (!queue.isEmpty()) {
+ final Formula current = queue.remove();
+ switch (current.type()) {
+ case LITERAL:
+ final Literal lit = (Literal) current;
+ if (lit.phase())
+ variables.add(lit.variable());
+ else
+ queue.add(lit.variable());
+ break;
+ case NOT:
+ queue.add(((Not) current).operand());
+ break;
+ case IMPL:
+ case EQUIV:
+ final BinaryOperator op = (BinaryOperator) current;
+ queue.add(op.left());
+ queue.add(op.right());
+ break;
+ case AND:
+ case OR:
+ for (final Formula operand : current)
+ queue.add(operand);
+ break;
+ case PBC:
+ final PBConstraint pbc = (PBConstraint) current;
+ for (final Literal literal : pbc.operands())
+ variables.add(literal.variable());
+ break;
+ }
+ }
+ return variables;
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/orderings/DFSOrdering.java b/src/main/java/org/logicng/bdds/orderings/DFSOrdering.java
new file mode 100644
index 00000000..36fe9562
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/orderings/DFSOrdering.java
@@ -0,0 +1,83 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.orderings;
+
+import org.logicng.formulas.BinaryOperator;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Literal;
+import org.logicng.formulas.Not;
+import org.logicng.formulas.PBConstraint;
+import org.logicng.formulas.Variable;
+
+import java.util.ArrayList;
+import java.util.LinkedHashSet;
+import java.util.List;
+
+/**
+ * A depth-first-search BDD variable ordering. Traverses the formula in a DFS manner
+ * and gathers all variables in the occurrence.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class DFSOrdering implements VariableOrderingProvider {
+
+ @Override
+ public List getOrder(final Formula formula) {
+ final LinkedHashSet order = new LinkedHashSet<>(formula.variables().size());
+ dfs(formula, order);
+ return new ArrayList<>(order);
+ }
+
+ private void dfs(final Formula formula, final LinkedHashSet variables) {
+ switch (formula.type()) {
+ case LITERAL:
+ variables.add(((Literal) formula).variable());
+ break;
+ case NOT:
+ dfs(((Not) formula).operand(), variables);
+ break;
+ case IMPL:
+ case EQUIV:
+ final BinaryOperator op = (BinaryOperator) formula;
+ dfs(op.left(), variables);
+ dfs(op.right(), variables);
+ break;
+ case AND:
+ case OR:
+ for (final Formula operand : formula)
+ dfs(operand, variables);
+ break;
+ case PBC:
+ final PBConstraint pbc = (PBConstraint) formula;
+ for (final Literal lit : pbc.operands())
+ variables.add(lit.variable());
+ break;
+ }
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/orderings/ForceOrdering.java b/src/main/java/org/logicng/bdds/orderings/ForceOrdering.java
new file mode 100644
index 00000000..eb40b68c
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/orderings/ForceOrdering.java
@@ -0,0 +1,140 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.orderings;
+
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Variable;
+import org.logicng.graphs.datastructures.Hypergraph;
+import org.logicng.graphs.datastructures.HypergraphNode;
+import org.logicng.graphs.generators.HypergraphGenerator;
+import org.logicng.predicates.CNFPredicate;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+/**
+ * Simple implementation of the FORCE BDD variable ordering due to Aloul, Markov, and Sakallah. This ordering only
+ * works for CNF formulas. A formula has to be converted to CNF before this ordering is called.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class ForceOrdering implements VariableOrderingProvider {
+
+ private static final Comparator, Double>> COMPARATOR =
+ new Comparator, Double>>() {
+ @Override
+ public int compare(final Map.Entry, Double> o1, final Map.Entry, Double> o2) {
+ return o1.getValue().compareTo(o2.getValue());
+ }
+ };
+
+ private final DFSOrdering dfsOrdering = new DFSOrdering();
+
+ @Override
+ public List getOrder(final Formula formula) {
+ if (!formula.holds(new CNFPredicate()))
+ throw new IllegalArgumentException("FORCE variable ordering can only be applied to CNF formulas.");
+ final Hypergraph hypergraph = HypergraphGenerator.fromCNF(formula);
+ final Map> nodes = new HashMap<>();
+ for (final HypergraphNode node : hypergraph.nodes())
+ nodes.put(node.content(), node);
+ return force(formula, hypergraph, nodes);
+ }
+
+ /**
+ * Executes the main FORCE algorithm.
+ * @param formula the CNF formula for the ordering
+ * @param hypergraph the hypergraph for this formula
+ * @param nodes the variable to hypergraph node mapping
+ * @return the variable ordering according to the FORCE algorithm
+ */
+ private List force(final Formula formula, final Hypergraph hypergraph,
+ final Map> nodes) {
+ final LinkedHashMap, Integer> initialOrdering = createInitialOrdering(formula, nodes);
+ LinkedHashMap, Integer> lastOrdering;
+ LinkedHashMap, Integer> currentOrdering = initialOrdering;
+ do {
+ lastOrdering = currentOrdering;
+ final LinkedHashMap, Double> newLocations = new LinkedHashMap<>();
+ for (final HypergraphNode node : hypergraph.nodes())
+ newLocations.put(node, node.computeTentativeNewLocation(lastOrdering));
+ currentOrdering = orderingFromTentativeNewLocations(newLocations);
+ } while (shouldProceed(lastOrdering, currentOrdering));
+ final Variable[] ordering = new Variable[currentOrdering.size()];
+ for (final Map.Entry, Integer> entry : currentOrdering.entrySet())
+ ordering[entry.getValue()] = entry.getKey().content();
+ return Arrays.asList(ordering);
+ }
+
+ /**
+ * Creates an initial ordering for the variables based on a DFS.
+ * @param formula the CNF formula
+ * @param nodes the variable to hypergraph node mapping
+ * @return the initial variable ordering
+ */
+ private LinkedHashMap, Integer> createInitialOrdering(final Formula formula, final Map> nodes) {
+ final LinkedHashMap, Integer> initialOrdering = new LinkedHashMap<>();
+ final List dfsOrder = this.dfsOrdering.getOrder(formula);
+ for (int i = 0; i < dfsOrder.size(); i++)
+ initialOrdering.put(nodes.get(dfsOrder.get(i)), i);
+ return initialOrdering;
+ }
+
+ /**
+ * Generates a new integer ordering from tentative new locations of nodes with the double weighting.
+ * @param newLocations the tentative new locations
+ * @return the new integer ordering
+ */
+ private LinkedHashMap, Integer> orderingFromTentativeNewLocations(final LinkedHashMap, Double> newLocations) {
+ final LinkedHashMap, Integer> ordering = new LinkedHashMap<>();
+ final List, Double>> list = new ArrayList<>(newLocations.entrySet());
+ Collections.sort(list, COMPARATOR);
+ int count = 0;
+ for (final Map.Entry, Double> entry : list)
+ ordering.put(entry.getKey(), count++);
+ return ordering;
+ }
+
+ /**
+ * The abortion criteria for the FORCE algorithm.
+ * @param lastOrdering the ordering of the last step
+ * @param currentOrdering the ordering of the current step
+ * @return {@code true} if the algorithm should proceed, {@code false} if it should stop
+ */
+ private boolean shouldProceed(final Map, Integer> lastOrdering, final Map, Integer> currentOrdering) {
+ return !lastOrdering.equals(currentOrdering);
+ }
+
+}
diff --git a/src/main/java/org/logicng/bdds/orderings/MaxToMinOrdering.java b/src/main/java/org/logicng/bdds/orderings/MaxToMinOrdering.java
new file mode 100644
index 00000000..5f6f310f
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/orderings/MaxToMinOrdering.java
@@ -0,0 +1,76 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.orderings;
+
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Variable;
+import org.logicng.functions.VariableProfileFunction;
+
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.List;
+import java.util.Map;
+
+import static org.logicng.bdds.orderings.MinToMaxOrdering.sortProfileByOccurrence;
+
+/**
+ * A BDD variable ordering sorting the variables from maximal to minimal occurrence
+ * in the input formula. If two variables have the same number of occurrences, their
+ * ordering according to their DFS ordering will be considered.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class MaxToMinOrdering implements VariableOrderingProvider {
+
+ private final VariableProfileFunction profileFunction = new VariableProfileFunction();
+ private final DFSOrdering dfsOrdering = new DFSOrdering();
+
+ @Override
+ public List getOrder(final Formula formula) {
+ final Map profile = formula.apply(this.profileFunction);
+ final List dfs = this.dfsOrdering.getOrder(formula);
+
+ final Comparator> comparator = new Comparator>() {
+ @Override
+ public int compare(final Map.Entry o1, final Map.Entry o2) {
+ final int occComp = o1.getValue().compareTo(o2.getValue());
+ if (occComp != 0)
+ return occComp;
+ final int index1 = dfs.indexOf(o1.getKey());
+ final int index2 = dfs.indexOf(o2.getKey());
+ return index1 - index2;
+ }
+ };
+ final Map sortedProfile = sortProfileByOccurrence(profile, comparator);
+ final List order = new ArrayList<>(sortedProfile.size());
+ for (final Map.Entry entry : sortedProfile.entrySet())
+ order.add(entry.getKey());
+ return order;
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/orderings/MinToMaxOrdering.java b/src/main/java/org/logicng/bdds/orderings/MinToMaxOrdering.java
new file mode 100644
index 00000000..408723b1
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/orderings/MinToMaxOrdering.java
@@ -0,0 +1,85 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.orderings;
+
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Variable;
+import org.logicng.functions.VariableProfileFunction;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+/**
+ * A BDD variable ordering sorting the variables from minimal to maximal occurrence
+ * in the input formula. If two variables have the same number of occurrences, their
+ * ordering according to their DFS ordering will be considered.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class MinToMaxOrdering implements VariableOrderingProvider {
+
+ private final VariableProfileFunction profileFunction = new VariableProfileFunction();
+ private final DFSOrdering dfsOrdering = new DFSOrdering();
+
+ @Override
+ public List getOrder(final Formula formula) {
+ final Map profile = formula.apply(this.profileFunction);
+ final List dfs = this.dfsOrdering.getOrder(formula);
+
+ final Comparator> comparator = new Comparator>() {
+ @Override
+ public int compare(final Map.Entry o1, final Map.Entry o2) {
+ final int occComp = o1.getValue().compareTo(o2.getValue());
+ if (occComp != 0)
+ return -occComp;
+ final int index1 = dfs.indexOf(o1.getKey());
+ final int index2 = dfs.indexOf(o2.getKey());
+ return index1 - index2;
+ }
+ };
+ final Map sortedProfile = sortProfileByOccurrence(profile, comparator);
+ final List order = new ArrayList<>(sortedProfile.size());
+ for (final Map.Entry entry : sortedProfile.entrySet())
+ order.add(entry.getKey());
+ return order;
+ }
+
+ static Map sortProfileByOccurrence(final Map map, final Comparator> comparator) {
+ final List> list = new ArrayList<>(map.entrySet());
+ Collections.sort(list, comparator);
+ final Map result = new LinkedHashMap<>();
+ for (final Map.Entry entry : list)
+ result.put(entry.getKey(), entry.getValue());
+ return result;
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/orderings/VariableOrdering.java b/src/main/java/org/logicng/bdds/orderings/VariableOrdering.java
new file mode 100644
index 00000000..1e191474
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/orderings/VariableOrdering.java
@@ -0,0 +1,62 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.orderings;
+
+/**
+ * An enumeration for the different BDD variable orderings. A variable ordering is associated
+ * with its own provider which can generate orderings for this ordering.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public enum VariableOrdering {
+
+ DFS(DFSOrdering.class),
+ BFS(BFSOrdering.class),
+ MIN2MAX(MinToMaxOrdering.class),
+ MAX2MIN(MaxToMinOrdering.class),
+ FORCE(ForceOrdering.class);
+
+ private final Class provider;
+
+ /**
+ * Constructs a new variable ordering with a given provider.
+ * @param provider the provider
+ */
+ VariableOrdering(final Class provider) {
+ this.provider = provider;
+ }
+
+ /**
+ * Returns the provider for this variable ordering.
+ * @return the provider for this variable ordering
+ */
+ public Class provider() {
+ return this.provider;
+ }
+}
diff --git a/src/main/java/org/logicng/bdds/orderings/VariableOrderingProvider.java b/src/main/java/org/logicng/bdds/orderings/VariableOrderingProvider.java
new file mode 100644
index 00000000..8ffb983f
--- /dev/null
+++ b/src/main/java/org/logicng/bdds/orderings/VariableOrderingProvider.java
@@ -0,0 +1,50 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.bdds.orderings;
+
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Variable;
+
+import java.util.List;
+
+/**
+ * An interface for variable ordering providers for BDDs.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public interface VariableOrderingProvider {
+
+ /**
+ * Generates a variable ordering for a given formula. Such a variable ordering can then be
+ * used in the {@link org.logicng.bdds.BDDFactory#setVariableOrder(List)} method.
+ * @param formula the formula
+ * @return the variable ordering
+ */
+ List getOrder(final Formula formula);
+}
diff --git a/src/main/java/org/logicng/collections/ImmutableFormulaList.java b/src/main/java/org/logicng/collections/ImmutableFormulaList.java
index 74d35dee..955a2a2d 100644
--- a/src/main/java/org/logicng/collections/ImmutableFormulaList.java
+++ b/src/main/java/org/logicng/collections/ImmutableFormulaList.java
@@ -86,7 +86,7 @@ public ImmutableFormulaList(final FType operator, final Formula... formulas) {
*/
public ImmutableFormulaList(final Collection formulas) {
this.operator = FType.NONE;
- this.formulas = formulas.toArray(new Formula[formulas.size()]);
+ this.formulas = formulas.toArray(new Formula[0]);
}
/**
@@ -96,7 +96,7 @@ public ImmutableFormulaList(final Collection formulas) {
*/
public ImmutableFormulaList(final FType operator, final Collection formulas) {
this.operator = operator;
- this.formulas = formulas.toArray(new Formula[formulas.size()]);
+ this.formulas = formulas.toArray(new Formula[0]);
}
/**
@@ -134,7 +134,7 @@ public ImmutableFormulaList(final FType operator, final ImmutableFormulaList for
* @param copy {@code true} if the input array should be copied, {@code false} otherwise
* @param formulas the formulas
*/
- private ImmutableFormulaList(final FType operator, boolean copy, final Formula... formulas) {
+ private ImmutableFormulaList(final FType operator, final boolean copy, final Formula... formulas) {
this.operator = operator;
this.formulas = copy ? Arrays.copyOf(formulas, formulas.length) : formulas;
}
@@ -155,9 +155,9 @@ public FType operator() {
*/
public Formula formula(final FormulaFactory f) {
if (this.operator != FType.AND && this.operator != FType.OR)
- throw new IllegalStateException("Illegal operator for formula list formula construction: " + operator);
+ throw new IllegalStateException("Illegal operator for formula list formula construction: " + this.operator);
if (this.formula == null) {
- if (operator == FType.AND)
+ if (this.operator == FType.AND)
this.formula = f.and(this.formulas);
else
this.formula = f.or(this.formulas);
@@ -186,7 +186,7 @@ public boolean empty() {
* @param i the index
* @return the i-th formula of this formula list
*/
- public Formula get(int i) {
+ public Formula get(final int i) {
if (i < 0 || i >= this.formulas.length)
throw new IllegalArgumentException("Illegal formula index: " + i);
return this.formulas[i];
@@ -215,7 +215,7 @@ public SortedSet variables() {
for (final Formula f : this.formulas)
this.variables.addAll(f.variables());
}
- return variables;
+ return this.variables;
}
/**
@@ -324,14 +324,14 @@ public Iterator iterator() {
@Override
public boolean hasNext() {
- return i < formulas.length;
+ return this.i < ImmutableFormulaList.this.formulas.length;
}
@Override
public Formula next() {
- if (i == formulas.length)
+ if (this.i == ImmutableFormulaList.this.formulas.length)
throw new NoSuchElementException();
- return formulas[i++];
+ return ImmutableFormulaList.this.formulas[this.i++];
}
@Override
diff --git a/src/main/java/org/logicng/datastructures/Assignment.java b/src/main/java/org/logicng/datastructures/Assignment.java
index bcb30de1..80b2f336 100644
--- a/src/main/java/org/logicng/datastructures/Assignment.java
+++ b/src/main/java/org/logicng/datastructures/Assignment.java
@@ -92,6 +92,21 @@ public Assignment(final Collection lits) {
this(lits, false);
}
+ /**
+ * Constructs a new assignment for a given array of literals (without fast evaluation).
+ * @param lits a new assignment for a given array of literals
+ */
+ public Assignment(final Literal... lits) {
+ this(false);
+ for (Literal lit : lits)
+ if (lit.phase())
+ this.pos.add((Variable) lit);
+ else {
+ this.neg.add(lit);
+ this.negVars.add((Variable) lit.negate());
+ }
+ }
+
/**
* Constructs a new assignment for a given collection of literals.
* @param lits a new assignment for a given collection of literals
diff --git a/src/main/java/org/logicng/datastructures/Substitution.java b/src/main/java/org/logicng/datastructures/Substitution.java
index 2b80d191..d5e71046 100644
--- a/src/main/java/org/logicng/datastructures/Substitution.java
+++ b/src/main/java/org/logicng/datastructures/Substitution.java
@@ -55,7 +55,7 @@ public Substitution() {
* @return the number of mappings in this substitution
*/
public int size() {
- return subst.size();
+ return this.subst.size();
}
/**
@@ -66,7 +66,7 @@ public int size() {
* @param formula the formula
*/
public void addMapping(final Variable variable, final Formula formula) {
- subst.put(variable, formula);
+ this.subst.put(variable, formula);
}
/**
@@ -75,15 +75,12 @@ public void addMapping(final Variable variable, final Formula formula) {
* @return an formula of {@code null}
*/
public Formula getSubstitution(final Variable variable) {
- Formula res = subst.get(variable);
- if (res == null)
- return null;
- return res;
+ return this.subst.get(variable);
}
@Override
public int hashCode() {
- return subst.hashCode();
+ return this.subst.hashCode();
}
@Override
@@ -93,6 +90,6 @@ public boolean equals(final Object other) {
@Override
public String toString() {
- return "Substitution" + subst;
+ return "Substitution" + this.subst;
}
}
diff --git a/src/main/java/org/logicng/formulas/Formula.java b/src/main/java/org/logicng/formulas/Formula.java
index 9884777c..936eb769 100644
--- a/src/main/java/org/logicng/formulas/Formula.java
+++ b/src/main/java/org/logicng/formulas/Formula.java
@@ -28,6 +28,10 @@
package org.logicng.formulas;
+import org.logicng.bdds.BDDFactory;
+import org.logicng.bdds.datastructures.BDD;
+import org.logicng.bdds.orderings.VariableOrdering;
+import org.logicng.bdds.orderings.VariableOrderingProvider;
import org.logicng.datastructures.Assignment;
import org.logicng.datastructures.Substitution;
import org.logicng.datastructures.Tristate;
@@ -109,7 +113,7 @@ public FormulaFactory factory() {
* @return the number of internal nodes of this formula.
*/
public long numberOfInternalNodes() {
- return f.numberOfNodes(this);
+ return this.f.numberOfNodes(this);
}
/**
@@ -179,7 +183,7 @@ public boolean containsVariable(final String variable) {
* @return a new substituted formula
*/
public Formula substitute(final Variable variable, final Formula formula) {
- Substitution subst = new Substitution();
+ final Substitution subst = new Substitution();
subst.addMapping(variable, formula);
return this.substitute(subst);
}
@@ -215,6 +219,40 @@ public Formula cnf() {
return this.f.cnfEncoder().encode(this);
}
+ /**
+ * Generates a BDD from this formula with a given variable ordering. This is done by generating a new BDD factory,
+ * generating the variable order for this formula, and building a new BDD. If more sophisticated operations should
+ * be performed on the BDD or more than one formula should be constructed on the BDD, an own instance of
+ * {@link BDDFactory} should be created and used.
+ * @param variableOrdering the variable ordering
+ * @return the BDD for this formula with the given ordering
+ */
+ public BDD bdd(final VariableOrdering variableOrdering) {
+ final int varNum = this.variables().size();
+ final BDDFactory factory = new BDDFactory(varNum * 30, varNum * 20, this.factory());
+ if (variableOrdering == null)
+ factory.setNumberOfVars(varNum);
+ else {
+ try {
+ final VariableOrderingProvider provider = variableOrdering.provider().newInstance();
+ factory.setVariableOrder(provider.getOrder(this));
+ } catch (final InstantiationException | IllegalAccessException e) {
+ throw new IllegalStateException("Could not generate the BDD variable ordering provider", e);
+ }
+ }
+ return factory.build(this);
+ }
+
+ /**
+ * Generates a BDD from this formula with no given variable ordering. This is done by generating a new BDD factory
+ * and building a new BDD. If more sophisticated operations should be performed on the BDD or more than one
+ * formula should be constructed on the BDD, an own instance of * {@link BDDFactory} should be created and used.
+ * @return the BDD for this formula
+ */
+ public BDD bdd() {
+ return bdd(null);
+ }
+
/**
* Transforms this formula with a given formula transformator and caches the result.
* @param transformation the formula transformator
@@ -230,7 +268,7 @@ public Formula transform(final FormulaTransformation transformation) {
* @param cache indicates whether the result (and associated predicates) should be cached in this formula's cache.
* @return the transformed formula
*/
- public Formula transform(final FormulaTransformation transformation, boolean cache) {
+ public Formula transform(final FormulaTransformation transformation, final boolean cache) {
return transformation.apply(this, cache);
}
@@ -250,7 +288,7 @@ public boolean holds(final FormulaPredicate predicate) {
* @param cache indicates whether the result should be cached in this formula's cache
* @return {@code true} if the predicate holds, {@code false} otherwise
*/
- public boolean holds(final FormulaPredicate predicate, boolean cache) {
+ public boolean holds(final FormulaPredicate predicate, final boolean cache) {
return predicate.test(this, cache);
}
@@ -261,7 +299,7 @@ public boolean holds(final FormulaPredicate predicate, boolean cache) {
* @param the result type of the function
* @return the result of the function application
*/
- public T apply(final FormulaFunction function, boolean cache) {
+ public T apply(final FormulaFunction function, final boolean cache) {
return function.apply(this, cache);
}
@@ -310,7 +348,7 @@ public Tristate predicateCacheEntry(final CacheEntry key) {
* @param key the cache key
* @param value the cache value
*/
- public void setPredicateCacheEntry(final CacheEntry key, boolean value) {
+ public void setPredicateCacheEntry(final CacheEntry key, final boolean value) {
this.predicateCache.put(key, Tristate.fromBool(value));
}
@@ -345,12 +383,12 @@ public void setFunctionCacheEntry(final CacheEntry key, final Object value) {
* Clears the transformation and function cache of the formula.
*/
public void clearCaches() {
- transformationCache.clear();
- functionCache.clear();
+ this.transformationCache.clear();
+ this.functionCache.clear();
}
@Override
public String toString() {
- return f.string(this);
+ return this.f.string(this);
}
}
diff --git a/src/main/java/org/logicng/formulas/FormulaFactory.java b/src/main/java/org/logicng/formulas/FormulaFactory.java
index 97a16004..d2dd7a18 100644
--- a/src/main/java/org/logicng/formulas/FormulaFactory.java
+++ b/src/main/java/org/logicng/formulas/FormulaFactory.java
@@ -164,7 +164,7 @@ public FormulaFactory() {
* @param f the formula
* @return {@code true} if a given list of formulas contains a given formula, {@code false} otherwise
*/
- private static boolean containsComplement(final LinkedHashSet formulas, Formula f) {
+ private static boolean containsComplement(final LinkedHashSet formulas, final Formula f) {
return formulas.contains(f.negate());
}
@@ -356,7 +356,7 @@ public CFalse falsum() {
* @throws IllegalArgumentException if a wrong formula type is passed
*/
public Formula naryOperator(final FType type, final Collection operands) {
- return this.naryOperator(type, operands.toArray(new Formula[operands.size()]));
+ return this.naryOperator(type, operands.toArray(new Formula[0]));
}
/**
@@ -426,7 +426,7 @@ private Formula constructAnd(final LinkedHashSet operands) {
}
if (tempAnd != null)
return tempAnd;
- LinkedHashSet condensedOperands = operands.size() < 2
+ final LinkedHashSet condensedOperands = operands.size() < 2
? operands
: this.condenseOperandsAnd(operands);
if (condensedOperands == null)
@@ -435,7 +435,7 @@ private Formula constructAnd(final LinkedHashSet operands) {
return this.verum();
if (condensedOperands.size() == 1)
return condensedOperands.iterator().next();
- And and;
+ final And and;
Map, And> condAndMap = this.andsN;
switch (condensedOperands.size()) {
case 2:
@@ -571,7 +571,7 @@ private Formula constructOr(final LinkedHashSet operands) {
}
if (tempOr != null)
return tempOr;
- LinkedHashSet condensedOperands = operands.size() < 2
+ final LinkedHashSet condensedOperands = operands.size() < 2
? operands
: this.condenseOperandsOr(operands);
if (condensedOperands == null)
@@ -580,7 +580,7 @@ private Formula constructOr(final LinkedHashSet operands) {
return this.falsum();
if (condensedOperands.size() == 1)
return condensedOperands.iterator().next();
- Or or;
+ final Or or;
Map, Or> condOrMap = this.orsN;
switch (condensedOperands.size()) {
case 2:
@@ -673,7 +673,7 @@ private Formula constructClause(final LinkedHashSet literals) {
* @param phase the literal phase
* @return a new literal with the given name and phase
*/
- public Literal literal(final String name, boolean phase) {
+ public Literal literal(final String name, final boolean phase) {
if (phase)
return this.variable(name);
else {
@@ -709,11 +709,11 @@ public Variable variable(final String name) {
* @return the pseudo-Boolean constraint
* @throws IllegalArgumentException if the number of literals and coefficients do not correspond
*/
- public PBConstraint pbc(final CType comparator, int rhs, final List literals, final List coefficients) {
- int[] cfs = new int[coefficients.size()];
+ public PBConstraint pbc(final CType comparator, final int rhs, final List literals, final List coefficients) {
+ final int[] cfs = new int[coefficients.size()];
for (int i = 0; i < coefficients.size(); i++)
cfs[i] = coefficients.get(i);
- return this.constructPBC(comparator, rhs, literals.toArray(new Literal[literals.size()]), cfs);
+ return this.constructPBC(comparator, rhs, literals.toArray(new Literal[0]), cfs);
}
/**
@@ -725,11 +725,11 @@ public PBConstraint pbc(final CType comparator, int rhs, final List variables) {
+ public PBConstraint cc(final CType comparator, final int rhs, final Collection variables) {
final int[] coefficients = new int[variables.size()];
Arrays.fill(coefficients, 1);
final Variable[] vars = new Variable[variables.size()];
@@ -765,7 +765,7 @@ public PBConstraint cc(final CType comparator, int rhs, final Collection condenseOperandsOr(Collection operands) {
+ private LinkedHashSet condenseOperandsOr(final Collection operands) {
final LinkedHashSet ops = new LinkedHashSet<>();
this.cnfCheck = true;
- for (Formula form : operands)
+ for (final Formula form : operands)
if (form.type() == OR) {
- for (Formula f : ((NAryOperator) form).operands) {
+ for (final Formula f : ((NAryOperator) form).operands) {
this.addFormulaOr(ops, f);
- if (!formulaAdditionResult[0])
+ if (!this.formulaAdditionResult[0])
return null;
- if (!formulaAdditionResult[1])
+ if (!this.formulaAdditionResult[1])
this.cnfCheck = false;
}
} else {
this.addFormulaOr(ops, form);
- if (!formulaAdditionResult[0])
+ if (!this.formulaAdditionResult[0])
return null;
- if (!formulaAdditionResult[1])
+ if (!this.formulaAdditionResult[1])
this.cnfCheck = false;
}
return ops;
@@ -883,23 +883,23 @@ private LinkedHashSet condenseOperandsOr(Collection
* @param operands the formulas
* @return a condensed array of operands
*/
- private LinkedHashSet condenseOperandsAnd(Collection operands) {
+ private LinkedHashSet condenseOperandsAnd(final Collection operands) {
final LinkedHashSet ops = new LinkedHashSet<>();
this.cnfCheck = true;
- for (Formula form : operands)
+ for (final Formula form : operands)
if (form.type() == AND) {
- for (Formula f : ((NAryOperator) form).operands) {
+ for (final Formula f : ((NAryOperator) form).operands) {
this.addFormulaAnd(ops, f);
- if (!formulaAdditionResult[0])
+ if (!this.formulaAdditionResult[0])
return null;
- if (!formulaAdditionResult[1])
+ if (!this.formulaAdditionResult[1])
this.cnfCheck = false;
}
} else {
this.addFormulaAnd(ops, form);
- if (!formulaAdditionResult[0])
+ if (!this.formulaAdditionResult[0])
return null;
- if (!formulaAdditionResult[1])
+ if (!this.formulaAdditionResult[1])
this.cnfCheck = false;
}
return ops;
@@ -930,7 +930,7 @@ public long numberOfNodes(final Formula formula) {
* @throws ParserException if the parser throws an exception
*/
public Formula parse(final String string) throws ParserException {
- return parser.parse(string);
+ return this.parser.parse(string);
}
/**
@@ -944,15 +944,15 @@ public Formula parse(final String string) throws ParserException {
*/
private void addFormulaOr(final LinkedHashSet ops, final Formula f) {
if (f.type == FALSE) {
- formulaAdditionResult[0] = true;
- formulaAdditionResult[1] = true;
+ this.formulaAdditionResult[0] = true;
+ this.formulaAdditionResult[1] = true;
} else if (f.type == TRUE || containsComplement(ops, f)) {
- formulaAdditionResult[0] = false;
- formulaAdditionResult[1] = false;
+ this.formulaAdditionResult[0] = false;
+ this.formulaAdditionResult[1] = false;
} else {
ops.add(f);
- formulaAdditionResult[0] = true;
- formulaAdditionResult[1] = f.type == LITERAL;
+ this.formulaAdditionResult[0] = true;
+ this.formulaAdditionResult[1] = f.type == LITERAL;
}
}
@@ -967,15 +967,15 @@ private void addFormulaOr(final LinkedHashSet ops, final Formula f) {
*/
private void addFormulaAnd(final LinkedHashSet ops, final Formula f) {
if (f.type() == TRUE) {
- formulaAdditionResult[0] = true;
- formulaAdditionResult[1] = true;
+ this.formulaAdditionResult[0] = true;
+ this.formulaAdditionResult[1] = true;
} else if (f.type == FALSE || containsComplement(ops, f)) {
- formulaAdditionResult[0] = false;
- formulaAdditionResult[1] = false;
+ this.formulaAdditionResult[0] = false;
+ this.formulaAdditionResult[1] = false;
} else {
ops.add(f);
- formulaAdditionResult[0] = true;
- formulaAdditionResult[1] = f.type == LITERAL || f.type == OR && ((Or) f).isCNFClause();
+ this.formulaAdditionResult[0] = true;
+ this.formulaAdditionResult[1] = f.type == LITERAL || f.type == OR && ((Or) f).isCNFClause();
}
}
@@ -989,7 +989,7 @@ public Formula importFormula(final Formula formula) {
if (this.importer == null) {
this.importer = new FormulaFactoryImporter(this);
}
- return formula.transform(importer);
+ return formula.transform(this.importer);
}
/**
@@ -1024,7 +1024,7 @@ public FormulaStringRepresentation stringRepresentation() {
* @return the statistics for this formula factory
*/
public FormulaFactoryStatistics statistics() {
- FormulaFactoryStatistics statistics = new FormulaFactoryStatistics();
+ final FormulaFactoryStatistics statistics = new FormulaFactoryStatistics();
statistics.name = this.name;
statistics.positiveLiterals = this.posLiterals.size();
statistics.negativeLiterals = this.negLiterals.size();
@@ -1061,7 +1061,7 @@ private static final class PBOperands {
* @param comparator the comparator of the constraint
* @param rhs the right-hand side of the constraint
*/
- public PBOperands(final Literal[] literals, final int[] coefficients, final CType comparator, int rhs) {
+ public PBOperands(final Literal[] literals, final int[] coefficients, final CType comparator, final int rhs) {
this.literals = literals;
this.coefficients = coefficients;
this.comparator = comparator;
@@ -1070,7 +1070,7 @@ public PBOperands(final Literal[] literals, final int[] coefficients, final CTyp
@Override
public int hashCode() {
- return Objects.hash(this.rhs, this.comparator, Arrays.hashCode(coefficients), Arrays.hashCode(literals));
+ return Objects.hash(this.rhs, this.comparator, Arrays.hashCode(this.coefficients), Arrays.hashCode(this.literals));
}
@Override
@@ -1134,7 +1134,7 @@ public static final class FormulaFactoryStatistics {
* @return the name of the formula factory
*/
public String name() {
- return name;
+ return this.name;
}
/**
@@ -1142,7 +1142,7 @@ public String name() {
* @return the number of positive literals in the factory
*/
public int positiveLiterals() {
- return positiveLiterals;
+ return this.positiveLiterals;
}
/**
@@ -1150,7 +1150,7 @@ public int positiveLiterals() {
* @return the number of negative literals in the factory
*/
public int negativeLiterals() {
- return negativeLiterals;
+ return this.negativeLiterals;
}
/**
@@ -1158,7 +1158,7 @@ public int negativeLiterals() {
* @return the number of negations in the factory
*/
public int negations() {
- return negations;
+ return this.negations;
}
/**
@@ -1166,7 +1166,7 @@ public int negations() {
* @return the number of implications in the factory
*/
public int implications() {
- return implications;
+ return this.implications;
}
/**
@@ -1174,7 +1174,7 @@ public int implications() {
* @return the number of equivalences in the factory
*/
public int equivalences() {
- return equivalences;
+ return this.equivalences;
}
/**
@@ -1182,7 +1182,7 @@ public int equivalences() {
* @return the number of conjunctions of size 2 in the factory
*/
public int conjunctions2() {
- return conjunctions2;
+ return this.conjunctions2;
}
/**
@@ -1190,7 +1190,7 @@ public int conjunctions2() {
* @return the number of conjunctions of size 3 in the factory
*/
public int conjunctions3() {
- return conjunctions3;
+ return this.conjunctions3;
}
/**
@@ -1198,7 +1198,7 @@ public int conjunctions3() {
* @return the number of conjunctions of size 4 in the factory
*/
public int conjunctions4() {
- return conjunctions4;
+ return this.conjunctions4;
}
/**
@@ -1206,7 +1206,7 @@ public int conjunctions4() {
* @return the number of conjunctions of a size >4 in the factory
*/
public int conjunctionsN() {
- return conjunctionsN;
+ return this.conjunctionsN;
}
/**
@@ -1214,7 +1214,7 @@ public int conjunctionsN() {
* @return the number of disjunctions of size 2 in the factory
*/
public int disjunctions2() {
- return disjunctions2;
+ return this.disjunctions2;
}
/**
@@ -1222,7 +1222,7 @@ public int disjunctions2() {
* @return the number of disjunctions of size 3 in the factory
*/
public int disjunctions3() {
- return disjunctions3;
+ return this.disjunctions3;
}
/**
@@ -1230,7 +1230,7 @@ public int disjunctions3() {
* @return the number of disjunctions of size 4 in the factory
*/
public int disjunctions4() {
- return disjunctions4;
+ return this.disjunctions4;
}
/**
@@ -1238,7 +1238,7 @@ public int disjunctions4() {
* @return the number of disjunctions of a size >4 in the factory
*/
public int disjunctionsN() {
- return disjunctionsN;
+ return this.disjunctionsN;
}
/**
@@ -1246,7 +1246,7 @@ public int disjunctionsN() {
* @return the number of generated cardinality constraint auxiliary variables
*/
public int ccCounter() {
- return ccCounter;
+ return this.ccCounter;
}
/**
@@ -1254,7 +1254,7 @@ public int ccCounter() {
* @return the number of generated pseudo-Boolean auxiliary variables
*/
public int pbCounter() {
- return pbCounter;
+ return this.pbCounter;
}
/**
@@ -1262,7 +1262,7 @@ public int pbCounter() {
* @return the number of generated CNF auxiliary variables
*/
public int cnfCounter() {
- return cnfCounter;
+ return this.cnfCounter;
}
/**
@@ -1276,56 +1276,56 @@ public int formulas() {
}
@Override
- public boolean equals(Object o) {
+ public boolean equals(final Object o) {
if (this == o) return true;
if (!(o instanceof FormulaFactoryStatistics)) return false;
- FormulaFactoryStatistics that = (FormulaFactoryStatistics) o;
- return positiveLiterals == that.positiveLiterals &&
- negativeLiterals == that.negativeLiterals &&
- negations == that.negations &&
- implications == that.implications &&
- equivalences == that.equivalences &&
- conjunctions2 == that.conjunctions2 &&
- conjunctions3 == that.conjunctions3 &&
- conjunctions4 == that.conjunctions4 &&
- conjunctionsN == that.conjunctionsN &&
- disjunctions2 == that.disjunctions2 &&
- disjunctions3 == that.disjunctions3 &&
- disjunctions4 == that.disjunctions4 &&
- disjunctionsN == that.disjunctionsN &&
- ccCounter == that.ccCounter &&
- pbCounter == that.pbCounter &&
- cnfCounter == that.cnfCounter &&
- Objects.equals(name, that.name);
+ final FormulaFactoryStatistics that = (FormulaFactoryStatistics) o;
+ return this.positiveLiterals == that.positiveLiterals &&
+ this.negativeLiterals == that.negativeLiterals &&
+ this.negations == that.negations &&
+ this.implications == that.implications &&
+ this.equivalences == that.equivalences &&
+ this.conjunctions2 == that.conjunctions2 &&
+ this.conjunctions3 == that.conjunctions3 &&
+ this.conjunctions4 == that.conjunctions4 &&
+ this.conjunctionsN == that.conjunctionsN &&
+ this.disjunctions2 == that.disjunctions2 &&
+ this.disjunctions3 == that.disjunctions3 &&
+ this.disjunctions4 == that.disjunctions4 &&
+ this.disjunctionsN == that.disjunctionsN &&
+ this.ccCounter == that.ccCounter &&
+ this.pbCounter == that.pbCounter &&
+ this.cnfCounter == that.cnfCounter &&
+ Objects.equals(this.name, that.name);
}
@Override
public int hashCode() {
- return Objects.hash(name, positiveLiterals, negativeLiterals, negations, implications, equivalences, conjunctions2,
- conjunctions3, conjunctions4, conjunctionsN, disjunctions2, disjunctions3, disjunctions4, disjunctionsN,
- ccCounter, pbCounter, cnfCounter);
+ return Objects.hash(this.name, this.positiveLiterals, this.negativeLiterals, this.negations, this.implications, this.equivalences, this.conjunctions2,
+ this.conjunctions3, this.conjunctions4, this.conjunctionsN, this.disjunctions2, this.disjunctions3, this.disjunctions4, this.disjunctionsN,
+ this.ccCounter, this.pbCounter, this.cnfCounter);
}
@Override
public String toString() {
return "FormulaFactoryStatistics{" +
- "name='" + name + '\'' +
- ", positiveLiterals=" + positiveLiterals +
- ", negativeLiterals=" + negativeLiterals +
- ", negations=" + negations +
- ", implications=" + implications +
- ", equivalences=" + equivalences +
- ", conjunctions2=" + conjunctions2 +
- ", conjunctions3=" + conjunctions3 +
- ", conjunctions4=" + conjunctions4 +
- ", conjunctionsN=" + conjunctionsN +
- ", disjunctions2=" + disjunctions2 +
- ", disjunctions3=" + disjunctions3 +
- ", disjunctions4=" + disjunctions4 +
- ", disjunctionsN=" + disjunctionsN +
- ", ccCounter=" + ccCounter +
- ", pbCounter=" + pbCounter +
- ", cnfCounter=" + cnfCounter +
+ "name='" + this.name + '\'' +
+ ", positiveLiterals=" + this.positiveLiterals +
+ ", negativeLiterals=" + this.negativeLiterals +
+ ", negations=" + this.negations +
+ ", implications=" + this.implications +
+ ", equivalences=" + this.equivalences +
+ ", conjunctions2=" + this.conjunctions2 +
+ ", conjunctions3=" + this.conjunctions3 +
+ ", conjunctions4=" + this.conjunctions4 +
+ ", conjunctionsN=" + this.conjunctionsN +
+ ", disjunctions2=" + this.disjunctions2 +
+ ", disjunctions3=" + this.disjunctions3 +
+ ", disjunctions4=" + this.disjunctions4 +
+ ", disjunctionsN=" + this.disjunctionsN +
+ ", ccCounter=" + this.ccCounter +
+ ", pbCounter=" + this.pbCounter +
+ ", cnfCounter=" + this.cnfCounter +
'}';
}
}
diff --git a/src/main/java/org/logicng/formulas/NAryOperator.java b/src/main/java/org/logicng/formulas/NAryOperator.java
index bc94e77c..e6cfe3e2 100644
--- a/src/main/java/org/logicng/formulas/NAryOperator.java
+++ b/src/main/java/org/logicng/formulas/NAryOperator.java
@@ -61,7 +61,7 @@ public abstract class NAryOperator extends Formula {
*/
NAryOperator(final FType type, final Collection operands, final FormulaFactory f) {
super(type, f);
- this.operands = operands.toArray(new Formula[operands.size()]);
+ this.operands = operands.toArray(new Formula[0]);
this.hashCode = 0;
}
@@ -87,7 +87,7 @@ public long numberOfNodes() {
@Override
public int numberOfOperands() {
- return operands.length;
+ return this.operands.length;
}
@Override
@@ -127,7 +127,7 @@ public Formula restrict(final Assignment assignment) {
final LinkedHashSet nops = new LinkedHashSet<>();
for (final Formula op : this.operands)
nops.add(op.restrict(assignment));
- return f.naryOperator(type, nops);
+ return this.f.naryOperator(this.type, nops);
}
@Override
@@ -143,7 +143,7 @@ public boolean containsNode(final Formula formula) {
final List fOps = new ArrayList<>(formula.numberOfOperands());
for (final Formula op : formula)
fOps.add(op);
- for (Formula op : this.operands) {
+ for (final Formula op : this.operands) {
fOps.remove(op);
if (op.containsNode(formula))
return true;
@@ -156,12 +156,12 @@ public Formula substitute(final Substitution substitution) {
final LinkedHashSet nops = new LinkedHashSet<>();
for (final Formula op : this.operands)
nops.add(op.substitute(substitution));
- return f.naryOperator(type, nops);
+ return this.f.naryOperator(this.type, nops);
}
@Override
public Formula negate() {
- return f.not(this);
+ return this.f.not(this);
}
@Override
@@ -171,7 +171,7 @@ public Formula nnf() {
final LinkedHashSet nops = new LinkedHashSet<>();
for (final Formula op : this.operands)
nops.add(op.nnf());
- nnf = f.naryOperator(type, nops);
+ nnf = this.f.naryOperator(this.type, nops);
this.transformationCache.put(NNF, nnf);
}
return nnf;
@@ -182,10 +182,10 @@ public Formula nnf() {
* @param shift shift value
* @return hashcode
*/
- protected int hashCode(int shift) {
+ protected int hashCode(final int shift) {
if (this.hashCode == 0) {
int temp = 1;
- for (Formula formula : this.operands)
+ for (final Formula formula : this.operands)
temp += formula.hashCode();
temp *= shift;
this.hashCode = temp;
@@ -200,14 +200,14 @@ public Iterator iterator() {
@Override
public boolean hasNext() {
- return i < operands.length;
+ return this.i < NAryOperator.this.operands.length;
}
@Override
public Formula next() {
- if (i == operands.length)
+ if (this.i == NAryOperator.this.operands.length)
throw new NoSuchElementException();
- return operands[i++];
+ return NAryOperator.this.operands[this.i++];
}
@Override
diff --git a/src/main/java/org/logicng/formulas/cache/TransformationCacheEntry.java b/src/main/java/org/logicng/formulas/cache/TransformationCacheEntry.java
index afa7c936..2d03b84a 100644
--- a/src/main/java/org/logicng/formulas/cache/TransformationCacheEntry.java
+++ b/src/main/java/org/logicng/formulas/cache/TransformationCacheEntry.java
@@ -41,10 +41,12 @@ public enum TransformationCacheEntry implements CacheEntry {
TSEITIN("Tseitin conjunctive normal form"),
TSEITIN_VARIABLE("Tseitin variable"),
FACTORIZED_CNF("factorized conjunctive normal form"),
+ BDD_CNF("conjunctive normal form via BDD"),
FACTORIZED_DNF("factorized disjunctive normal form"),
AIG("and-inverter graph"),
UNIT_PROPAGATION("unit propagation"),
- DISTRIBUTIVE_SIMPLIFICATION("distributive simplification");
+ DISTRIBUTIVE_SIMPLIFICATION("distributive simplification"),
+ ANONYMIZATION("anonymization");
private final String description;
@@ -58,6 +60,6 @@ public enum TransformationCacheEntry implements CacheEntry {
@Override
public String description() {
- return "TransformationCacheEntry{description=" + description + "}";
+ return "TransformationCacheEntry{description=" + this.description + "}";
}
}
diff --git a/src/main/java/org/logicng/graphs/datastructures/Hypergraph.java b/src/main/java/org/logicng/graphs/datastructures/Hypergraph.java
new file mode 100644
index 00000000..5b3cf87b
--- /dev/null
+++ b/src/main/java/org/logicng/graphs/datastructures/Hypergraph.java
@@ -0,0 +1,120 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.graphs.datastructures;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.LinkedHashSet;
+import java.util.Set;
+
+/**
+ * A simple data structure for a hypergraph.
+ * @param the content type of the graph's nodes
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class Hypergraph {
+
+ private final LinkedHashSet> nodes;
+ private final LinkedHashSet> edges;
+
+ /**
+ * Constructs a new hypergraph.
+ */
+ public Hypergraph() {
+ this.nodes = new LinkedHashSet<>();
+ this.edges = new LinkedHashSet<>();
+ }
+
+ /**
+ * Returns the set of nodes of the hypergraph.
+ * @return the set of nodes of the hypergraph
+ */
+ public Set> nodes() {
+ return this.nodes;
+ }
+
+ /**
+ * Returns the set of edges of the hypergraph.
+ * @return the set of edges of the hypergraph
+ */
+ public Set> edges() {
+ return this.edges;
+ }
+
+ /**
+ * Adds a node to the hypergraph.
+ * @param node the node
+ */
+ void addNode(final HypergraphNode node) {
+ this.nodes.add(node);
+ }
+
+ /**
+ * Adds an edge to the hypergraph.
+ * @param edge the edge
+ */
+ public void addEdge(final HypergraphEdge edge) {
+ this.edges.add(edge);
+ }
+
+ /**
+ * Adds an edges to the hypergraph. The edge is represented by its connected nodes.
+ * @param nodes the nodes of the edge
+ */
+ public void addEdge(final Collection> nodes) {
+ final HypergraphEdge edge = new HypergraphEdge<>(nodes);
+ this.nodes.addAll(nodes);
+ this.edges.add(edge);
+ }
+
+ /**
+ * Adds an edges to the hypergraph. The edge is represented by its connected nodes.
+ * @param nodes the nodes of the edge
+ */
+ public void addEdge(final HypergraphNode... nodes) {
+ addEdge(Arrays.asList(nodes));
+ }
+
+ /**
+ * Adds a set of edges to the hypergraph.
+ * @param edges the edges
+ */
+ public void addEdges(final Collection> edges) {
+ this.edges.addAll(edges);
+ }
+
+ @Override
+ public String toString() {
+ return "Hypergraph{" +
+ "nodes=" + this.nodes +
+ ", edges=" + this.edges +
+ '}';
+ }
+}
diff --git a/src/main/java/org/logicng/graphs/datastructures/HypergraphEdge.java b/src/main/java/org/logicng/graphs/datastructures/HypergraphEdge.java
new file mode 100644
index 00000000..02d26271
--- /dev/null
+++ b/src/main/java/org/logicng/graphs/datastructures/HypergraphEdge.java
@@ -0,0 +1,109 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.graphs.datastructures;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.LinkedHashSet;
+import java.util.Map;
+import java.util.Objects;
+import java.util.Set;
+
+/**
+ * An edge in a hypergraph.
+ * @param the content type of the graph's nodes
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class HypergraphEdge {
+
+ private final LinkedHashSet> nodes;
+
+ /**
+ * Constructs a new edge for a given set of nodes.
+ * @param nodes the nodes connected by this edge
+ */
+ public HypergraphEdge(final Collection> nodes) {
+ this.nodes = new LinkedHashSet<>(nodes);
+ for (final HypergraphNode node : nodes)
+ node.addEdge(this);
+ }
+
+ /**
+ * Constructs a new edge for a given set of nodes.
+ * @param nodes the nodes connected by this edge
+ */
+ public HypergraphEdge(HypergraphNode... nodes) {
+ this(Arrays.asList(nodes));
+ }
+
+ /**
+ * Returns the nodes connected by this edge.
+ * @return the nodes connected by this edge
+ */
+ public Set> nodes() {
+ return this.nodes;
+ }
+
+ /**
+ * Computes the center of gravity for this edge (see Aloul, Markov, and Sakallah).
+ * @param nodeOrdering the node ordering for which the COG is computed
+ * @return the center of gravity for this edge
+ */
+ public double centerOfGravity(final Map, Integer> nodeOrdering) {
+ int cog = 0;
+ for (final HypergraphNode node : this.nodes) {
+ final Integer level = nodeOrdering.get(node);
+ if (level == null)
+ throw new IllegalStateException("Could not find node " + node + " in the node ordering.");
+ cog += level;
+ }
+ return (double) cog / this.nodes.size();
+ }
+
+ @Override
+ public boolean equals(final Object o) {
+ if (this == o) return true;
+ if (o == null || getClass() != o.getClass()) return false;
+ final HypergraphEdge that = (HypergraphEdge) o;
+ return Objects.equals(this.nodes, that.nodes);
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(this.nodes);
+ }
+
+ @Override
+ public String toString() {
+ return "HypergraphEdge{" +
+ "nodes=" + this.nodes +
+ '}';
+ }
+}
diff --git a/src/main/java/org/logicng/graphs/datastructures/HypergraphNode.java b/src/main/java/org/logicng/graphs/datastructures/HypergraphNode.java
new file mode 100644
index 00000000..d88694c1
--- /dev/null
+++ b/src/main/java/org/logicng/graphs/datastructures/HypergraphNode.java
@@ -0,0 +1,124 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2016 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.graphs.datastructures;
+
+import java.util.LinkedHashSet;
+import java.util.Map;
+import java.util.Objects;
+import java.util.Set;
+
+/**
+ * A node in an hypergraph.
+ * @param the content type of the graph's nodes
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class HypergraphNode {
+
+ private final Hypergraph graph;
+ private final T content;
+ private final LinkedHashSet> edges;
+
+ /**
+ * Constructs a new hypergraph node for a given graph and content.
+ * @param graph the graph for this node
+ * @param content the content of this node
+ */
+ public HypergraphNode(final Hypergraph graph, final T content) {
+ this.graph = graph;
+ this.content = content;
+ this.edges = new LinkedHashSet<>();
+ this.graph.addNode(this);
+ }
+
+ /**
+ * Returns the hypergraph of this node.
+ * @return the hypergraph of this node
+ */
+ public Hypergraph graph() {
+ return this.graph;
+ }
+
+ /**
+ * Returns the content of this node.
+ * @return the content of this node
+ */
+ public T content() {
+ return this.content;
+ }
+
+ /**
+ * Returns the edges which are connected with this node.
+ * @return the edges which are connected with this node
+ */
+ public Set> edges() {
+ return this.edges;
+ }
+
+ /**
+ * Adds an edge to this node.
+ * @param edge the edge
+ */
+ public void addEdge(final HypergraphEdge edge) {
+ this.edges.add(edge);
+ }
+
+ /**
+ * Computes the tentative new location for this node (see Aloul, Markov, and Sakallah).
+ * @param nodeOrdering the node ordering for which the COG is computed
+ * @return the tentative new location for this node
+ */
+ public double computeTentativeNewLocation(final Map, Integer> nodeOrdering) {
+ double newLocation = 0;
+ for (final HypergraphEdge edge : this.edges)
+ newLocation += edge.centerOfGravity(nodeOrdering);
+ return newLocation / this.edges.size();
+ }
+
+ @Override
+ public boolean equals(final Object o) {
+ if (this == o) return true;
+ if (o == null || getClass() != o.getClass()) return false;
+ final HypergraphNode that = (HypergraphNode) o;
+ return Objects.equals(this.graph, that.graph) &&
+ Objects.equals(this.content, that.content);
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(this.graph, this.content);
+ }
+
+ @Override
+ public String toString() {
+ return "HypergraphNode{" +
+ "content=" + this.content +
+ '}';
+ }
+}
diff --git a/src/main/java/org/logicng/graphs/generators/HypergraphGenerator.java b/src/main/java/org/logicng/graphs/generators/HypergraphGenerator.java
new file mode 100644
index 00000000..68cae0aa
--- /dev/null
+++ b/src/main/java/org/logicng/graphs/generators/HypergraphGenerator.java
@@ -0,0 +1,109 @@
+package org.logicng.graphs.generators;
+
+import org.logicng.formulas.FType;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Variable;
+import org.logicng.graphs.datastructures.Hypergraph;
+import org.logicng.graphs.datastructures.HypergraphNode;
+import org.logicng.predicates.CNFPredicate;
+
+import java.util.Arrays;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.SortedSet;
+
+/**
+ * A generator for hypergraphs from formulas.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class HypergraphGenerator {
+
+ /**
+ * Generates a hypergraph from a CNF given as a list of clauses. Each variable is represented by a node in the
+ * hypergraph, each clause is represented by a hyperedge between all variables of the clause.
+ * @param cnf the list of clauses of the CNF for the hypergraph
+ * @return the hypergraph for the CNF formula
+ */
+ public static Hypergraph fromCNF(final Formula... cnf) {
+ return fromCNF(Arrays.asList(cnf));
+ }
+
+ /**
+ * Generates a hypergraph from a CNF given as a list of clauses. Each variable is represented by a node in the
+ * hypergraph, each clause is represented by a hyperedge between all variables of the clause.
+ * @param cnf the list of clauses of the CNF for the hypergraph
+ * @return the hypergraph for the CNF formula
+ */
+ public static Hypergraph fromCNF(final List cnf) {
+ final Hypergraph hypergraph = new Hypergraph<>();
+ final Map> nodes = new HashMap<>();
+ for (final Formula clause : cnf)
+ switch (clause.type()) {
+ case PBC:
+ case EQUIV:
+ case IMPL:
+ case NOT:
+ case AND:
+ throw new IllegalStateException("Unexpected element in clause: " + clause);
+ case LITERAL:
+ case OR:
+ addClause(clause, hypergraph, nodes);
+ break;
+ }
+ return hypergraph;
+ }
+
+ /**
+ * Generates a hypergraph from a CNF. Each variable is represented by a node in the hypergraph, each clause
+ * is represented by a hyperedge between all variables of the clause.
+ * @param cnf the CNF formula for the hypergraph
+ * @return the hypergraph for the CNF formula
+ */
+ public static Hypergraph fromCNF(final Formula cnf) {
+ if (!cnf.holds(new CNFPredicate()))
+ throw new IllegalArgumentException("Cannot generate a hypergraph from a non-cnf formula");
+ final Hypergraph hypergraph = new Hypergraph<>();
+ final Map> nodes = new HashMap<>();
+ switch (cnf.type()) {
+ case PBC:
+ case EQUIV:
+ case IMPL:
+ case NOT:
+ throw new IllegalStateException("Unexpected element in CNF: " + cnf);
+ case LITERAL:
+ case OR:
+ addClause(cnf, hypergraph, nodes);
+ break;
+ case AND:
+ for (final Formula clause : cnf)
+ addClause(clause, hypergraph, nodes);
+ break;
+ }
+ return hypergraph;
+ }
+
+ /**
+ * Adds a single clause to the given hypergraph and updates the variable to node mapping.
+ * @param formula the clause
+ * @param hypergraph the current hypergraph
+ * @param nodes the mapping from variables in the CNF to nodes in the hypergraph
+ */
+ private static void addClause(final Formula formula, final Hypergraph hypergraph, final Map> nodes) {
+ assert formula.type() == FType.LITERAL || formula.type() == FType.OR;
+ final SortedSet variables = formula.variables();
+ final Set> clause = new HashSet<>();
+ for (final Variable variable : variables) {
+ HypergraphNode node = nodes.get(variable);
+ if (node == null) {
+ node = new HypergraphNode<>(hypergraph, variable);
+ nodes.put(variable, node);
+ }
+ clause.add(node);
+ }
+ hypergraph.addEdge(clause);
+ }
+}
diff --git a/src/main/java/org/logicng/io/parsers/FormulaParser.java b/src/main/java/org/logicng/io/parsers/FormulaParser.java
index 4fa6857f..9dfcaad4 100644
--- a/src/main/java/org/logicng/io/parsers/FormulaParser.java
+++ b/src/main/java/org/logicng/io/parsers/FormulaParser.java
@@ -28,9 +28,18 @@
package org.logicng.io.parsers;
+import org.antlr.v4.runtime.BailErrorStrategy;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.Lexer;
+import org.antlr.v4.runtime.misc.ParseCancellationException;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
+import java.io.IOException;
+import java.io.InputStream;
+
/**
* Super class for a formula parser.
* @version 1.2
@@ -39,22 +48,78 @@
public abstract class FormulaParser {
private final FormulaFactory f;
+ private Lexer lexer;
+ private ParserWithFormula parser;
/**
* Constructor.
* @param f the formula factory
*/
- public FormulaParser(FormulaFactory f) {
+ FormulaParser(final FormulaFactory f) {
this.f = f;
}
+ /**
+ * Sets the internal lexer and the parser.
+ * @param lexer the lexer
+ * @param parser the parser
+ */
+ void setLexerAndParser(final Lexer lexer, final ParserWithFormula parser) {
+ this.lexer = lexer;
+ this.parser = parser;
+ this.parser.setFormulaFactory(this.f);
+ this.lexer.removeErrorListeners();
+ this.parser.removeErrorListeners();
+ this.parser.setErrorHandler(new BailErrorStrategy());
+ }
+
+ /**
+ * Parses and returns a given input stream.
+ * @param inputStream an input stream
+ * @return the {@link Formula} representation of this stream
+ * @throws ParserException if there was a problem with the input stream
+ */
+ public Formula parse(final InputStream inputStream) throws ParserException {
+ if (inputStream == null) {
+ return this.f.verum();
+ }
+ try {
+ final CharStream input = CharStreams.fromStream(inputStream);
+ this.lexer.setInputStream(input);
+ final CommonTokenStream tokens = new CommonTokenStream(this.lexer);
+ this.parser.setInputStream(tokens);
+ return this.parser.getParsedFormula();
+ } catch (final IOException e) {
+ throw new ParserException("IO exception when parsing the formula", e);
+ } catch (final ParseCancellationException e) {
+ throw new ParserException("Parse cancellation exception when parsing the formula", e);
+ } catch (final LexerException e) {
+ throw new ParserException("Lexer exception when parsing the formula.", e);
+ }
+ }
+
/**
* Parses and returns a given string.
- * @param string the input string
- * @return the {@link Formula} representation of the given string
- * @throws ParserException if there was a problem parsing the string
+ * @param in a string
+ * @return the {@link Formula} representation of this string
+ * @throws ParserException if the string was not a valid formula
*/
- public abstract Formula parse(final String string) throws ParserException;
+ public Formula parse(final String in) throws ParserException {
+ if (in == null || in.isEmpty()) {
+ return this.f.verum();
+ }
+ try {
+ final CharStream input = CharStreams.fromString(in);
+ this.lexer.setInputStream(input);
+ final CommonTokenStream tokens = new CommonTokenStream(this.lexer);
+ this.parser.setInputStream(tokens);
+ return this.parser.getParsedFormula();
+ } catch (final ParseCancellationException e) {
+ throw new ParserException("Parse cancellation exception when parsing the formula", e);
+ } catch (final LexerException e) {
+ throw new ParserException("Lexer exception when parsing the formula.", e);
+ }
+ }
/**
* Returns the factory of this parser.
@@ -66,6 +131,6 @@ public FormulaFactory factory() {
@Override
public String toString() {
- return this.getClass().getSimpleName();
+ return getClass().getSimpleName();
}
}
diff --git a/src/main/java/org/logicng/io/parsers/ParserWithFormula.java b/src/main/java/org/logicng/io/parsers/ParserWithFormula.java
new file mode 100644
index 00000000..5d70ff1a
--- /dev/null
+++ b/src/main/java/org/logicng/io/parsers/ParserWithFormula.java
@@ -0,0 +1,38 @@
+package org.logicng.io.parsers;
+
+import org.antlr.v4.runtime.Parser;
+import org.antlr.v4.runtime.TokenStream;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaFactory;
+
+/**
+ * Abstract super class for parsers which have a formula factory and return a formula.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public abstract class ParserWithFormula extends Parser {
+
+ protected FormulaFactory f;
+
+ /**
+ * Constructor.
+ * @param input the token stream (e.g. a lexer) for the parser
+ */
+ public ParserWithFormula(final TokenStream input) {
+ super(input);
+ }
+
+ /**
+ * Sets the LogicNG formula factory for this parser
+ * @param f the LogicNG formula factory
+ */
+ public void setFormulaFactory(final FormulaFactory f) {
+ this.f = f;
+ }
+
+ /**
+ * Returns the parsed formula.
+ * @return the parsed formula
+ */
+ public abstract Formula getParsedFormula();
+}
diff --git a/src/main/java/org/logicng/io/parsers/PropositionalParser.java b/src/main/java/org/logicng/io/parsers/PropositionalParser.java
index d9c8f19b..cba5bdd8 100644
--- a/src/main/java/org/logicng/io/parsers/PropositionalParser.java
+++ b/src/main/java/org/logicng/io/parsers/PropositionalParser.java
@@ -28,12 +28,7 @@
package org.logicng.io.parsers;
-import org.antlr.v4.runtime.BailErrorStrategy;
-import org.antlr.v4.runtime.CharStream;
-import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
-import org.antlr.v4.runtime.misc.ParseCancellationException;
-import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
/**
@@ -60,38 +55,15 @@
*/
public final class PropositionalParser extends FormulaParser {
- private final PropositionalLexer lexer;
- private final LogicNGPropositionalParser parser;
-
/**
* Constructs a new parser.
* @param f the formula factory
*/
public PropositionalParser(final FormulaFactory f) {
super(f);
- this.lexer = new PropositionalLexer(null);
- CommonTokenStream tokens = new CommonTokenStream(this.lexer);
- this.parser = new LogicNGPropositionalParser(tokens);
- this.parser.setFormulaFactory(f);
- this.lexer.removeErrorListeners();
- this.parser.removeErrorListeners();
- this.parser.setErrorHandler(new BailErrorStrategy());
- }
-
- @Override
- public Formula parse(final String string) throws ParserException {
- if (string == null || string.isEmpty())
- return factory().verum();
- try {
- CharStream input = CharStreams.fromString(string);
- this.lexer.setInputStream(input);
- CommonTokenStream tokens = new CommonTokenStream(this.lexer);
- this.parser.setInputStream(tokens);
- return this.parser.formula().f;
- } catch (ParseCancellationException e) {
- throw new ParserException("Parse cancellation exception when parsing the formula", e);
- } catch (LexerException e) {
- throw new ParserException("Lexer exception when parsing the formula.", e);
- }
+ final PropositionalLexer lexer = new PropositionalLexer(null);
+ final CommonTokenStream tokens = new CommonTokenStream(lexer);
+ final ParserWithFormula parser = new LogicNGPropositionalParser(tokens);
+ setLexerAndParser(lexer, parser);
}
}
diff --git a/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java b/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java
index 19c17d85..eaf0f623 100644
--- a/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java
+++ b/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java
@@ -28,12 +28,7 @@
package org.logicng.io.parsers;
-import org.antlr.v4.runtime.BailErrorStrategy;
-import org.antlr.v4.runtime.CharStream;
-import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
-import org.antlr.v4.runtime.misc.ParseCancellationException;
-import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
/**
@@ -70,38 +65,15 @@
*/
public final class PseudoBooleanParser extends FormulaParser {
- private final PseudoBooleanLexer lexer;
- private final LogicNGPseudoBooleanParser parser;
-
/**
* Constructs a new parser for pseudo boolean formulas.
* @param f the formula factory
*/
public PseudoBooleanParser(final FormulaFactory f) {
super(f);
- this.lexer = new PseudoBooleanLexer(null);
- CommonTokenStream tokens = new CommonTokenStream(this.lexer);
- this.parser = new LogicNGPseudoBooleanParser(tokens);
- this.parser.setFormulaFactory(f);
- this.lexer.removeErrorListeners();
- this.parser.removeErrorListeners();
- this.parser.setErrorHandler(new BailErrorStrategy());
- }
-
- @Override
- public Formula parse(final String string) throws ParserException {
- if (string == null || string.isEmpty())
- return factory().verum();
- try {
- CharStream input = CharStreams.fromString(string);
- this.lexer.setInputStream(input);
- CommonTokenStream tokens = new CommonTokenStream(this.lexer);
- this.parser.setInputStream(tokens);
- return this.parser.formula().f;
- } catch (ParseCancellationException e) {
- throw new ParserException("Parse cancellation exception when parsing the formula", e);
- } catch (LexerException e) {
- throw new ParserException("Lexer exception when parsing the formula.", e);
- }
+ final PseudoBooleanLexer lexer = new PseudoBooleanLexer(null);
+ final CommonTokenStream tokens = new CommonTokenStream(lexer);
+ final ParserWithFormula parser = new LogicNGPseudoBooleanParser(tokens);
+ setLexerAndParser(lexer, parser);
}
}
diff --git a/src/main/java/org/logicng/io/readers/DimacsReader.java b/src/main/java/org/logicng/io/readers/DimacsReader.java
index 71e2f623..a8e606a2 100644
--- a/src/main/java/org/logicng/io/readers/DimacsReader.java
+++ b/src/main/java/org/logicng/io/readers/DimacsReader.java
@@ -31,7 +31,6 @@
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Literal;
-import org.logicng.io.parsers.ParserException;
import java.io.BufferedReader;
import java.io.File;
@@ -64,10 +63,9 @@ private DimacsReader() {
* @param file the file
* @param f the formula factory
* @return the list of formulas (clauses)
- * @throws IOException if there was a problem reading the file
- * @throws ParserException if there was a problem parsing the formula
+ * @throws IOException if there was a problem reading the file
*/
- public static List readCNF(final File file, final FormulaFactory f) throws IOException, ParserException {
+ public static List readCNF(final File file, final FormulaFactory f) throws IOException {
return readCNF(file, f, "v");
}
@@ -80,17 +78,17 @@ public static List readCNF(final File file, final FormulaFactory f) thr
* @throws IOException if there was a problem reading the file
*/
public static List readCNF(final File file, final FormulaFactory f, final String prefix) throws IOException {
- List result = new ArrayList<>();
+ final List result = new ArrayList<>();
try (final BufferedReader br = new BufferedReader(new FileReader(file))) {
while (br.ready()) {
final String line = br.readLine();
if (!line.startsWith("c") && !line.startsWith("p") && !line.trim().isEmpty()) {
- String[] split = line.split("\\s+");
+ final String[] split = line.split("\\s+");
if (!"0".equals(split[split.length - 1].trim()))
throw new IllegalArgumentException("Line " + line + " did not end with 0.");
- LinkedHashSet vars = new LinkedHashSet<>(split.length - 1);
+ final LinkedHashSet vars = new LinkedHashSet<>(split.length - 1);
for (int i = 0; i < split.length - 1; i++) {
- String lit = split[i].trim();
+ final String lit = split[i].trim();
if (!lit.isEmpty()) {
if (lit.startsWith("-"))
vars.add(f.literal(prefix + split[i].trim().substring(1), false));
@@ -111,10 +109,9 @@ public static List readCNF(final File file, final FormulaFactory f, fin
* @param fileName the file name
* @param f the formula factory
* @return the list of formulas (clauses)
- * @throws IOException if there was a problem reading the file
- * @throws ParserException if there was a problem parsing the formula
+ * @throws IOException if there was a problem reading the file
*/
- public static List readCNF(final String fileName, final FormulaFactory f) throws IOException, ParserException {
+ public static List readCNF(final String fileName, final FormulaFactory f) throws IOException {
return readCNF(new File(fileName), f, "v");
}
@@ -124,11 +121,9 @@ public static List readCNF(final String fileName, final FormulaFactory
* @param f the formula factory
* @param prefix the prefix for the variable names
* @return the list of formulas (clauses)
- * @throws IOException if there was a problem reading the file
- * @throws ParserException if there was a problem parsing the formula
+ * @throws IOException if there was a problem reading the file
*/
- public static List readCNF(final String fileName, final FormulaFactory f, final String prefix)
- throws IOException, ParserException {
+ public static List readCNF(final String fileName, final FormulaFactory f, final String prefix) throws IOException {
return readCNF(new File(fileName), f, prefix);
}
diff --git a/src/main/java/org/logicng/solvers/MiniSat.java b/src/main/java/org/logicng/solvers/MiniSat.java
index 4c7db2e5..f95f3f4a 100644
--- a/src/main/java/org/logicng/solvers/MiniSat.java
+++ b/src/main/java/org/logicng/solvers/MiniSat.java
@@ -87,7 +87,7 @@ private enum SolverStyle {MINISAT, GLUCOSE, MINICARD}
private final SolverStyle style;
private final LNGIntVector validStates;
private final boolean initialPhase;
- private boolean incremental;
+ private final boolean incremental;
private int nextStateId;
/**
@@ -182,7 +182,7 @@ public static MiniSat miniCard(final FormulaFactory f, final MiniSatConfig confi
}
@Override
- public void add(final Formula formula, Proposition proposition) {
+ public void add(final Formula formula, final Proposition proposition) {
if (formula.type() == FType.PBC) {
final PBConstraint constraint = (PBConstraint) formula;
this.result = UNDEF;
@@ -199,7 +199,7 @@ else if (constraint.comparator() == CType.EQ && constraint.rhs() == 1) {
this.addClauseSet(constraint.cnf(), proposition);
} else {
final EncodingResult result = EncodingResult.resultForMiniSat(this.f, this);
- ccEncoder.encode(constraint, result);
+ this.ccEncoder.encode(constraint, result);
}
} else
this.addClauseSet(constraint.cnf(), proposition);
@@ -221,11 +221,11 @@ public void addWithoutUnknown(final Formula formula) {
}
@Override
- public CCIncrementalData addIncrementalCC(PBConstraint cc) {
+ public CCIncrementalData addIncrementalCC(final PBConstraint cc) {
if (!cc.isCC())
throw new IllegalArgumentException("Cannot generate an incremental cardinality constraint on a pseudo-Boolean constraint");
final EncodingResult result = EncodingResult.resultForMiniSat(this.f, this);
- return ccEncoder.encodeIncremental(cc, result);
+ return this.ccEncoder.encodeIncremental(cc, result);
}
@Override
@@ -235,7 +235,7 @@ protected void addClause(final Formula formula, final Proposition proposition) {
}
@Override
- protected void addClauseWithRelaxation(Variable relaxationVar, Formula formula) {
+ protected void addClauseWithRelaxation(final Variable relaxationVar, final Formula formula) {
this.result = UNDEF;
final SortedSet literals = new TreeSet<>(formula.literals());
literals.add(relaxationVar);
@@ -247,7 +247,7 @@ public Tristate sat(final SATHandler handler) {
if (this.result != UNDEF)
return this.result;
this.result = this.solver.solve(handler);
- return result;
+ return this.result;
}
@Override
@@ -255,10 +255,10 @@ public Tristate sat(final SATHandler handler, final Literal literal) {
final LNGIntVector clauseVec = new LNGIntVector(1);
int index = this.solver.idxForName(literal.name());
if (index == -1) {
- index = this.solver.newVar(!initialPhase, true);
+ index = this.solver.newVar(!this.initialPhase, true);
this.solver.addName(literal.name(), index);
}
- int litNum = literal.phase() ? index * 2 : (index * 2) ^ 1;
+ final int litNum = literal.phase() ? index * 2 : (index * 2) ^ 1;
clauseVec.push(litNum);
this.result = this.solver.solve(handler, clauseVec);
return this.result;
@@ -271,10 +271,10 @@ public Tristate sat(final SATHandler handler, final Collection variables) {
throw new IllegalStateException("Cannot get a model as long as the formula is not solved. Call 'sat' first.");
final LNGIntVector relevantIndices = variables == null ? null : new LNGIntVector(variables.size());
if (relevantIndices != null) {
- for (Variable var : variables) {
+ for (final Variable var : variables) {
relevantIndices.push(this.solver.idxForName(var.name()));
}
}
@@ -306,7 +306,7 @@ public List enumerateAllModels(final Collection variables)
}
@Override
- public List enumerateAllModels(Collection variables, Collection additionalVariables) {
+ public List enumerateAllModels(final Collection variables, final Collection additionalVariables) {
return enumerateAllModels(variables, additionalVariables, null);
}
@@ -316,10 +316,10 @@ public List enumerateAllModels(final Collection literals,
}
@Override
- public List enumerateAllModels(Collection variables, Collection additionalVariables, ModelEnumerationHandler handler) {
- List models = new LinkedList<>();
+ public List enumerateAllModels(final Collection variables, final Collection additionalVariables, final ModelEnumerationHandler handler) {
+ final List models = new LinkedList<>();
SolverState stateBeforeEnumeration = null;
- if (this.style == SolverStyle.MINISAT && incremental)
+ if (this.style == SolverStyle.MINISAT && this.incremental)
stateBeforeEnumeration = this.saveState();
boolean proceed = true;
SortedSet allVariables = new TreeSet<>();
@@ -332,12 +332,12 @@ public List enumerateAllModels(Collection variables, Colle
final LNGIntVector relevantIndices = variables == null ? null : new LNGIntVector(variables.size());
LNGIntVector relevantAllIndices = null;
if (relevantIndices != null) {
- for (Variable var : variables) {
+ for (final Variable var : variables) {
relevantIndices.push(this.solver.idxForName(var.name()));
}
relevantAllIndices = additionalVariables.isEmpty() ? relevantIndices : new LNGIntVector(allVariables.size());
if (!additionalVariables.isEmpty()) {
- for (Variable var : allVariables) {
+ for (final Variable var : allVariables) {
relevantAllIndices.push(this.solver.idxForName(var.name()));
}
}
@@ -349,14 +349,14 @@ public List enumerateAllModels(Collection variables, Colle
models.add(model);
proceed = handler == null || handler.foundModel(model);
if (model.size() > 0) {
- LNGIntVector blockingClause = generateBlockingClause(modelFromSolver, relevantIndices);
+ final LNGIntVector blockingClause = generateBlockingClause(modelFromSolver, relevantIndices);
this.solver.addClause(blockingClause, null);
this.result = UNDEF;
} else {
break;
}
}
- if (this.style == SolverStyle.MINISAT && incremental)
+ if (this.style == SolverStyle.MINISAT && this.incremental)
this.loadState(stateBeforeEnumeration);
return models;
}
@@ -373,8 +373,10 @@ private LNGIntVector generateBlockingClause(final LNGBooleanVector modelFromSolv
blockingClause = new LNGIntVector(relevantVars.size());
for (int i = 0; i < relevantVars.size(); i++) {
final int varIndex = relevantVars.get(i);
- final boolean varAssignment = modelFromSolver.get(varIndex);
- blockingClause.push(varAssignment ? (varIndex * 2) ^ 1 : varIndex * 2);
+ if (varIndex != -1) {
+ final boolean varAssignment = modelFromSolver.get(varIndex);
+ blockingClause.push(varAssignment ? (varIndex * 2) ^ 1 : varIndex * 2);
+ }
}
} else {
blockingClause = new LNGIntVector(modelFromSolver.size());
@@ -389,15 +391,15 @@ private LNGIntVector generateBlockingClause(final LNGBooleanVector modelFromSolv
@Override
public SolverState saveState() {
final int id = this.nextStateId++;
- validStates.push(id);
+ this.validStates.push(id);
return new SolverState(id, this.solver.saveState());
}
@Override
public void loadState(final SolverState state) {
int index = -1;
- for (int i = validStates.size() - 1; i >= 0 && index == -1; i--)
- if (validStates.get(i) == state.id())
+ for (int i = this.validStates.size() - 1; i >= 0 && index == -1; i--)
+ if (this.validStates.get(i) == state.id())
index = i;
if (index == -1)
throw new IllegalArgumentException("The given solver state is not valid anymore.");
@@ -430,11 +432,11 @@ public UNSATCore unsatCore() {
if (this.underlyingSolver() instanceof GlucoseSyrup && this.config.incremental())
throw new IllegalStateException("Cannot compute an unsat core with Glucose in incremental mode.");
- DRUPTrim trimmer = new DRUPTrim();
+ final DRUPTrim trimmer = new DRUPTrim();
- Map clause2proposition = new HashMap<>();
+ final Map clause2proposition = new HashMap<>();
final LNGVector clauses = new LNGVector<>(this.underlyingSolver().pgOriginalClauses().size());
- for (MiniSatStyleSolver.ProofInformation pi : this.underlyingSolver().pgOriginalClauses()) {
+ for (final MiniSatStyleSolver.ProofInformation pi : this.underlyingSolver().pgOriginalClauses()) {
clauses.push(pi.clause());
final Formula clause = getFormulaForVector(pi.clause());
Proposition proposition = pi.proposition();
@@ -444,7 +446,7 @@ public UNSATCore unsatCore() {
}
if (containsEmptyClause(clauses)) {
- final Proposition emptyClause = clause2proposition.get(f.falsum());
+ final Proposition emptyClause = clause2proposition.get(this.f.falsum());
return new UNSATCore<>(Collections.singletonList(emptyClause), true);
}
@@ -452,7 +454,7 @@ public UNSATCore unsatCore() {
if (result.trivialUnsat())
return handleTrivialCase();
final LinkedHashSet propositions = new LinkedHashSet<>();
- for (LNGIntVector vector : result.unsatCore())
+ for (final LNGIntVector vector : result.unsatCore())
propositions.add(clause2proposition.get(getFormulaForVector(vector)));
return new UNSATCore<>(new ArrayList<>(propositions), false);
}
@@ -464,13 +466,13 @@ public UNSATCore unsatCore() {
*/
private LNGIntVector generateClauseVector(final Collection literals) {
final LNGIntVector clauseVec = new LNGIntVector(literals.size());
- for (Literal lit : literals) {
+ for (final Literal lit : literals) {
int index = this.solver.idxForName(lit.name());
if (index == -1) {
- index = this.solver.newVar(!initialPhase, true);
+ index = this.solver.newVar(!this.initialPhase, true);
this.solver.addName(lit.name(), index);
}
- int litNum = lit.phase() ? index * 2 : (index * 2) ^ 1;
+ final int litNum = lit.phase() ? index * 2 : (index * 2) ^ 1;
clauseVec.push(litNum);
}
return clauseVec;
@@ -487,13 +489,13 @@ private Assignment createAssignment(final LNGBooleanVector vec, final LNGIntVect
final Assignment model = new Assignment();
if (relevantIndices == null) {
for (int i = 0; i < vec.size(); i++) {
- model.addLiteral(f.literal(this.solver.nameForIdx(i), vec.get(i)));
+ model.addLiteral(this.f.literal(this.solver.nameForIdx(i), vec.get(i)));
}
} else {
for (int i = 0; i < relevantIndices.size(); i++) {
final int index = relevantIndices.get(i);
if (index != -1) {
- model.addLiteral(f.literal(this.solver.nameForIdx(index), vec.get(index)));
+ model.addLiteral(this.f.literal(this.solver.nameForIdx(index), vec.get(index)));
}
}
}
@@ -525,7 +527,7 @@ private UNSATCore handleTrivialCase() {
for (int j = i + 1; j < clauses.size(); j++) {
if (clauses.get(i).clause().size() == 1 && clauses.get(j).clause().size() == 1
&& clauses.get(i).clause().get(0) + clauses.get(j).clause().get(0) == 0) {
- LinkedHashSet propositions = new LinkedHashSet<>();
+ final LinkedHashSet propositions = new LinkedHashSet<>();
final Proposition pi = clauses.get(i).proposition();
final Proposition pj = clauses.get(j).proposition();
propositions.add(pi != null ? pi : new StandardProposition(getFormulaForVector(clauses.get(i).clause())));
@@ -537,20 +539,20 @@ private UNSATCore handleTrivialCase() {
}
private boolean containsEmptyClause(final LNGVector clauses) {
- for (LNGIntVector clause : clauses)
+ for (final LNGIntVector clause : clauses)
if (clause.empty())
return true;
return false;
}
- private Formula getFormulaForVector(LNGIntVector vector) {
+ private Formula getFormulaForVector(final LNGIntVector vector) {
final List literals = new ArrayList<>(vector.size());
for (int i = 0; i < vector.size(); i++) {
- int lit = vector.get(i);
- String varName = this.underlyingSolver().nameForIdx(Math.abs(lit) - 1);
- literals.add(f.literal(varName, lit > 0));
+ final int lit = vector.get(i);
+ final String varName = this.underlyingSolver().nameForIdx(Math.abs(lit) - 1);
+ literals.add(this.f.literal(varName, lit > 0));
}
- return f.or(literals);
+ return this.f.or(literals);
}
@Override
diff --git a/src/main/java/org/logicng/solvers/SATSolver.java b/src/main/java/org/logicng/solvers/SATSolver.java
index 509d0e8b..caf11c14 100644
--- a/src/main/java/org/logicng/solvers/SATSolver.java
+++ b/src/main/java/org/logicng/solvers/SATSolver.java
@@ -86,6 +86,24 @@ public void add(final Formula formula) {
*/
public abstract void addWithoutUnknown(final Formula formula);
+ /**
+ * Adds a given set of propositions to the solver.
+ * @param propositions the set of propositions
+ */
+ public void addPropositions(final Collection propositions) {
+ for (final Proposition proposition : propositions)
+ add(proposition);
+ }
+
+ /**
+ * Adds a given set of propositions to the solver.
+ * @param propositions the set of propositions
+ */
+ public void addPropositions(final Proposition... propositions) {
+ for (final Proposition proposition : propositions)
+ add(proposition);
+ }
+
/**
* Adds a proposition to the solver. The formulas of the proposition are first converted to CNF.
* @param proposition the proposition
@@ -181,7 +199,7 @@ void addClauseSet(final Formula formula, final Proposition proposition) {
this.addClause(formula, proposition);
break;
case AND:
- for (Formula op : formula)
+ for (final Formula op : formula)
this.addClause(op, proposition);
break;
default:
@@ -204,7 +222,7 @@ private void addClauseSetWithRelaxation(final Variable relaxationVar, final Form
this.addClauseWithRelaxation(relaxationVar, formula);
break;
case AND:
- for (Formula op : formula)
+ for (final Formula op : formula)
this.addClauseWithRelaxation(relaxationVar, op);
break;
default:
diff --git a/src/main/java/org/logicng/transformations/Anonymizer.java b/src/main/java/org/logicng/transformations/Anonymizer.java
new file mode 100644
index 00000000..7aa2bb97
--- /dev/null
+++ b/src/main/java/org/logicng/transformations/Anonymizer.java
@@ -0,0 +1,62 @@
+package org.logicng.transformations;
+
+import org.logicng.datastructures.Substitution;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaTransformation;
+import org.logicng.formulas.Variable;
+
+import static org.logicng.formulas.cache.TransformationCacheEntry.ANONYMIZATION;
+
+/**
+ * An anonymizer replaces all variables in a formula with new variables generated from a given prefix and a counter.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class Anonymizer implements FormulaTransformation {
+
+ private final Substitution substitution;
+ private final String prefix;
+ private int counter;
+
+ /**
+ * Constructs a new anonymizer with a given prefix for the newly introduced variables.
+ * @param prefix the prefix for the new variables
+ * @param startCounter where should the counter start
+ */
+ public Anonymizer(final String prefix, final int startCounter) {
+ this.prefix = prefix;
+ this.substitution = new Substitution();
+ this.counter = startCounter;
+ }
+
+ /**
+ * Constructs a new anonymizer with a given prefix for the newly introduced variables.
+ * @param prefix the prefix for the new variables
+ */
+ public Anonymizer(final String prefix) {
+ this(prefix, 0);
+ }
+
+ /**
+ * Constructs a new anonymizer with the standard variable prefix 'v'.
+ */
+ public Anonymizer() {
+ this("v");
+ }
+
+ @Override
+ public Formula apply(final Formula formula, final boolean cache) {
+ if (formula.variables().isEmpty())
+ return formula;
+ final Formula cached = formula.transformationCacheEntry(ANONYMIZATION);
+ if (cache && cached != null)
+ return cached;
+ for (final Variable variable : formula.variables())
+ if (this.substitution.getSubstitution(variable) == null)
+ this.substitution.addMapping(variable, formula.factory().variable(this.prefix + this.counter++));
+ final Formula transformed = formula.substitute(this.substitution);
+ if (cache)
+ formula.setTransformationCacheEntry(ANONYMIZATION, transformed);
+ return transformed;
+ }
+}
diff --git a/src/main/java/org/logicng/transformations/FormulaFactoryImporter.java b/src/main/java/org/logicng/transformations/FormulaFactoryImporter.java
index 9adfc452..4d5eb4d5 100644
--- a/src/main/java/org/logicng/transformations/FormulaFactoryImporter.java
+++ b/src/main/java/org/logicng/transformations/FormulaFactoryImporter.java
@@ -111,7 +111,7 @@ public Formula apply(final Formula formula, final boolean cache) {
* @return the applied operands of the given operator
*/
private LinkedHashSet gatherAppliedOperands(final NAryOperator operator) {
- final LinkedHashSet applied = new LinkedHashSet();
+ final LinkedHashSet applied = new LinkedHashSet<>();
for (final Formula operand : operator) {
applied.add(apply(operand, false));
}
diff --git a/src/main/java/org/logicng/transformations/cnf/BDDCNFTransformation.java b/src/main/java/org/logicng/transformations/cnf/BDDCNFTransformation.java
new file mode 100644
index 00000000..9bfe93d6
--- /dev/null
+++ b/src/main/java/org/logicng/transformations/cnf/BDDCNFTransformation.java
@@ -0,0 +1,103 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2018 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.transformations.cnf;
+
+import org.logicng.bdds.BDDFactory;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaTransformation;
+import org.logicng.predicates.CNFPredicate;
+import org.logicng.transformations.UnitPropagation;
+
+import static org.logicng.formulas.FType.LITERAL;
+import static org.logicng.formulas.cache.TransformationCacheEntry.BDD_CNF;
+
+/**
+ * Transformation of a formula in CNF by converting it to a BDD.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public final class BDDCNFTransformation implements FormulaTransformation {
+
+ private final CNFPredicate cnfPredicate = new CNFPredicate();
+ private final UnitPropagation up = new UnitPropagation();
+ private BDDFactory bddFactory;
+ private final boolean externalFactory;
+ private int numNodes;
+ private int cacheSize;
+
+
+ /**
+ * Constructs a new BDD-based CNF transformation with a given BDD factory
+ * @param factory the BDD factory
+ */
+ public BDDCNFTransformation(final BDDFactory factory) {
+ this.bddFactory = factory;
+ this.externalFactory = true;
+ }
+
+ /**
+ * Constructs a new BDD-based CNF transformation with a given number of nodes and cache size for the BDD factory.
+ * @param numNodes the number of nodes
+ * @param cacheSize the cache size
+ */
+ public BDDCNFTransformation(final int numNodes, final int cacheSize) {
+ this.numNodes = numNodes;
+ this.cacheSize = cacheSize;
+ this.externalFactory = false;
+ }
+
+ /**
+ * Constructs a new BDD-based CNF transformation and determines the node size and cache size on its own.
+ */
+ public BDDCNFTransformation() {
+ this(0, 0);
+ }
+
+ @Override
+ public Formula apply(final Formula formula, final boolean cache) {
+ if (formula.type().precedence() >= LITERAL.precedence())
+ return formula;
+ if (formula.holds(this.cnfPredicate))
+ return formula;
+ final Formula cached = formula.transformationCacheEntry(BDD_CNF);
+ if (cache && cached != null)
+ return cached;
+ if (!this.externalFactory) {
+ final int numVars = formula.variables().size();
+ final int nodes = this.numNodes == 0 ? numVars * 30 : this.numNodes;
+ final int cacheS = this.cacheSize == 0 ? numVars * 20 : this.cacheSize;
+ this.bddFactory = new BDDFactory(nodes, cacheS, formula.factory());
+ this.bddFactory.setNumberOfVars(numVars);
+ }
+ final Formula cnf = this.bddFactory.build(formula).cnf().transform(this.up);
+ if (cache)
+ formula.setTransformationCacheEntry(BDD_CNF, cnf);
+ return cnf;
+ }
+}
diff --git a/src/main/java/org/logicng/transformations/cnf/CNFConfig.java b/src/main/java/org/logicng/transformations/cnf/CNFConfig.java
index a6253d07..2062ea38 100644
--- a/src/main/java/org/logicng/transformations/cnf/CNFConfig.java
+++ b/src/main/java/org/logicng/transformations/cnf/CNFConfig.java
@@ -42,7 +42,7 @@ public final class CNFConfig extends Configuration {
* The algorithm for the CNF encoding.
*/
public enum Algorithm {
- FACTORIZATION, TSEITIN, PLAISTED_GREENBAUM, ADVANCED
+ FACTORIZATION, TSEITIN, PLAISTED_GREENBAUM, ADVANCED, BDD
}
final Algorithm algorithm;
@@ -119,7 +119,7 @@ public Builder fallbackAlgorithmForAdvancedEncoding(final Algorithm fallbackAlgo
* @param distributionBoundary the distribution boundary
* @return the builder
*/
- public Builder distributionBoundary(int distributionBoundary) {
+ public Builder distributionBoundary(final int distributionBoundary) {
this.distributionBoundary = distributionBoundary;
return this;
}
@@ -130,7 +130,7 @@ public Builder distributionBoundary(int distributionBoundary) {
* @param createdClauseBoundary the clause creation boundary
* @return the builder
*/
- public Builder createdClauseBoundary(int createdClauseBoundary) {
+ public Builder createdClauseBoundary(final int createdClauseBoundary) {
this.createdClauseBoundary = createdClauseBoundary;
return this;
}
@@ -141,7 +141,7 @@ public Builder createdClauseBoundary(int createdClauseBoundary) {
* @param atomBoundary the atom boundary
* @return the builder
*/
- public Builder atomBoundary(int atomBoundary) {
+ public Builder atomBoundary(final int atomBoundary) {
this.atomBoundary = atomBoundary;
return this;
}
diff --git a/src/main/java/org/logicng/transformations/cnf/CNFEncoder.java b/src/main/java/org/logicng/transformations/cnf/CNFEncoder.java
index d0c94e24..f8388b5c 100644
--- a/src/main/java/org/logicng/transformations/cnf/CNFEncoder.java
+++ b/src/main/java/org/logicng/transformations/cnf/CNFEncoder.java
@@ -51,6 +51,7 @@ public class CNFEncoder {
private CNFFactorization factorization;
private CNFFactorization advancedFactorization;
+ private BDDCNFTransformation bddCnfTransformation;
private TseitinTransformation tseitin;
private PlaistedGreenbaumTransformation plaistedGreenbaum;
private int currentAtomBoundary;
@@ -98,6 +99,10 @@ public Formula encode(final Formula formula) {
this.plaistedGreenbaum = new PlaistedGreenbaumTransformation(this.config().atomBoundary);
}
return formula.transform(this.plaistedGreenbaum);
+ case BDD:
+ if (this.bddCnfTransformation == null)
+ this.bddCnfTransformation = new BDDCNFTransformation();
+ return formula.transform(this.bddCnfTransformation);
case ADVANCED:
if (this.factorizationHandler == null) {
this.factorizationHandler = new AdvancedFactorizationHandler();
@@ -159,7 +164,7 @@ private Formula singleAdvancedEncoding(final Formula formula) {
public CNFConfig config() {
if (this.config != null)
return this.config;
- Configuration cnfConfig = this.f.configurationFor(ConfigurationType.CNF);
+ final Configuration cnfConfig = this.f.configurationFor(ConfigurationType.CNF);
return cnfConfig != null ? (CNFConfig) cnfConfig : this.defaultConfig;
}
@@ -178,7 +183,7 @@ private static class AdvancedFactorizationHandler implements FactorizationHandle
private int currentDistributions;
private int currentClauses;
- private void reset(int distributionBoundary, int createdClauseBoundary) {
+ private void reset(final int distributionBoundary, final int createdClauseBoundary) {
this.distributionBoundary = distributionBoundary;
this.createdClauseBoundary = createdClauseBoundary;
this.currentDistributions = 0;
@@ -187,12 +192,12 @@ private void reset(int distributionBoundary, int createdClauseBoundary) {
@Override
public boolean performedDistribution() {
- return distributionBoundary == -1 || ++currentDistributions <= distributionBoundary;
+ return this.distributionBoundary == -1 || ++this.currentDistributions <= this.distributionBoundary;
}
@Override
- public boolean createdClause(Formula clause) {
- return createdClauseBoundary == -1 || ++currentClauses <= createdClauseBoundary;
+ public boolean createdClause(final Formula clause) {
+ return this.createdClauseBoundary == -1 || ++this.currentClauses <= this.createdClauseBoundary;
}
}
}
diff --git a/src/main/java/org/logicng/transformations/qe/ExistentialQuantifierElimination.java b/src/main/java/org/logicng/transformations/qe/ExistentialQuantifierElimination.java
index d13fab60..5bb48dcd 100644
--- a/src/main/java/org/logicng/transformations/qe/ExistentialQuantifierElimination.java
+++ b/src/main/java/org/logicng/transformations/qe/ExistentialQuantifierElimination.java
@@ -63,14 +63,14 @@ public ExistentialQuantifierElimination(final Variable... variables) {
* @param variables the collection of variables
*/
public ExistentialQuantifierElimination(final Collection variables) {
- this.elimination = variables.toArray(new Variable[variables.size()]);
+ this.elimination = variables.toArray(new Variable[0]);
}
@Override
- public Formula apply(final Formula formula, boolean cache) {
+ public Formula apply(final Formula formula, final boolean cache) {
Formula result = formula;
final FormulaFactory f = formula.factory();
- for (final Variable var : elimination)
+ for (final Variable var : this.elimination)
result = f.or(result.restrict(new Assignment(var)), result.restrict(new Assignment(var.negate())));
return result;
}
diff --git a/src/main/java/org/logicng/transformations/qe/UniversalQuantifierElimination.java b/src/main/java/org/logicng/transformations/qe/UniversalQuantifierElimination.java
index 2462d2ec..0011a537 100644
--- a/src/main/java/org/logicng/transformations/qe/UniversalQuantifierElimination.java
+++ b/src/main/java/org/logicng/transformations/qe/UniversalQuantifierElimination.java
@@ -63,14 +63,14 @@ public UniversalQuantifierElimination(final Variable... variables) {
* @param variables the collection of variables
*/
public UniversalQuantifierElimination(final Collection variables) {
- this.elimination = variables.toArray(new Variable[variables.size()]);
+ this.elimination = variables.toArray(new Variable[0]);
}
@Override
- public Formula apply(final Formula formula, boolean cache) {
+ public Formula apply(final Formula formula, final boolean cache) {
Formula result = formula;
final FormulaFactory f = formula.factory();
- for (final Variable var : elimination)
+ for (final Variable var : this.elimination)
result = f.and(result.restrict(new Assignment(var)), result.restrict(new Assignment(var.negate())));
return result;
}
diff --git a/src/main/java/org/logicng/transformations/qmc/QuineMcCluskeyAlgorithm.java b/src/main/java/org/logicng/transformations/qmc/QuineMcCluskeyAlgorithm.java
new file mode 100644
index 00000000..fc1d0581
--- /dev/null
+++ b/src/main/java/org/logicng/transformations/qmc/QuineMcCluskeyAlgorithm.java
@@ -0,0 +1,356 @@
+///////////////////////////////////////////////////////////////////////////
+// __ _ _ ________ //
+// / / ____ ____ _(_)____/ | / / ____/ //
+// / / / __ \/ __ `/ / ___/ |/ / / __ //
+// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
+// /_____/\____/\__, /_/\___/_/ |_/\____/ //
+// /____/ //
+// //
+// The Next Generation Logic Library //
+// //
+///////////////////////////////////////////////////////////////////////////
+// //
+// Copyright 2015-2018 Christoph Zengler //
+// //
+// Licensed under the Apache License, Version 2.0 (the "License"); //
+// you may not use this file except in compliance with the License. //
+// You may obtain a copy of the License at //
+// //
+// http://www.apache.org/licenses/LICENSE-2.0 //
+// //
+// Unless required by applicable law or agreed to in writing, software //
+// distributed under the License is distributed on an "AS IS" BASIS, //
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
+// implied. See the License for the specific language governing //
+// permissions and limitations under the License. //
+// //
+///////////////////////////////////////////////////////////////////////////
+package org.logicng.transformations.qmc;
+
+import org.logicng.cardinalityconstraints.CCIncrementalData;
+import org.logicng.datastructures.Assignment;
+import org.logicng.datastructures.Tristate;
+import org.logicng.formulas.CType;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaFactory;
+import org.logicng.formulas.Literal;
+import org.logicng.formulas.Variable;
+import org.logicng.solvers.MiniSat;
+import org.logicng.solvers.SATSolver;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.LinkedHashMap;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.SortedMap;
+import java.util.TreeMap;
+
+/**
+ * An implementation of the Quine-McCluskey algorithm for minimizing canonical DNFs. This implementation is fairly
+ * efficient but keep in mind that Quine-McCluskey can be a very expensive procedure for large canonical DNFs. So we
+ * would not recommend using this implementation for super large DNFs.
+ * @version 1.4.0
+ * @since 1.4.0
+ */
+public class QuineMcCluskeyAlgorithm {
+
+ /**
+ * Computes a minimized DNF for a given formula projected to a given set of variables. First a projected canonical
+ * DNF of the formula is computed for the given variables. Then for this canonical DNF the Quine-McCluskey algorithm
+ * is computed.
+ * @param formula the formula
+ * @param relevantVariables the relevant formulas for the projected canonical DNF
+ * @return the minimized DNF due to Quine-McCluskey
+ */
+ public static Formula compute(final Formula formula, final Collection relevantVariables) {
+ final FormulaFactory f = formula.factory();
+ final SATSolver solver = MiniSat.miniSat(f);
+ solver.add(formula);
+ final List
@@ -19,7 +19,7 @@ LogicNG is released in the Maven Central Repository. To include it just add