This cgi-function provides various BDD algorithms.

This cgi-function is used to first construct the BDD of a formula with a specified variable ordering and the converts it to the BDD of another specified variable ordering by a sequence of swap operations. Afterwards, it applies sifting to optimize the second ordering.

print a propositional formula in Latex

This function derives a formula in conjunctive normal form from a BDD. The CNF is given as a set of sets of literals with an obvious meaning.

Compute canonical CNF by truth table, where the maxterms are ordered as given by atomL.

This function derives a formula in disjunctive normal form from a BDD. The DNF is given as a set of sets of literals with an obvious meaning.

Compute canonical DNF by truth table, where the minterms are ordered as given by atomL.

Compute Reed-Muller normal form directly from a formula, where the RMNF is encoded as sets of sets of variables where false is {}, true is {{}}, x is {{x}}, and !x is {{},{x}}. We define a n-ary XOR as XOR{} := false; XOR{m} := m; and otherwise the xor of the elements. Similarly, we have AND{} := true, AND{x} := x, etc.

This function derives a formula in Shannon normal form from a BDD. Of course, the formula can have an exponential size also for a small BDD.

Enumerate all assignments for the given list of atoms; an assignment is thereby a map that maps an atom of the given boolean expression to a boolean value.

ComputeFDDs computes the functional decision diagrams of Reed-Muller normal forms as computed by CanonicalRMNF following the variable order given by argument atomL (as always for decision diagrams, the leftmost atom in atomL is closest to the leaf nodes). The FDDs are stored in a map that maps a node address i to a triple (x,i1,i0) where x is the variable of the node, and i1,i0 are the addresses of the positive and negative subFDDs. The result is a pair (iL,m) where iL is the list of addresses of the FDDs and m is the map described before.

ComputeZDDs computes for a given list of BDDs the corresponding ZDDs where the variable ordering atomL is followed (should be the one used by the BDDs, i.e., as always for decision diagrams, the leftmost atom in atomL is closest to the leaf nodes). Analogously to the FDDs, the ZDDs are stored in a map that maps a node address i to a triple (x,i1,i0) where x is the variable of the node, and i1,i0 are the addresses of the positive and negative subZDDs. The result is a pair (iL,m) where iL is the list of addresses of the ZDDs and m is the map described before.

Dual-rail encoding of a formula: If a variable x belongs to inputSet, it will be encoded as (x,!x) instead of (x+,x-).

Evaluate a formula with respect to a given assignment of the atoms. It is expected that the given assignment is complete, i.e., that every atom of the given boolean expression is mapped to either true or false.

Write a FDD as generated by function ComputeFDD to a DotFile.

Computes a KV diagram for a given list of atoms. The KV diagram is given as two arrays (col,row) where col and row denote the column and row vectors, respectively, i.e., col[i] and row[j] denote the assignments to the variables in entry (i,j) of the KV diagram, and their union is therefore the assignment to be evaluated there.

Generate linear clause forms for a given formula phi. The result is a pair (v,l) where v is the variable that finally abbreviates phi, and l is a list of pairs ((v,t),cl) where (v,t) represents an abbreviation v=t and cl is its corresponding clause set.

This cgi-function is used for logic minimization using KV diagrams, the Quine/McCluskey table, or symbolic logic minimization.

This function explains the recursive calls of a BDD function like Apply. The function expects a call to such a BDD function as explained with type BddCallExpr. In case of Compose, the optional argument vComp must contain the BDD index of the variable that should be replaced in the BDD. The result is a table that maps a BddCallExpr to a list of such that explains the computations.

Construct a CNF formula of a set of sets representation (clause set), where the literals in the cubes are ordered as given by atomL.

Construct a DNF formula of a set of sets representation, where the literals in the maxterms are ordered as given by atomL.

Partial evaluation of a formula wrt. a partial variable assignment: Since the given assignment rho may not map every atom of the boolean expression to a boolean value, the result is just another boolean formula where the mapped atoms are replaced by constants and where simplifications were applied to propagate these constants.

Print a KV diagram as constructed by KarnaughVeitch as a html table.

Print the truth tables for the given functions as a html table.

PropLogicTool is the function to be called from the web page

Convert a cube (idx,(pos,neg)) as used in the Quine table to a string. The index set idx is written as a set of integers {i1,...,iN} and the cube (pos,neg) itself is written as a bitvector with * whenever there is a don't care.

Convert a cube (idx,(pos,neg)) as used in the Quine table to a boolean expression where the literals occur as specified by the variable order atomL.

The following function computes minimal DNFs for a given formula phi with a care set care, where the ordering of atoms atomL is respected. The function applies first the Quine method QuineTable to compute all cubes (implicants) of care->phi, and extracts then the prime cubes with function QuineTablePrimeImplicants where each prime cube is associated with a new boolean variable PI[i]. After this, it generates a formula coverPhi in CNF over the variables PI[i] such that coverPhi has a disjunct for each model of care&phi and that contains all PI[i] that cover that model. The formula coverPhi is then converted to DNF (in sets of sets representation) so that minimal DNFs for phi wrt. care can be derived. The function finally returns a tuple (qt,primeCubes,coverPhi,dnfCover,minDNFs) with:

• qt is the Quine table as generated by function QuineTable.
• primeCubes is a list of pairs (PI[i],pc[i]) where pi is a variable associated with prime cube pc[i].
• coverPhi is the cover formula using variables PI[i] in CNF.
• dnfCover is the set of set representation of coverPhi.
• minDNFs is the list of minimal DNFs of phi wrt. care set care.

Compute the Quine table: The function expects a formula phi and its variable order order atomL. It computes the Quine table that contains all implicants of phi as a list of list of lists [I0;...;In] where each Ik is the list of list of implicants of order k, i.e., where k variables are don't cares, hence, I0 are all full models of phi. Each Ik=[Lk0;...;Lkj] is partitioned into levels Lki according to the number of atoms made true (zero in Lk0 up to j in Lkj]. Each Lki is finally a list of cubes, where a cube (idx,(pos,neg)) is given by the sets of atoms (pos,neg) made true and false by the cube, respectively. The index idx is a set of integers that uniquely represents the cube; it is the union of binary numbers that an be derived when all don't cares are replaced by either true and false (following the order atomL).

Print a Quine table as a html table

Get the prime implicants of a formula phi from its Quine table: We check whether the index set of a cube is contained in one of the other cube's index set of the next level. If so, it is not a prime implicant, since it has been used to construct that higher cube. The function returns a list of tuples (piv,(idx,(pos,neg))) where piv is a boolean variable generated for the prime implicant (idx,(pos,neg)).

This function converts a Reed-Muller form given in set representation to a string where xor is printed as ⊕.

Construct a proof tree for the validity of a given formula; the function expects an index i for the root node and the goal of the root node.

write proof tree to a dot file

Solves a propositional logic formula phi by means of the BDD package. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values.

Solves a propositional logic formula phi by means of the SAT solver. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values.

Write a ZDD as generated by function ComputeZDD to a DotFile.

Extract a Reed-Muller form set representation from a graph (FDD) given in a unique table as returned by functions ComputeFDDs and ComputeZDDs.

Extract a Shannon normal representation from a decision diagram (read as ZDD) given in a unique table as returned by functions ComputeFDDs and ComputeZDDs. The ordering given in atomL should be consistent with the one used in the ZDDs, i.e., leftmost atom in atomL should be closest to the leaf nodes.

This function prints a formula in Shannon normal form such that the cofactors are printed in different lines with suitable indentation.