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
Solver performances for family instances
QBFEVAL'08
Family
Overall
Time
Reference solver
N
#
S
U
Abduction
303
286
152
134
731.75
QuBE6.1
Adder
32
20
11
9
705.33
Nenofex
blackbox-01X-QBF
450
310
0
310
10607.7
AQME-1NN
blackbox_design
28
28
27
1
15.83
QuBE6.1
Blocks
13
13
4
9
25.24
Nenofex
BMC
132
114
56
58
1462.5
quantor3.0
C432
8
7
3
4
490.22
quantor3.0
C499
8
5
3
2
348.54
AQME-1NN
C5315
8
4
2
2
7.14
quantor3.0
C6288
8
2
2
0
6.53
ssolve-A
C880
8
2
2
0
22.93
ssolve-A
Chain
12
12
12
0
0.28
quantor3.0
circuits
63
7
7
0
69.48
AQME-1NN
comp
8
8
4
4
0.16
quantor3.0
conformant_planning
24
16
10
6
1710.01
quantor3.0
Counter
24
12
12
0
15.79
AQME-1NN
Debug
38
32
32
0
2459.1
quantor3.0
DFlipFlop
10
10
0
10
2.15
quantor3.0
evader-pursuer-4x4-logarithmic
7
7
7
0
21.31
AQME-1NN
evader-pursuer-4x4-standard
7
7
7
0
256.74
QuBE6.1
evader-pursuer-6x6-logarithmic
8
5
0
5
759.38
ssolve-A
evader-pursuer-6x6-standard
8
1
0
1
243.7
AQME-1NN
evader-pursuer-8x8-logarithmic
8
4
0
4
18.1
AQME-1NN
FPGA_PLB_FIT_FAST
5
5
4
1
2.21
quantor3.0
FPGA_PLB_FIT_SLOW
3
3
1
2
2.04
quantor3.0
Impl
10
10
10
0
0.04
quantor3.0
irqlkeapclte
46
1
1
0
1.29
AQME-1NN
jmc_quant
10
3
2
1
17.39
QuBE6.1
jmc_quant_squaring
10
3
2
1
8.82
QuBE6.1
k_branch_n
21
5
5
0
20.93
ssolveC
k_branch_p
21
16
0
16
295.14
AQME-1NN
k_d4_n
21
21
21
0
268.72
AQME-1NN
k_d4_p
21
21
0
21
19.76
ssolveC
k_dum_n
21
21
21
0
0.35
quantor3.0
k_dum_p
21
21
0
21
0.41
quantor3.0
k_grz_n
21
21
21
0
56.52
Nenofex
k_grz_p
21
21
0
21
31.27
AQME-1NN
k_lin_n
21
21
21
0
167.52
QuBE6.1
k_lin_p
21
21
0
21
3.2
QuBE6.1
k_path_n
21
21
21
0
0.52
quantor3.0
k_path_p
21
21
0
21
0.47
quantor3.0
k_ph_n
21
21
21
0
159.68
QuBE6.1
k_ph_p
21
11
0
11
184.75
QuBE6.1
k_poly_n
21
21
21
0
0.31
quantor3.0
k_poly_p
21
21
0
21
0.29
quantor3.0
k_t4p_n
21
21
21
0
57.76
AQME-1NN
k_t4p_p
21
21
0
21
26.84
AQME-1NN
Logn
2
2
0
2
5.1
Nenofex
MutexP
7
7
7
0
0.63
ssolveC
Qshifter
6
6
6
0
7.67
ssolveC
s1196
6
1
1
0
0.79
QuBE6.1
s1269
14
1
1
0
0.85
QuBE6.1
s27
4
4
1
3
0.17
QuBE6.1
s298
24
9
9
0
15.36
QuBE6.1
s3330
13
3
3
0
141.55
QuBE6.1
s386
11
11
7
4
1613.94
QuBE6.1
s499
25
14
14
0
201.26
QuBE6.1
s510
50
11
11
0
696.03
QuBE6.1
s713
10
3
3
0
10.22
QuBE6.1
s820
14
5
5
0
326.14
QuBE6.1
Sorting_networks
84
59
35
24
2147.18
AQME-1NN
SzymanskiP
12
12
0
12
112.91
QuBE6.1
term1
8
8
4
4
215.32
QuBE6.1
terminator
595
577
0
577
6447.71
AQME-1NN
tipdiam
203
158
140
18
2530.36
AQME-1NN
tipfixpoint
446
230
162
68
9997.25
QuBE6.1
Toilet
8
8
5
3
1.06
quantor3.0
Tree
14
14
5
9
0.05
Nenofex
VonNeumann
10
10
0
10
12.3
quantor3.0
wmiforward
72
69
69
0
517.73
AQME-1NN
z4ml
8
8
4
4
0.05
quantor3.0
Contact
|
Organization
|
Links
|
Citing QBFLIB