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   

  • 2020 Constraints Jean-Marie Lagniez, Emmanuel Lonca, Pierre Marquis, Definability for model counting in Artificial Intelligence, vol. 281, pp. 103229, 2020.
    2017 Jean-Marie Lagniez, Pierre Marquis, On Preprocessing Techniques and Their Impact on Propositional Model Counting in Journal of Automated Reasoning (JAR), vol. 58, n° 4, pp. 413-481, 2017.
    2023 Constraints Jean-Marie Lagniez, Pierre Marquis, Boosting Definability Bipartition Computation Using SAT Witnesses in The 18th European Conference on Logics in Artificial Intelligence (JELIA'23), Springer Nature Switzerland, vol. 14281, pp. 697-711, 2023.
    2017 Jean-Marie Lagniez, Pierre Marquis, An Improved Decision-DNNF Compiler in 26th International Joint Conference on Artificial Intelligence (IJCAI'17), pp. 667-673, 2017.
    2021 Jean-Marie Lagniez, Pierre Marquis, About Caching in D4 2.0 in Workshop on Counting and Sampling 2021, 2021.