The Compile! Project
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.
News
- At the 2nd International Competition on Model Counting (MC'21), d4 2.0 ranked 2nd on the "Weighted Model Counting" track, 2nd on the "Projected Model Counting" track, 3rd on the "Model Counting" track, and 3rd on the "Model Counting (harder/low confidence)"
- d4, in model counting mode, won (1st ex aequo) the weighted model counting track of the First International Competition on Model Counting (MC'20), see https://mccompetition.org/
- KnOwledge COmpilatiOn Network (KOCOON) workshop, Arras, December 16 to December 19, 2019
- IJCAI-18 Tutorial on Recent Advances in Knowledge Compilation, 15th July 2018
- Research school: An overview of Knowledge Compilation, ENS Lyon, 4th-8th December 2017
- Dagstuhl seminar: "Recent Trends in Knowledge Compilation", 17th-22nd September 2017
- AAAI'16 Workshop on Beyond NP
- BeyondNP.org community website
- Symposium on New Frontiers in Knowledge Compilation, Vienna, June 4-6, 2015
Available ressources
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 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 br2cnf compiler
The br2cnf compiler is a program for compiling a given CNF belief revision instance into a query-equivalent CNF formula. Several topic-decomposable distance-based belief revision operators have been implemented, namely those based on the drastic distance or Hamming distance between interpretations, and using sum, leximin or leximax as aggregation function. [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 d4 compiler
d4 is a compiler associating with an input CNF formula an equivalent representation from the language Decision-DNNF. Decision-DNNF is the language consisting of the Boolean circuits with a single output (its root), where each input is a literal or a Boolean constant, and each internal gate is either a decomposable ∧ gate of the form N = ∧(N1, . . . , Nk) (”decomposable” means here that for each i, j ∈ {1, . . . , k} with i ≠ j the subcircuits of N rooted at Ni and Nj do not share any common variable) or decision gates of the form N = ite(x, N1, N2). x is the decision variable at gate N, it does not occur in the subcircuits N1, N2, and ite is a ternary connective whose semantics is given by ite(X, Y, Z) = (¬X ∧ Y ) ∨ (X ∧ Z) (”ite” means ”if ... then ... else ...: if X then Z else Y ). [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]
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 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 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]