Translators, preprocessors, compilers, and reasoners
The purpose of the Compile! project is to make available on the Web some ressources, especially pieces of software developed at CRIL, which are somehow relevant to knowledge compilation purposes. Those pieces of software consist mainly of translators of various kinds, which can be used to improve (from a computational point of view) the solving of a number of problems from different AI fields.
Translators are just programs implementing mappings from representation languages to representation languages. Typically, some expected properties must be satisfied by the corresponding translations (e.g., the ‘’solutions’’ or their number must be preserved).
Preprocessors are translators from representation languages to themselves. Basically, preprocessing a given representation aims at ‘’simplifying’’ it in a certain sense, so that some targeted processes become computationally easier (but can be still demanding) from the preprocessed representations.
Compilers are translators as well. Compiling a representation consists in turning it into another representation (a compiled form) from which some targeted processes are much more easier (and in some cases, tractable). Compiling a representation proves useful when the effort spent during the off-line compilation phase is balanced over the solving of sufficiently many instances sharing this representation.
Reasoners are programs for exploiting the generated compiled forms.
The bn2cnf translator
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. The weight of any piece of evidence for the input model can be computed as the weighted model count of the corresponding output. Several encoding schemes can be considered depending on the options used. [more]
The cn2cnf translator
cn2cnf is a translator associating with an input constraint network (CN) in XCSP3 format a CNF formula. The whole set of constraints of XCSP3-core is handled by the translator, except optimization functions. All the constraints are translated into intensional constraints, which are encoded using a Tseitin-like technique. The solutions of the input network are in one-to-one correspondence with the models of the output formula. [more]
The tt2bm translator
tt2bm is a translator which can be used both to generate time-tabling instances, and to turn them into distance-based merging instances. [more]
The pddl2cnf translator
pddl2cnf is a translator associating with a classical planning instance encoded in PDDL (Planning Domain Definition Language) and a given horizon an output which consists of a CNF formula. The valid plans of the input correspond to the models of the output, once projected onto the action variables. [more]
The pmc preprocessor
pmc is a preprocessor associating with an input CNF formula an output CNF formula which is either logically equivalent to the input or has only the same number of models as the input (depending on the elementary preprocessings which are used). Such preprocessings include occurrence reduction, vivification, backbone identification, as well as equivalence, AND and XOR gate identification and replacement. [more]
The B+E preprocessor
B+E is a preprocessor that associates with an input CNF formula an output CNF formula which admits the same number of models. B+E tracks definability relations between variables (aka gates) and use them to reduce the instance by eliminating variables which have been identified as outputs of some gates. [more]
The cnf2eadt compiler
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 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. [more]
The bm2cnf compiler
bm2cnf is a compiler for turning a given CNF merging instance into a query-equivalent CNF formula. Several distance-based merging operators have been implemented, namely those based on the (possibly weighted) drastic distance or Hamming distance between interpretations, and using sum, leximin or leximax as aggregation function.[more]
The cn2mddg compiler
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. MDDG is precisely the extension to non-Boolean domains of the language Decision-DNNF: it is based on decomposable AND-nodes and (multivalued) decision nodes. Similarly to Decision-DNNF, the MDDG language offers a number of tractable queries, including (possibly weighted) solution finding and counting, solution enumeration (solutions can be enumerated with polynomial delay), and optimization w.r.t. a linear objective function. [more]
The d-DNNF reasoner
d-DNNF-reasoner is a tool for reasoning on d-DNNF representations. This tool implements some useful queries and transformations on compiled forms, including conditioning, satisfiability checking and model counting (CD, CO and CT operations as defined in the knowledge compilation map).[more]