Le CRIL en bref
Le Centre de Recherche en Informatique de Lens (CRIL UMR 8188) est un laboratoire de l’Université d’Artois et du CNRS qui regroupe plus de cinquante membres : chercheurs, enseignants-chercheurs, doctorants et personnels administratifs et techniques.
Recherches en intelligence artificielle et applications
Actualités (RSS)
Séminaire An Improved CNF Encoding Scheme for Probabilistic Inference (ECAI 2016)
Jean-Marie Lagniez (CRIL, Université d’Artois - CNRS)
We present and evaluate a new CNF encoding scheme for reducing probabilistic inference from a graphical model to weighted model counting. This new encoding scheme elaborates on the CNF encoding scheme ENC4 introduced by Chavira and Darwiche, and improves it by taking advantage of log encodings of the elementary variable/value assignments and of the implicit encoding of the most frequent probability value per conditional probability table. From the theory side, we show that our encoding scheme is faithful, and that for each input network, the CNF formula it leads to contains less variables and less clauses than the CNF formula obtained using ENC4. From the practical side, we show that the C2D compiler empowered by our encoding scheme performs in many cases significantly better than when ENC4 is used, or when the state-of-the-art ACE compiler is considered instead.
Séminaire TBA
Anastasia Paparrizou (CRIL, CNRS - Université d’Artois)
TBA
Séminaire TBA
Bart Gruyaert (Société Altifort)
TBA
Séminaire Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation (CP 2017)
Takehide Soh (Kobe University, Japan)
This talk about SAT encoding consists of two parts.
The first part briefly explains recent our work around SAT
encoding—a SAT-based CP system “scarab” and a hybrid encoding
integrating the order and log encodings.
In the second part, as an application of the order encoding, we detail
a propositional logic based approach to solve MultiObjective Discrete
Optimization Problems (MODOPs).
In this approach, there exists a one-to-one correspondence between
a Pareto front point of MODOP and a P-minimal model of
the CNF formula obtained from MODOP.
This correspondence is achieved by adopting the order encoding
as encoding for multiobjective functions.
Finding the Pareto front is done by enumerating all P-minimal models.
The beauty of the approach is that each Pareto front point is
blocked by a single clause that contains at most one literal
for each objective function.
We evaluate the effectiveness of this approach by empirically
contrasting it to a state-of-the-art MODOP solving technique.
Séminaire A lower bound on CNF encodings of the at-most-one constraint
Petr Kučera (Charles University, Czech Republic)
Constraint “at most one” is a basic cardinality constraint which requires that at most one of its n boolean inputs is set to 1. This constraint is widely used when translating a problem into a conjunctive normal form (CNF) and we investigate its CNF encodings suitable for this purpose. An encoding differs from a CNF representation of a function in that it can use auxiliary variables. We are especially interested in propagation complete encodings which have the property that unit propagation is strong enough to enforce consistency on input variables. We show a lower bound on the number of clauses in any propagation complete encoding of the “at most one” constraint. The lower bound almost matches the size of the best known encodings. We also study an important case of 2-CNF encodings where we show a slightly better lower bound. The lower bound holds also for a related “exactly one” constraint.