SAT4J: pseudo-boolean optimization & dependency management problems
One important problem that arises in component based software is to build a product according to the dependencies (requirements or conflicts) between component. The aim of the lecture is to present that problem and how it can be solved using SAT-based techniques, namely Pseudo Boolean Optimization, and how a CDCL solver can be modified for that purpose. The last part of the lecture will present the open source SAT library Sat4j, used to resolve software dependencies within the Eclipse open platform since June 2008.
- Sat4j in the Sat Race 2010
- Sat4j MaxSat in the Max Sat 2010 competition
- The Pseudo Boolean Competition 2010
- The Pseudo Boolean Competition 2011
- The Mancoosi International Solver Competition
- p2cudf
Argelich Josep, Le Berre Daniel, Lynce Ines, Marques-Silva Joao, Rapicault Pascal,
Solving Linux Upgradeability Problems Using Boolean Optimization,
dans Workshop on Logics for Component Configuration (Lococo), pp. 11-22, july 2010.
Le Berre Daniel, Rapicault Pascal,
Dependency management for the Eclipse ecosystem,
dans Open Component Ecosystems International Workshop (IWOCE2009), august 2009.
Daniel Le Berre, Université d'Artois, France
Daniel Le Berre is associate professeur (maître de conférences habilité à diriger des recherches) in Artois University, in the Computer Science Laboratory of Lens. His main interest lies in various aspects of propositional logic, from the design of SAT solvers (Sat4j) to the design of new logics (Qualitative Choice Logic). He co-organized since 2002 with Laurent Simon, Edward Hirsch, Olivier Roussel and Matti Jarvisalo the SAT competition. He is also the man behind the SAT Live! community web site.