Research activities

2011-2012 : Neuroimaging Genetics in the A-Brain project.

Joint acquisition of neuroimaging and genetic data on large cohorts of subjects is a new approach used to assess and understand the variability that exists between individuals, and that has remained poorly understood so far. As both neuroimaging and genetic-domain observations represent a huge amount of variables (of the order of 106), performing statistically rigorous analyses on such amounts of data represents a computational challenge that cannot be addressed with conventional computational techniques. On one hand, sophisticated regression techniques need to be used in order to perform sensitive analysis on these large datasets; on the other hand, the cost entailed by parameter optimization and statistical validation procedures (e.g. permutation tests).

In this project, researchers of the Parietal and KerData INRIA teams will jointly address address this computational problem using cloud computing techniques on Microsoft Azure cloud computing environment. The two teams bring their complementary expertise: KERDATA (Rennes) in the area of scalable cloud data management and PARIETAL (Saclay) in the field of neuroimaging and genetics data analysis.

The postdoc was the opportunity to study statistical learning in a very rich and new domain of neuroscience. The main goal was to deliver scalable and fast procedures to analyse huge dataset in a reasonable amount of time. About six month after the begining of the project, we present a fast (more than 2000 times compared to SOTA) and hilghly scalable procedure that can run both on clouds and HPC clusters.
MapReduce framework

2007-2011 : Quantified Boolean Formulae.

The quantified Boolean formula (QBF) validity problem is a generalization of the Boolean formulae satisfiability problem. While the complexity of Boolean satisfiability problem is NP-complete, it is PSPACE-complete for the QBF validity problem.

The thesis was the opportunity to study in detail the quantified Boolean formulas without syntactic restrictions. Most of the recent and efficient decision procedures for QBF have formulae in negative normal form (NNF) as input or even more restrictive format such as formulae in conjunctive normal form (CNF). But rarely, problems are expressed in such a form which destroyed completely their original structures. I focus on three problematics:
  • Formal Processings : Our contribution is a set of equivalences and algorithms that can process a particular pattern, the intermediate results. This pattern provides an effective alternative in space and in time resolution, at the naive suppression of bi-implications and exclusive-or during the conversion in prenex form. It also offers new opportunities of transformations in different fragments of the QBF language (like DNF or mixed CNF/DNF).
  • Certification and compilation : We propose a unified framework for certificate and compilation for QBF. We provide a search-based algorithm to compute a certificate for the validity of a QBF and a search-based algorithm to compile a valid QBF in our unified framework.
  • Parallel computations : Our goal is to use the power of parallel computing architectures to deal with QBF without syntactic restriction. So we are developing an innovative architecture for parallelizing the QBF validity problem. Its originality lies in its architecture of « syntactic parallelization » versus parallelization based on the semantics of quantifiers.
  • Check my publications page.

2006-2007 : From (Quantified) Boolean Formulae to Answer Set Programming.

We propose a translation from Quantified Boolean Formulae to Answer Set Programming. The computation of a solution of a Quantified Boolean Formula is then equivalent to the computation of a stable model for a normal logic program. The case of unquantified Boolean formulae is also considered since it is equivalent to the case of Quantified Boolean Formulae with only existential quantifiers.

2005-2006 : Zero-suppressed Binary Decision Diagram (ZBDD).

During my first training period (Master degree) in the LERIA, I study the zero-suppressed binary decision diagram. This structure is very useful to represent boolean functions in a compressed manner. The goal of my work is to build first a Prolog, then a C++ library to handle ZBDD with the new operators describe in:
  1. P. Chatalic, L. Simon: Multiresolution for SAT Checking. International Journal on Artificial Intelligence Tools.
  2. P. Chatalic, L. Simon: ZRES: The Old Davis-Putman Procedure Meets ZBDD. CADE 2000.
  3. P. Chatalic, L. Simon: Multi-resolution on compressed sets of clauses. ICTAI 2000.