SAT Benchmarks

Satisfiable Boolean circuit satisfiability benchmarks used in the ECAI'08 paper [9] are available here. The circuits encode bounded model checking of asynchronous systems for deadlocks as presented in the paper Heljanko, K.: Bounded Reachability Checking with Process Semantics. In Proceedings of the 12th International Conference on Concurrency Theory (Concur'2001), pages 218-232, Lecture Notes in Computer Science 2154, Springer 2001, and have been generated with the punroll tool.
Boolean circuit satisfiability benchmarks used in the JARGOL'08 [8], CP'07 [7], and RCRA'07 papers [5] are available here. (Contains the Boolean circuit satisfiability benchmarks also used in the Licentiate's thesis [6].)
Equivalence checking multiplier designs: Unsatisfiable CNFs encoding the problem of equivalence checking two hardware designs for integer multiplication, as submitted to the SAT Competition 2007: multiplier-equivalence.benchmark.satcomp07.tgz. For a brief description, see [4].
Regular XORSAT: Benchmark instances based on 3-regular graphs (Regular XORSAT [1])
- The set of instances submitted to the SAT Competition 2005: hjkn-mod2-benchmarks.tar.gz. For a brief description see [2] and this.
- The results of the SAT competition 2005 are here. The benchmark set provided some of the smallest unsolved instances (w.r.t. number of variables).
- An instance generator is also available (in C for Linux):
  rgen - a SAT benchmark generator based on 3-regular bipartite graphs. [bibtex]
Regular k-XORSAT: An instance generator for the generalized Regular k-XORSAT model [3] is available [here].