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.

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

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.

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.

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.

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 the truth tables for the given functions as a html table.

PropLogicTool is the function to be called from the web page

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.