Benchmarks
Industrial Track
| Benchmark | Training-Test-Split | Reference | DL |
|---|---|---|---|
| Bounded Model Checking (BMC) | 684/302 | derived by unrolling the HWMCC 2008 circuits | 11GB* |
| Circuit Fuzz | 299/302 | Generator | 82MB |
| IBM - Hardware Verification | 381/302 | IBM Formal Verification Benchmark Library | 1.7GB* |
Crafted Track
| Benchmark | Training-Test-Split | Reference | DL |
|---|---|---|---|
| Graph Isomorphism (GI) | 1032/351 | 2013 SAT Challenge Proceedings | 12GB |
| Low Autocorrelation Binary Sequence | 350/351 | 2013 SAT Challenge Proceedings | 1.4GB |
| Queens | 484/351 | generated by Norbert Manthey and Peter Steinke | 1.8GB |
Random SAT+UNSAT Track
| Benchmark | Training-Test-Split | Reference | DL |
|---|---|---|---|
| 3cnf | 500/250 | generated by Sam Bayless | 7.7MB |
| K3 | 300/250 | N/A | 166MB |
| unif-k5 | 300/250 | 2012 SAT Challenge Proceedings, Generator | 3.5MB |
Random SAT Track
| Benchmark | Training-Test-Split | Reference | DL |
|---|---|---|---|
| 3sat1k | 250/250 | Captain Jack | 13MB |
| 5sat500 | 250/250 | Captain Jack | 44MB |
| 7sat90 | 250/250 | Captain Jack | 35MB |
(*) The license of the BMC and IBM set is not known; therefore the sets are only available upon request.
Configurable SAT Solver Challenge (CSSC) 2014