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.
- Extract of the project page.
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.
- 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 uniﬁed framework for certiﬁcate and compilation for QBF. We provide a search-based algorithm to compute a certiﬁcate for the validity of a QBF and a search-based algorithm to compile a valid QBF in our uniﬁed 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 Quantiﬁed Boolean Formulae to Answer Set Programming. The computation of a solution of a Quantiﬁed Boolean Formula is then equivalent to the computation of a stable model for a normal logic program. The case of unquantiﬁed Boolean formulae is also considered since it is equivalent to the case of Quantiﬁed Boolean Formulae with only existential quantiﬁers.
- From (Quantified) Boolean Formulas to Answer Set Programming. I. Stéphan et B. Da Mota et P. Nicolas. Journal of logic and computation. Volume 19. issue 4. 2009.
- dedicated website.
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:
- P. Chatalic, L. Simon: Multiresolution for SAT Checking. International Journal on Artificial Intelligence Tools.
- P. Chatalic, L. Simon: ZRES: The Old Davis-Putman Procedure Meets ZBDD. CADE 2000.
- P. Chatalic, L. Simon: Multi-resolution on compressed sets of clauses. ICTAI 2000.