SATLIB - Benchmark Problems

All instances provided here are cnf formulae encoded in DIMACS cnf format. This format is supported by most of the solvers provided in the SATLIB Solvers Collection. For a description of the DIMACS cnf format, see DIMACS Challenge - Satisfiability: Suggested Format (ps file, 108k) (taken from the DIMACS FTP site).

Please help us to extend our benchmark set by submitting new benchmark instances or suggesting existing benchmarks we should include. We are especially interested in SAT-encoded problems from other domains, for example, encodings of problems available from CSPLIB.

At the moment, we provide mainly satisfiable instances, as many popular SAT algorithms are incomplete. However, we will extend our collection of unsatisfiable benchmark instances in the near future, to further facilitate comparative studies of complete algorithms.

• Uniform Random-3-SAT, phase transition region, unforced filtered - description (html)
  • uf20-91: 20 variables, 91 clauses - 1000 instances, all satisfiable
  • uf50-218 / uuf50-218: 50 variables, 218 clauses - 1000 instances, all sat/unsat
  • uf75-325 / uuf75-325: 75 variables, 325 clauses - 100 instances, all sat/unsat
  • uf100-430 / uuf100-430: 100 variables, 430 clauses - 1000 instances, all sat/unsat
  • uf125-538 / uuf125-538: 125 variables, 538 clauses - 100 instances, all sat/unsat
  • uf150-645 / uuf150-645: 150 variables, 645 clauses - 100 instances, all sat/unsat
  • uf175-753 / uuf175-753: 175 variables, 753 clauses - 100 instances, all sat/unsat
  • uf200-860 / uuf200-860: 200 variables, 860 clauses - 100 instances, all sat/unsat
  • uf225-960 / uuf225-960: 225 variables, 960 clauses - 100 instances, all sat/unsat
  • uf250-1065 / uuf250-1065: 250 variables, 1065 clauses - 100 instances, all sat/unsat

• Random-3-SAT Instances and Backbone-minimal Sub-instances (contributed by Josh Singer) - description (html)
  • RTI_k3_n100_m429: 100 variables, 429 clauses - 500 instances, all satisfiable
  • BMS_k3_n100_m429: 100 variables, number of clauses varies - 500 instances, all satisfiable

• Random-3-SAT Instances with Controlled Backbone Size (contributed by Josh Singer) - description (html)
  • CBS_k3_n100_m403_b10: 100 variables, 403 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m403_b30: 100 variables, 403 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m403_b50: 100 variables, 403 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m403_b70: 100 variables, 403 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m403_b90: 100 variables, 403 clauses, backbone size 90 - 1000 instances, all satisfiable
  • CBS_k3_n100_m411_b10: 100 variables, 411 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m411_b30: 100 variables, 411 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m411_b50: 100 variables, 411 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m411_b70: 100 variables, 411 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m411_b90: 100 variables, 411 clauses, backbone size 90 - 1000 instances, all satisfiable
  • CBS_k3_n100_m418_b10: 100 variables, 418 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m418_b30: 100 variables, 418 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m418_b50: 100 variables, 418 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m418_b70: 100 variables, 418 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m418_b90: 100 variables, 418 clauses, backbone size 90 - 1000 instances, all satisfiable
  • CBS_k3_n100_m423_b10: 100 variables, 423 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m423_b30: 100 variables, 423 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m423_b50: 100 variables, 423 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m423_b70: 100 variables, 423 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m423_b90: 100 variables, 423 clauses, backbone size 90 - 1000 instances, all satisfiable
  • CBS_k3_n100_m429_b10: 100 variables, 429 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m429_b30: 100 variables, 429 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m429_b50: 100 variables, 429 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m429_b70: 100 variables, 429 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m429_b90: 100 variables, 429 clauses, backbone size 90 - 1000 instances, all satisfiable
  • CBS_k3_n100_m435_b10: 100 variables, 435 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m435_b30: 100 variables, 435 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m435_b50: 100 variables, 435 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m435_b70: 100 variables, 435 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m435_b90: 100 variables, 435 clauses, backbone size 90 - 1000 instances, all satisfiable
  • CBS_k3_n100_m441_b10: 100 variables, 441 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m441_b30: 100 variables, 441 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m441_b50: 100 variables, 441 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m441_b70: 100 variables, 441 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m441_b90: 100 variables, 441 clauses, backbone size 90 - 1000 instances, all satisfiable
  • CBS_k3_n100_m449_b10: 100 variables, 449 clauses, backbone size 10 - 1000 instances, all satisfiable
  • CBS_k3_n100_m449_b30: 100 variables, 449 clauses, backbone size 30 - 1000 instances, all satisfiable
  • CBS_k3_n100_m449_b50: 100 variables, 449 clauses, backbone size 50 - 1000 instances, all satisfiable
  • CBS_k3_n100_m449_b70: 100 variables, 449 clauses, backbone size 70 - 1000 instances, all satisfiable
  • CBS_k3_n100_m449_b90: 100 variables, 449 clauses, backbone size 90 - 1000 instances, all satisfiable

• "Flat" Graph Colouring, 3 colourable - description (html)
  • flat30-60: 30 vertices, 60 edges - 100 instances, all satisfiable
  • flat50-115: 50 vertices, 115 edges - 1000 instances, all satisfiable
  • flat75-180: 75 vertices, 180 edges - 100 instances, all satisfiable
  • flat100-239: 100 vertices, 239 edges - 100 instances, all satisfiable
  • flat125-301: 125 vertices, 301 edges - 100 instances, all satisfiable
  • flat150-360: 150 vertices, 360 edges - 100 instances, all satisfiable
  • flat175-417: 175 vertices, 417 edges - 100 instances, all satisfiable
  • flat200-479: 200 vertices, 479 edges - 100 instances, all satisfiable

• "Morphed" Graph Colouring, 5 colourable - description (html)
  • sw100-8-lp0-c5: 100 vertices, 400 edges, p=1 - 100 instances, all satisfiable
  • sw100-8-lp1-c5: 100 vertices, 400 edges, p=2^-1 - 100 instances, all satisfiable
  • sw100-8-lp2-c5: 100 vertices, 400 edges, p=2^-2 - 100 instances, all satisfiable
  • sw100-8-lp3-c5: 100 vertices, 400 edges, p=2^-3 - 100 instances, all satisfiable
  • sw100-8-lp4-c5: 100 vertices, 400 edges, p=2^-4 - 100 instances, all satisfiable
  • sw100-8-lp5-c5: 100 vertices, 400 edges, p=2^-5 - 100 instances, all satisfiable
  • sw100-8-lp6-c5: 100 vertices, 400 edges, p=2^-6 - 100 instances, all satisfiable
  • sw100-8-lp7-c5: 100 vertices, 400 edges, p=2^-7 - 100 instances, all satisfiable
  • sw100-8-lp8-c5: 100 vertices, 400 edges, p=2^-8 - 100 instances, all satisfiable
  • sw100-8-p0-c5: 100 vertices, 400 edges, p=0 - 1 instance, satisfiable

• Planning (contributed by Henry Kautz and Bart Selman)
  • blocksworld: 7 instances, all satisfiable - description (html)
  • logistics: 3 instances, all satisfiable - description (html)

• All Intervall Series - description (html)
  • ais: 4 instances, all satisfiable

• SAT-encoded Quasigroup (or Latin square) instances (contributed by Hantao Zhang)- description (html)
  • qg: 22 instances

• SAT-encoded bounded model checking intances (contributed by Ofer Shtrichman)- description (html)
  • bmc: 13 instances

• DIMACS Benchmark Instances (original source: DIMACS Benchmark set for SAT) - overview (ps-file, 72k)
  • AIM: Artificially generated Random-3-SAT - 48 instances satisfiable, 24 unsatisfiable description (html)
  • LRAN: Large Random-3-SAT instances - 3 instances, all satisfiable description (html)
  • JNH: Random SAT instances with variable length clauses - 16 instances satisfiable, 34 instances unsatisfiable description (html)
  • DUBOIS: Randomly generated SAT instances - 13 instances, all unsatisfiable description (html)
  • GCP: Large SAT-encoded Graph Colouring problems - 4 instances, all satisfiable description (html)
  • PARITY: Instances for problem in learning the parity function - 20 instances, all satisfiable description (html)
  • II: Instances from a problem in inductive inference - 41 instances, all satisfiable description (html)
  • HANOI: SAT-encoding of Towers of Hanoi - 2 instances, all satisfiable description (html)
  • BF: Circuit fault analysis: bridge fault - 4 instances, all unsatisfiable description (html)
  • SSA: Circuit fault analysis: single-stuck-at fault - 4 instances satisfiable, 4 instances unsatisfiable description (html)
  • PHOLE: Pigeon hole problem - 5 instances, all unsatisfiable description (html)
  • PRET: Encoded 2-colouring forced to be unsatisfiable - 8 instances, all unsatisfiable description (html)

• SAT Competition Bejing (original source: Bejing Competition benchmark set) - original guide (ps-file, 42k) - description (html)
  • Bejing: 16 instances

• More test-sets and instances coming soon!