TCS / Matti Järvisalo / SAT Benchmarks
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

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].


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 27 May 2008.