Compilation of a CNF belief revision instance into CNF formula
cnf2eadt is a compiler associating with an input CNF formula an equivalent representation from the language EADT of (extended) affine decision trees. An extended affine decision tree simply is a tree with affine decision nodes and some specific decomposable conjunction or disjunction nodes. Unlike standard decision trees, the decision nodes of an EADT formula are not labeled by variables but by affine clauses. Interestingly, the models of an EADT representation can be counted efficiently.
Any category Compiler
2013 Frédéric Koriche, Jean-Marie Lagniez, Pierre Marquis, Samuel Thomas, Knowledge Compilation for Model Counting: Affine Decision Trees in 23rd International Joint Conference on Artificial Intelligence (IJCAI'13), pp. 947-953, 2013.