## 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

### Available ressources

#### 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]