QBF Solver Evaluation Portal
Home
QBFLIB
QBFGALLERY'23
QBFEVALs
2022
2020
2019
2018
2017
2016
2010
2008
2007
2006
2005
2004
QBF GALLERIES
QBF Gallery 2014
QBF Gallery 2013
DOWNLOADS
Download the QBFEVAL'22 dataset
Download the QBFEVAL'20 dataset
Download the QBFEVAL'19 dataset and raw results
Download the QBFEVAL'18 dataset and raw results
Download the QBFEVAL'17 dataset and raw results
Download the QBFEVAL'16 dataset
Download the QBFEVAL'10 dataset
Download the QBFEVAL'08 dataset
Download the non-prenex non-cnf track dataset
Download the QBFEVAL'07 dataset
Download the QBFEVAL'06 dataset
Download the QDIMACS to QPRO converter
Download the QDIMACS to QBF1.0 converter
qbflib.org
cheq results solving families - 2016
Family
# Total
# Sat
# Unsat
Time
Abduction
71
4
3
6215.19
Adder
115
61579.24
blackbox-01X-QBF
77
6
19725.25
blackbox_design
76
46695.18
Blocks
88
2
28982.93
BMC
91
2
1
43298.84
bomb
51
79.65
C432
73
3
1
26541.83
C499
76
3
26246.86
C5315
86
1
44657.78
C6288
86
53084.09
C880
78
1
42535.27
Chain
82
4
35885.85
circuits
75
1
42285.81
conformant_planning
88
3
1
36881.77
Connect4
68
4
16234.64
Counter
54
4
20220.81
Debug
103
62537.41
DFlipFlop
73
1
1714.1
dungeon
73
44551.84
evader-pursuer-4x4-logarithmic
61
4
19073.67
evader-pursuer-4x4-standard
65
39686.64
evader-pursuer-6x6-logarithmic
74
1
31274.43
evader-pursuer-6x6-standard
77
46972.96
evader-pursuer-8x8-logarithmic
78
1
34464.07
FPGA_PLB_FIT_FAST
38
3
1
4878.12
FPGA_PLB_FIT_SLOW
25
1
1
6825.22
fpu
47
3
22253.2
Generalized-Tic-Tac-Toe
54
1
2
11196.33
HardwareFixpoint
81
50132.56
Impl
74
10
0.74
incrementer-encoder
67
6
25092.44
irqlkeapclte
121
75122.63
ISCAS89
32
17235.59
ITC99
56
29742.44
jmc_quant_squaring
118
72082.6
k_branch_n
88
2
47251.65
k_branch_p
103
61719.75
k_d4_n
73
3
34489.08
k_d4_p
72
37414.27
k_dum_n
66
4
25896.01
k_dum_p
74
30109.14
k_grz_n
68
3
32944.76
k_grz_p
70
37413.15
k_lin_n
64
6
20367.72
k_lin_p
65
299.27
k_path_n
67
2
32986.47
k_path_p
67
2
33060.66
k_ph_n
74
10
6208.69
k_ph_p
85
1
41090.48
k_poly_n
68
1
38009.84
k_poly_p
64
1
35606.66
k_t4p_n
71
43520.74
k_t4p_p
76
46420.44
LinearBitvectorRankingFunction
86
52717.96
Logn
29
2
70.37
mqm
84
2
4
26524.01
MutexP
78
3
29876.98
Planning-CTE
55
2
28064.15
QBF-Hardness
63
3
27076.59
qbfeval12
27
1
2
3426.25
Qshifter
62
1
32147.45
RankingFunctions
61
37275.15
Reduction-finding
65
1
28833.06
Rewriting
45
10
2.14
s1196
44
24181.67
s1269
76
45065.24
s27
36
1
17626.18
s298
70
41945.96
s3330
76
43372.92
s386
69
41122.72
s499
62
36887.5
s510
59
35723.79
s641
55
28234.71
s713
73
38014.74
s820
72
43152.51
Sorting_networks
110
1
59464.9
SzymanskiP
99
9
12782.98
term1
69
4
12332.54
terminator
86
53175.9
tipdiam
86
4
38632.36
tipfixpoint
81
3
38592.16
ToiletA
48
3
7
10.37
ToiletC
48
1
3021.47
ToiletG
43
7
0.72
trafficlight-controller
45
8
5923.68
Tree
74
2
8
54.01
uclid
30
18225.29
VonNeumann
75
7
20922.21
wmiforward
74
3
33138.8
z4ml
61
4
1.13
Contact
|
Organization
|
Links
|
Citing QBFLIB