Compilation of a CNF belief revision instance into CNF formula

cnf2eadt est un compilateur associant à une formule CNF d’entrée une représentation équivalente du langage EADT d’arbres de décision affines. Un arbre de décision affine étendu est simplement un arbre avec des nœuds de décision affine et certains nœuds de conjonction ou de disjonction décomposables spécifiques. Contrairement aux arbres de décision standard, les nœuds de décision d’une formule EADT ne sont pas étiquetés par des variables mais par des clauses affines. Il est intéressant de noter que les modèles d’une représentation EADT peuvent être comptés efficacement.