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'16 - Prenex CNF Track.
Family
Overall
Time
Hardness
N
#
S
U
EA
ME
MH
Abduction
10
9
4
5
13.16
9
Adder
10
9
4
5
194.83
1
5
3
blackbox-01X-QBF
10
10
10
4.43
10
blackbox_design
10
10
10
0.91
10
Blocks
10
10
2
8
0.39
1
9
BMC
10
10
2
8
39.42
9
1
bomb
10
10
4
6
160.13
6
4
C432
8
8
3
5
3.43
1
7
C499
8
8
4
4
13.67
2
6
C5315
8
5
4
1
4.43
1
4
C6288
8
3
3
53.88
2
1
C880
8
8
5
3
413.55
6
2
Chain
10
10
10
0.09
10
circuits
10
8
8
753.6
1
3
4
conformant_planning
10
10
5
5
211.74
2
8
Connect4
10
9
3
6
997.38
6
3
Counter
10
10
10
35.36
3
7
Debug
10
2
2
825.81
2
DFlipFlop
10
10
10
0.42
10
dungeon
10
10
10
134.59
5
5
evader-pursuer-4x4-logarithmic
7
7
7
1.67
7
evader-pursuer-4x4-standard
7
7
7
86.56
7
evader-pursuer-6x6-logarithmic
8
6
6
276.29
6
evader-pursuer-6x6-standard
8
3
3
340.64
3
evader-pursuer-8x8-logarithmic
8
5
5
351.28
5
FPGA_PLB_FIT_FAST
5
5
4
1
0.14
2
3
FPGA_PLB_FIT_SLOW
3
3
1
2
0.36
3
fpu
10
10
10
5.41
10
Generalized-Tic-Tac-Toe
10
10
10
22.12
10
HardwareFixpoint
10
9
2
7
268.58
5
4
Impl
10
10
10
0
10
incrementer-encoder
10
10
1
9
10.3
10
irqlkeapclte
10
10
10
148.74
10
ISCAS89
7
7
6
1
33.66
2
5
ITC99
7
4
3
1
25.62
1
3
jmc_quant_squaring
10
8
4
4
27.66
4
4
k_branch_n
10
9
9
11.3
3
6
k_branch_p
10
10
10
39.46
10
k_d4_n
10
10
10
0.54
3
7
k_d4_p
10
10
10
0.26
10
k_dum_n
10
10
10
0.09
4
6
k_dum_p
10
10
10
0.09
10
k_grz_n
10
10
10
0.2
7
3
k_grz_p
10
10
10
0.25
10
k_lin_n
10
10
10
3.89
10
k_lin_p
10
10
10
0.19
10
k_path_n
10
10
10
0.18
4
6
k_path_p
10
10
10
0.23
10
k_ph_n
10
10
10
16.05
8
2
k_ph_p
10
6
6
244.73
1
3
2
k_poly_n
10
10
10
0.07
1
9
k_poly_p
10
10
10
0.08
10
k_t4p_n
10
10
10
0.49
1
9
k_t4p_p
10
10
10
0.38
10
LinearBitvectorRankingFunction
10
7
5
2
729.08
2
5
Logn
4
4
4
0.86
4
mqm
10
10
5
5
75.62
10
MutexP
7
7
7
0.18
1
6
Planning-CTE
7
7
2
5
181.77
7
QBF-Hardness
10
10
1
9
29.68
2
8
qbfeval12
6
5
1
4
0.06
3
3
Qshifter
6
6
6
1.62
2
4
RankingFunctions
10
10
10
0.31
10
Reduction-finding
10
9
2
7
43.42
2
6
1
Rewriting
10
10
10
0.02
10
s1196
6
6
6
1.07
6
s1269
10
5
5
91.36
5
s27
4
4
1
3
0
1
3
s298
10
10
6
4
2.22
1
9
s3330
10
7
5
2
337.64
5
2
s386
10
10
5
5
0.93
10
s499
10
10
10
2.66
10
s510
10
10
9
1
11.07
10
s641
9
9
9
0.74
9
s713
10
10
10
1.06
10
s820
10
10
6
4
3.21
10
Sorting_networks
10
10
6
4
116.92
1
9
SzymanskiP
10
10
10
35.3
10
term1
8
8
5
3
0.64
6
2
terminator
10
10
1
9
193.5
9
1
tipdiam
10
10
5
5
26.99
4
4
2
tipfixpoint
10
10
6
4
15.34
10
ToiletA
10
10
3
7
0.37
7
3
ToiletC
10
10
1
9
0.69
7
3
ToiletG
7
7
7
0
7
trafficlight-controller
10
10
3
7
8.1
3
7
Tree
10
10
2
8
0
1
9
uclid
3
2
1
1
2.68
2
VonNeumann
10
10
10
2.79
10
wmiforward
10
10
10
0.17
3
7
z4ml
8
8
4
4
0
4
4
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org