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 - Solver Portfolio Track.
Family
Overall
Time
Hardness
N
#
S
U
EA
ME
MH
Abduction
10
9
4
5
12.58
9
Adder
10
4
2
2
284.32
2
1
1
blackbox-01X-QBF
10
8
8
170.8
4
3
1
blackbox_design
10
10
10
15.53
10
Blocks
10
10
3
7
13.24
10
BMC
10
7
4
3
79.27
3
3
1
bomb
10
4
4
50.33
3
1
C432
8
8
3
5
351.59
5
3
C499
8
5
3
2
4.01
5
C5315
8
4
2
2
10.48
3
1
C6288
8
2
2
8.42
2
C880
8
2
2
0.84
1
1
Chain
10
10
10
1.6
5
5
circuits
10
2
2
43.52
1
1
conformant_planning
10
9
5
4
662.6
3
5
1
Connect4
10
6
6
9.01
2
4
Counter
10
9
9
10.61
8
1
Debug
10
8
8
584.95
8
DFlipFlop
10
10
10
11.74
7
3
dungeon
10
10
10
84.85
9
1
evader-pursuer-4x4-logarithmic
7
7
7
11.18
5
1
1
evader-pursuer-4x4-standard
7
5
5
521.3
2
3
evader-pursuer-6x6-logarithmic
8
3
3
48.13
3
evader-pursuer-6x6-standard
8
2
2
66.46
2
evader-pursuer-8x8-logarithmic
8
4
4
16.2
2
1
1
FPGA_PLB_FIT_FAST
5
5
4
1
2.82
5
FPGA_PLB_FIT_SLOW
3
3
1
2
3.62
3
fpu
10
10
10
61.83
10
Generalized-Tic-Tac-Toe
10
9
1
8
245.12
8
1
HardwareFixpoint
10
5
2
3
15.53
5
Impl
10
10
10
1.2
10
incrementer-encoder
10
6
6
14.32
5
1
irqlkeapclte
10
0
0
0
-
ISCAS89
7
7
6
1
39.49
6
1
ITC99
7
3
2
1
10.53
1
2
jmc_quant_squaring
10
3
2
1
153.82
3
k_branch_n
10
9
9
21.11
3
6
k_branch_p
10
9
9
29.97
8
1
k_d4_n
10
10
10
6.22
7
3
k_d4_p
10
10
10
2.6
10
k_dum_n
10
10
10
1.51
10
k_dum_p
10
10
10
1.72
10
k_grz_n
10
10
10
3.1
10
k_grz_p
10
10
10
2.6
10
k_lin_n
10
10
10
19.55
10
k_lin_p
10
10
10
2.21
10
k_path_n
10
10
10
2.02
10
k_path_p
10
10
10
2.4
10
k_ph_n
10
10
10
90.55
4
2
4
k_ph_p
10
4
4
173.44
3
1
k_poly_n
10
10
10
1.73
10
k_poly_p
10
10
10
1.61
10
k_t4p_n
10
10
10
4.9
10
k_t4p_p
10
10
10
3.73
10
LinearBitvectorRankingFunction
10
0
0
0
-
Logn
4
4
4
4.74
2
2
mqm
10
10
5
5
596.99
5
3
2
MutexP
7
7
7
3.63
7
Planning-CTE
7
5
2
3
343.97
3
2
QBF-Hardness
10
8
1
7
66.48
6
2
qbfeval12
6
5
1
4
3.72
5
Qshifter
6
6
6
13.44
6
RankingFunctions
10
10
10
6.33
6
4
Reduction-finding
10
7
2
5
16.79
5
2
Rewriting
10
10
10
1.2
10
s1196
6
5
1
4
762.3
5
s1269
10
3
3
212.15
3
s27
4
4
1
3
0.88
4
s298
10
6
6
239.65
2
4
s3330
10
2
2
139.39
2
s386
10
10
5
5
607.96
1
9
s499
10
6
6
650.41
6
s510
10
3
3
113.07
3
s641
9
8
5
3
575.62
1
7
s713
10
8
5
3
789.03
1
7
s820
10
5
5
601.88
1
4
Sorting_networks
10
8
4
4
341.41
5
2
1
SzymanskiP
10
10
10
124.01
6
4
term1
8
8
4
4
198.73
4
2
2
terminator
10
8
8
81.05
4
2
2
tipdiam
10
5
5
8.2
4
1
tipfixpoint
10
6
3
3
8.34
1
3
2
ToiletA
10
10
3
7
3.02
10
ToiletC
10
10
1
9
10.51
10
ToiletG
7
7
7
0.91
7
trafficlight-controller
10
10
10
52.61
7
3
Tree
10
10
2
8
1.21
10
uclid
3
0
0
0
-
VonNeumann
10
10
10
26.94
10
wmiforward
10
10
10
2.51
5
5
z4ml
8
8
4
4
0.96
8
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org