Challenging benchmarks

Quick Help: This set of challenging benchmarks is based on the biggest subset of benchs on which all solvers have been tested. It is based only on SatEx experimentations with the cpu-cutoff paramater of 10000s on the reference machine (see FAQ for more details about runnings). A challenging benchmarks is one that has not been solved by any solver within the given cpu time.

This challenging section is only based on:

The following 23 SAT-solvers: asat, calcres, csat, dr, eqsatz, heerhugo, modoc, modoc-2.0, nsat, ntab, ntab_back, ntab_back2, posit, relsat, relsat-200, sat-grasp, sato, sato-3.2.1, satz, satz-213, satz-215, zchaff, zres
The following 11 benchs origins: avg-checker, beijing, bmc, des-encryption, dimacs, formal-verification, miters, morphed, paderborn, quasigroup, ucsc

List of 10 Challenging benchmarks

cnf-r4-b1-k1.1-comp, from the des-encryption
cnf-r4-b1-k1.2-comp, from the des-encryption
f1000, from the f
f2000, from the f
g125.17, from the g
g125.18, from the g
g250.15, from the g
g250.29, from the g
par32-5-c, from the Parity-32
par32-5, from the Parity-32

List of 26 benchmarks solved by one or two provers only

2dlx_ca_mc_ex_bp_f, from the fvp
2dlx_cc_mc_ex_bp_f, from the fvp
3bitadd_31, from the Beijing
9vliw_bp_mc, from the fvp
c3540-s, from the miters
c5315-s, from the miters
c5315, from the miters
c6288-s, from the miters
c6288, from the miters
c7552-s, from the miters
c7552, from the miters
cnf-r4-b2-k1.1-comp, from the des-encryption
cnf-r4-b2-k1.2-comp, from the des-encryption
cnf-r4-b3-k1.1-comp, from the des-encryption
cnf-r4-b3-k1.2-comp, from the des-encryption
cnf-r4-b4-k1.1-comp, from the des-encryption
cnf-r4-b4-k1.2-comp, from the des-encryption
f600, from the f
par32-1-c, from the Parity-32
par32-1, from the Parity-32
par32-2-c, from the Parity-32
par32-2, from the Parity-32
par32-3-c, from the Parity-32
par32-3, from the Parity-32
par32-4-c, from the Parity-32
par32-4, from the Parity-32

List of 6 solvers that solves at least one of the quasi-challenges

Scripts last modified on 01-07-2001
File generated on 6-09-2001