This is the Canadian SATLIB site, hosted by the Laboratory for Computational Intelligence at the Computer Science Department of the University of British Columbia in Vancouver (Canada). The SATLIB main site (which should be used for bookmarking purposes) can be found at

SATLIB - The Satisfiability Library

Version 1.4.4, 01/05/11 - version history / news / updates

created and maintained by Holger H Hoos & Thomas Stützle at Darmstadt University of Technology



SATLIB is a collection of benchmark problems, solvers, and tools we are using for our own SAT related research. One strong motivation for creating SATLIB is to provide a uniform test-bed for SAT solvers as well as a site for collecting SAT problem instances, algorithms, and empirical characterisations of the algorithms' performance.

The SATLIB Benchmark Suite comprises three different types of problems: test-sets sampled from random instance distributions, such as uniform Random-3-SAT; test-sets obtained by encoding instances from random instance distribution of SAT-encoded combinatorial problems such as Graph Colouring; and individual SAT-encoded instances from various domains. The majority of the instances from the benchmark suite is considered hard for both systematic and local search algorithms for SAT. For the SAT-encoded problems, the hardness of the instances is typically inherent rather than just induced by the encoding scheme that was used for transforming them into SAT.

The SATLIB Solvers Collection includes the original distributions of some of the most powerful SAT algorithms we are currently aware of. We intend to add brief descriptions of these solvers soon.

The Solver Evaluation Section is currently under construction and will contain the results of our extensive empirical study on the characterisation of the behaviour of stochastic local search algorithms when applied to the benchmark suite.

The Tools Collection is currently under construction and will contain useful tools for converting SAT instances between different formats and empirically analysing the behaviour of SAT algorithms.

The Annotated Bibliography on SAT contains pointers to papers on SAT solvers, algorithms, and applications as well as closely related areas. This section is still incomplete and we appreciate to get references to papers you'd like to see included in this list.

Finally, SATLIB maintains lists of links to related sites, people involved in SAT research, and SAT related events. These are very incomplete and will be updated upon request.

Your contributions are always welcome. If you want to submit benchmark problems, solvers, or tools, we ask you to follow the submission guidelines and/or to contact us by email. We also appreciate feedback, comments, and suggestions for improving SATLIB.

DISCLAIMER OF WARRANTY. The software hosted on this page is research work provided by various people (as indicated above). The software is provided "as is" without warranty of any kind and without any support services
© hh, last update 01/05/11.