SATLIB Benchmark Suite

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.