SAT'11 Proc.


Aug, 2011: (New) Web Site opens

Last News

glucose v2.1 code released
Jul, 2012

glucose v2.1 won the "best single engine solver in the application track" category un the SAT challenge 2012.
Jun, 2012

glucose v.2 released
Jul. 12, 2011

glucose v2 won 3 medals at the SAT 2011 competition
Jun. 23, 2011

SAT Conference
June 19th to 22th, 2011 (inclusive)

Don't Miss this

SAT'2013 in Helsinki!


This Site will close! Since September 2013, I have a professor position at the Labri (Bordeaux). This web site is obsolete now and I strongly encourage you to jump to my new web site! In a few months, I'll close this web site and put redirections.



Viewing extended resolution as a compression technique
In GlucosER, we see the powerful
ER rule as a compression rule
glucosER is our solver enriched with Extended Resolution (see paper "A Restriction of Extended Resolution for Clause Learning SAT Solvers", by G. Audemard, G. Katsirelos and L. Simon, in AAAI-2010, july 2010). This solver was developed with G. Katsirelos, during its Post-Doc, thanks to our UNLOC project. It's aim is to push CDCL solvers to more powerful proof systems, without loosing practical performances on industrial problems. Results are quite encouraging, thanks to a new vision on what extended resolution can do: we see this powerful reasoning mechanism as a way to compress the resolution proof the CDCL is working on. You can Download the tarball of glucosER or directly use the zipped Linux 32 bits static precompiled version. The source uses the C++ Boost library.


The first trophy of Glucose
The first Trophy of Glucose, v.1

Our SAT solver, glucose (the SAT solver that looks for glue clauses), won the SAT Competition 2009 in the Application (Industrial) UNSAT Track, a track of particular interest for many industrial applications of SAT. It also has the silver medal in the SAT+UNSAT track (it solved the same number of benchmarks as precosat). This is the first time a french team wins the competition in the Application/Industrial track. Our solver is based on the last publicly available version of Minisat and illustrates the efficiency of our new static score of clauses, based on our IJCAI'09 paper (see below).

Source code and paper available at glucose home page


SomeWhere is a Java-Based semantic peer-to-peer data management system that promotes a small is beautiful vision of the Semantic Web based on simple personalized ontologies (e.g., taxonomies of classes) but which are distributed at a large scale. In this vision of the Semantic Web, no user imposes to others his own ontology. Logical mappings between ontologies make possible the creation of a web of people in which personalized semantic marking up of data cohabits nicely with a collaborative exchange of data. In this view, the Web is a huge peer-to-peer data management system based on simple distributed ontologies and mappings. You can see how the Firefox somewhere extension works. Project done with P. Adjiman, M.-C. Rousset, F. Goasdoué, P. Chatalic.


zres is an implementation of the very procedure of Davis and Putnam as stated in 1960. It uses ZBDDs as a data structure to represent set of clauses. It demonstrates the efficiency of multi-resolution for symbolic reasoning. The package used to manipulate ZBDD is the CUDD package (a great BDD package), available the home page of Fabio Somenzi, its main author.

zres is a very good solver for prime implicates generation, one of the hardest tasks of classical A.I. approaches to reasonning.

zres was successfully extended to QBF by M. Vardi to QMRes with Guoqiang Pan.


The SatEx was a web-site publishing experiments of solvers on benchmarks. It has been replaced by all sat competitions and sat races web sites. If you need to acces to my old datas (old solvers, old benchmarks (before 2002)), please contact me. I'm trying to build a new satex web site, but this may take me some time.