BE

B+E est un préprocesseur qui associe à une formule CNF d'entrée une formule CNF de sortie qui admet le même nombre de modèles.

bn

bn2cnf est un traducteur associant à un modèle graphique d'entrée (un réseau bayésien ou un réseau de Markov) une sortie qui consiste en une formule CNF et une carte de poids.

Co

Le compilateur br2cnf est un programme permettant de compiler une instance de révision de croyance CNF donnée en une formule CNF équivalente

Co

cnf2eadt est un compilateur associant à une formule CNF d'entrée une représentation équivalente du langage EADT d'arbres de décision affines.

Co

bm2cnf est un compilateur permettant de transformer une instance de fusion CNF donnée en une formule CNF équivalente.

Co

cn2mddg est un compilateur associant à un réseau de contraintes à domaine fini représenté dans le format XCSP 2.1 une représentation équivalente du langage MDDG de graphes de décision décomposables multivalués.

Software

Un outil d'agrégation de croyances.

dD

d-DNNF-reasoner est un outil de raisonnement sur les représentations d-DNNF.

Software

d4 est un compilateur de CNF vers d-DNNF pour le comptage de modèles.

Ge

tt2bm est un programme qui peut être utilisé à la fois pour générer des instances d'horaires et pour les transformer en instances de fusion basées sur la distance.

pd

pddl2cnf est un traducteur associant à une instance de planification classique codée en PDDL (Planning Domain Definition Language) et à un horizon donné une sortie qui consiste en une formule CNF.

Pr

pmc est un préprocesseur associant à une formule CNF d'entrée une formule CNF de sortie qui est soit logiquement équivalente à l'entrée, soit n'a que le même nombre de modèles que l'entrée

Tr

cn2cnf est un traducteur associant à un réseau de contraintes d'entrée (en XCSP3) une formule CNF.