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

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