SATLIB - The Satisfiability Library

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

Overview:

• Introduction
• SAT Benchmark Problems
• SAT Solvers
• SAT Solvers Evaluation
• SAT Tools
• SAT Annotated Bibliography
• Links to Related Sites
• Some People Involved in SAT Research
• SAT-related Conferences, Special Issues

Introduction

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.