BE

B+E is a preprocessor that associates with an input CNF formula an output CNF formula which admits the same number of models.

bn

bn2cnf is a translator associating with an input graphical model (a Bayesian network or a Markov network) an output which consists of a CNF formula and a weight map.

Co

br2cnf compiler is a program for compiling a given CNF belief revision instance into a query-equivalent CNF formula.

Co

cnf2eadt is a compiler associating with an input CNF formula an equivalent representation from the language EADT of (extended) affine decision trees.

Co

bm2cnf is a compiler for turning a given CNF merging instance into a query-equivalent CNF formula.

Co

cn2mddg is a compiler associating with a finite-domain constraint network represented in the XCSP 2.1 format an equivalent representation from the language MDDG of multivalued decomposable decision graphs.

dD

d-DNNF-reasoner is a tool for reasoning on d-DNNF representations.

Software

d4 is a compiler associating with an input CNF formula an equivalent representation from the language Decision-DNNF.

Ge

tt2bm is a program which can be used both to generate time-tabling instances, and to turn them into distance-based merging instances.

pd

pddl2cnf is a translator associating with a classical planning instance encoded in PDDL and a given horizon an output which consists of a CNF formula.

Pr

pmc is a preprocessor associating with an input CNF formula an output CNF formula which is either logically quivalent to the input or has only the same number of models as the input.

Tr

cn2cnf is a translator associating with an input constraint network (respecting the format XCSP3) a CNF formula.