|Download the tarball of glucosER or directly use the zipped Linux 32 bits static precompiled version. The source uses the C++ Boost library.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|
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.
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.