International Journal: Journal on Satisfiability, Boolean Modeling and Computation (JSAT), Constraints, International Journal of Advanced Information Technology (IJAIT), ICGA Journal
International Conferences: SAT 2009, SAT 2010, SAT 2011, SAT 2013, CP 2011, CP 2012, CP 2013, AAAI 2011, CPAIOR 2012, AAAI-17
Research Projects
ANR SATAS -- SAT As a Service (2015-2019). The SATAS project is an ambitious project, which aims to advance the state of the art in massively parallel SAT solving with a particular eye to the applications driving progress in the field. The final goal of the project is to be able to provide a “pay as you go” interface to SAT solving services, with a particular focus on its power consumption. This project will extend the reach of SAT solving technologies, daily used in many critical and industrial applications, to new application areas, which were previously considered too hard, and lower the cost of deploying massively parallel SAT solvers on the cloud. Many critical applications are daily relying on the recent and constant progress made around SAT and incremental SAT Solving.
ANR BR4CP -- Business Recommendation for Configurable Products (2011–2014). E-commerce, like classical commerce, adresses the problem of conciliating the different needs of customers, and the choices or even the purposes of the supply. The ambition of the project is to provide models and algorithms allowing the management of the customer's preferences and directing her choices (as recommender systems
do), and are able to deal with combinatorial domains in an interactive way (as configuration systems do). The control of the system response time is a crucial point because e-configuration is an on-line activity. Scientifically speaking, the originality of the project relies on two main ideas: on the one hand, the use of learning techniques for the definition of combinatorial models of recommendation; on the other hand, the use of compilation approaches for pre-processing the catalogue or the customer's indicators, and the recommendation models
The "PAJERO" project (2011-2015) includes 3 labs (PRISM (Versailles), I3S (NICE) et CRIL (Lens)) together with 3 industrial partners (HSW, ICAPS and EquiTime). The purpose consists in developping a framework that is able to handle complex management of multiple ressources (human ressources, planification,...).
2006-2007 : PESSOA MUSICAa French-Portuguese project about explanation of inconsistency in propositional logic
Softwares
PeneLoPe is a SAT solver based on the portfolio schema. Maintained by Benoit Hoessen, PeneLoPe is a fruit from the joint work between Gilles Audemard and Said Jabbour. Our solver, based on Minisat, has its own set of strategies, regarding clause exchange.
Particularly, the novel technique of nogood management called PSM is implemented. It enables to "freeze" learning clauses, namely remove them from the solver's data structures, without actually erase them from the RAM. This leads to a precise nogood management between the different workers. PeneLoPe obtains very good empirical results, since she (she's a she ;) came 2nd (among 19 solvers) in the "Parallel Track" of SAT Challenge 2012, and 3rd in the "Core Solvers, Parallel" track of the SAT Competition 2013. Full details (binaries, papers, results, etc.) here.
(A)OMUS is a "Local-search oriented MUS extractor", formally presented here : [pdf]. A comparison between techniques enabling to approximate one MUS, and another one where the focus is on extracting exactly one MUS are also available. The source code is available here.
HYCAM is an improved version of an algorithm of Mark Liffiton and Karem Sakallah (based on Minisat) that aims to compute all MUS contained in a CNF. It is actually an hybridization with a local search that enables to gain an order of magnitude in many cases, without being slower in others cases. The main idea is presented here : [pdf], and the binaries of the procedure are available here.
MUSTER is a MUST (Minimally Unsatisfiable Set of Tuples) extractor, within an unsatisfiable CSP, presented here: [pdf]
ReVivAl is a new preprocessing technique developped by Cédric Piette, Youssef Hamadi and Lakhdar Saïs.
The main idea is to perform particular forms of resolution (through Unit Propagation) for efficiently producing sub-clauses. It can also use different schemes of learning to add relevant clauses. The vivification algorithm ReViVal is based on is designed to be fully integrated within a SAT solver, taking advantage of most recent techniques and data structures implemented for SAT.
