d4

d4 is a compiler associating with an input CNF formula an equivalent representation from the language Decision-DNNF. Decision-DNNF is the language consisting of the Boolean circuits with a single output (its root), where each input is a literal or a Boolean constant, and each internal gate is either a decomposable ∧ gate of the form N = ∧(N1, . . . , Nk) (”decomposable” means here that for each i, j ∈ {1, . . . , k} with i ≠ j the subcircuits of N rooted at Ni and Nj do not share any common variable) or decision gates of the form N = ite(x, N1, N2). x is the decision variable at gate N, it does not occur in the subcircuits N1, N2, and ite is a ternary connective whose semantics is given by ite(X, Y, Z) = (¬X ∧ Y ) ∨ (X ∧ Z) (”ite” means ”if … then … else …: if X then Z else Y ).

LGPL    Any category    Perennial software    Recent software    Compiler