Sat4j, a free reasoning engine in propositional logic
- Daniel Le Berre
- HDR Defended on :
- Dec 3, 2010 • Salle des thèses, Faculté des Sciences Jean Perrin, Lens.
Our research work is situated in the framework of propositional logic. We are interested in the modeling of problems in this formalism and in their practical resolution. We present as a guideline of the document, the problem of managing dependencies between software. We show how various aspects of this problem can be modeled as pseudo-Boolean or MaxSat optimization problems, and also indicate how qualitative choice logic can be used as a framework for representing complex preferences that must be taken into account when managing dependencies. We then present in detail the functionalities of the free library Sat4j, which allows to solve various decision and optimization problems in propositional logic. Its performances are evaluated against the state of the art in each domain (SAT, pseudo-Boolean, MaxSat). Finally, we present the motivations and the functioning of the various editions of the international SAT prover competition that we have organized.
- Armin Biere, Professor at Johannes Kepler University
- Roberto Di Cosmo, Professor at Paris Diderot University
- Enrico Giunchiglia, Professor at the University of Genoa
- Éric Grégoire, Professor at the University of Artois
- Christophe Lecoutre, Professor at the University of Artois
- Joao Marques-Silva, Professor at the University of Dublin
- Lakhdar Saïs, Professor at the University of Artois
- Pierre Marquis, Professor at the University of Artois