d4
d4 est un compilateur associant à une formule CNF d’entrée une représentation équivalente en langage Decision-DNNF. Decision-DNNF est un langage constitué de circuits booléens avec une seule sortie (sa racine), et où chaque entrée est un littéral ou une constante booléenne, et chaque porte interne est soit une porte décomposable avec les portes ∧ de la forme N = ∧(N1, . . . , Nk) (”décomposable” signifie ici que pour chaque i, j ∈ {1, . . . , k} avec i ≠ j les sous-circuits de N ayant pour racine Ni et Nj ne partagent pas de variable commune) ou de portes de décisions de la forme N = ite(x, N1, N2). x est la variable de décision à la porte N, Il ne se produit pas dans les sous-circuits N1, N2, et ite est une connective ternaire dont la sémantique est donnée par ite(X, Y, Z) = (¬X ∧ Y ) ∨ (X ∧ Z) (”ite” signifie ”if … then … else …: if X then Z else Y ).