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
SOTA views
QBFEVAL'08
Family
Overall
Time
Hardness
N
#
S
U
EA
ME
MH
Abduction
303
288
154
134
1245.69
28
257
3
Adder
32
22
12
10
229.96
4
9
9
blackbox-01X-QBF
450
316
316
4823.68
129
154
33
blackbox_design
28
28
27
1
15.83
28
Blocks
13
13
4
9
23.76
4
9
BMC
132
115
57
58
1432.59
48
63
4
C432
8
8
3
5
704.43
3
2
3
C499
8
5
3
2
2.71
2
3
C5315
8
4
2
2
6.14
2
2
C6288
8
2
2
6.19
2
C880
8
2
2
22.92
2
Chain
12
12
12
0.28
12
circuits
63
7
7
64.65
1
6
comp
8
8
4
4
0.15
8
conformant_planning
24
16
10
6
1178.98
3
12
1
Counter
24
12
12
7.08
7
5
Debug
38
32
32
2459.1
17
15
DFlipFlop
10
10
10
2.15
10
evader-pursuer-4x4-logarithmic
7
7
7
18.06
7
evader-pursuer-4x4-standard
7
7
7
256.74
7
evader-pursuer-6x6-logarithmic
8
5
5
703.1
4
1
evader-pursuer-6x6-standard
8
1
1
243.7
1
evader-pursuer-8x8-logarithmic
8
4
4
14.83
4
FPGA_PLB_FIT_FAST
5
5
4
1
1.16
3
2
FPGA_PLB_FIT_SLOW
3
3
1
2
2.04
2
1
Impl
10
10
10
0.02
10
irqlkeapclte
46
1
1
1.29
1
jmc_quant
10
3
2
1
17.39
3
jmc_quant_squaring
10
3
2
1
8.82
3
k_branch_n
21
6
6
326.32
3
2
1
k_branch_p
21
16
16
291.93
3
1
12
k_d4_n
21
21
21
266.21
5
8
8
k_d4_p
21
21
21
15.73
6
15
k_dum_n
21
21
21
0.35
7
14
k_dum_p
21
21
21
0.41
11
10
k_grz_n
21
21
21
36.43
6
15
k_grz_p
21
21
21
23.26
6
15
k_lin_n
21
21
21
89.11
9
12
k_lin_p
21
21
21
2.89
15
6
k_path_n
21
21
21
0.52
6
15
k_path_p
21
21
21
0.46
7
14
k_ph_n
21
21
21
126.85
8
13
k_ph_p
21
11
11
184.39
7
3
1
k_poly_n
21
21
21
0.31
12
9
k_poly_p
21
21
21
0.28
15
6
k_t4p_n
21
21
21
34.74
2
19
k_t4p_p
21
21
21
17.16
4
17
Logn
2
2
2
5.1
2
MutexP
7
7
7
0.62
3
4
Qshifter
6
6
6
7.47
5
1
s1196
6
1
1
0.79
1
s1269
14
1
1
0.85
1
s27
4
4
1
3
0.12
4
s298
24
9
9
15.36
9
s3330
13
3
3
141.55
2
1
s386
11
11
7
4
1613.94
5
6
s499
25
14
14
201.26
14
s510
50
11
11
696.03
8
3
s713
10
3
3
10.22
3
s820
14
5
5
326.14
4
1
Sorting_networks
84
62
35
27
1577.72
12
46
4
SzymanskiP
12
12
12
112.89
2
10
term1
8
8
4
4
141.06
4
4
terminator
595
577
577
288.65
576
1
tipdiam
203
160
142
18
973.31
59
94
7
tipfixpoint
446
234
163
71
9338.75
13
184
37
Toilet
8
8
5
3
1.06
5
3
Tree
14
14
5
9
0.02
14
uclid
3
0
0
0
-
VonNeumann
10
10
10
12.3
9
1
wmiforward
72
69
69
369.27
11
39
19
z4ml
8
8
4
4
0.04
8
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org