The orsat Library

This page is in construction (last update 2004/05/07)

Short description

The goal of the orsat library is to provide a set of data structures, algorithms and tools to facilitate the implementation of novative algorithms more or less directly linked to the satisfiability problem (SAT).

To this end, the library should offer a good level of genericity while maintaining reasonable efficiency. The stress is put on the genericity of the code to allow code reuse and speed up the developpment of new prototypes. Efficiency is not neglected, but is only the second priority.

This library is developped in C++, with the use of templates. The choice of C++ is a good compromise which allows the development of generic and efficient code.

The library should eventually provide the user with


The documentation of the library will be composed of


A very first prover using a preliminary version of this library has been developed for the QBF 2004 evaluation. This development was a first test to experiment with the ability of the library to accomodate with different requirements. This experimental prover has been developed in a few weeks and was not completely achieved when it was submitted. Furthermore, the algorithm that was used was experimental too. Therefore, the performances of that prover are quite poor. You may want to read the two pages description of the solver that was written for the evaluation.


The library is still in the early phase of its development and we don't think it's very useful to make available code that is obviously completely unstable. Therefore, the first public release of the library is not expected before the summer 2004.