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
- common data structures
- basic data structures
- lazy data structures
- ...
- common algorithms
- DLL based procedures, with or without intelligent backtracking, with or without learning
- stochastic procedures
- syntactic procedures (resolution)
- a generic search procedure
- ...
- helpful tools
The use of the generic search procedure should allow to
- use non standard algorithms with non binary choice points
- save and restore the search (checkpointing)
- distribute the search over several hosts
- get a graphical representation of the search tree
- ...
Documentation
The documentation of the library will be composed of
- a general description of the library and its components
- a browsable documentation of the classes (javadoc like)
- some example algorithms
Programs
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.
Release
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.
Retour