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'16 - Prenex CNF Track.
Family
Overall
Time
Reference solver
N
#
S
U
Abduction
10
9
4
5
26.27
depqbf-v3
Adder
10
9
6
3
607.98
AIGSolve
blackbox-01X-QBF
10
10
0
10
10.38
rareqs
blackbox_design
10
10
10
0
1.24
aqua-s2v
Blocks
10
10
3
7
0.62
rareqs
BMC
10
9
0
9
41.66
qsts
bomb
10
9
3
6
759.42
xb-bid-qsts
C432
8
8
3
5
6.42
AIGSolve
C499
8
8
3
5
25.57
AIGSolve
C5315
8
5
3
2
9.64
ghostq-plain
C6288
8
3
3
0
310.85
xb-bid-qsts
C880
8
8
2
6
458.33
ghostq-plain
Chain
10
10
10
0
0.09
qestos
circuits
10
5
5
0
551.49
xb-bid-qsts
conformant_planning
10
10
6
4
360.32
qestos
Connect4
10
9
5
4
1199.3
xb-bid-qsts
Counter
10
10
10
0
58.84
xb-bid-qsts
Debug
10
2
2
0
825.81
rareqs
DFlipFlop
10
10
0
10
0.42
depqbf-v3
dungeon
10
9
0
9
148.52
AIGSolve
evader-pursuer-4x4-logarithmic
7
7
7
0
1.67
depqbf-v1
evader-pursuer-4x4-standard
7
7
7
0
210.29
depqbf-v2
evader-pursuer-6x6-logarithmic
8
6
0
6
278.88
hiqqer1
evader-pursuer-6x6-standard
8
3
0
3
362.93
depqbf-v3
evader-pursuer-8x8-logarithmic
8
5
0
5
434.06
depqbf-v1
FPGA_PLB_FIT_FAST
5
5
4
1
0.27
rareqs
FPGA_PLB_FIT_SLOW
3
3
1
2
0.36
rareqs
fpu
10
10
0
10
5.41
depqbf-v3
Generalized-Tic-Tac-Toe
10
10
1
9
286.53
xb-qsts
HardwareFixpoint
10
9
2
7
364.41
AIGSolve
Impl
10
10
10
0
0
AIGSolve
incrementer-encoder
10
10
1
9
13.81
rareqs
irqlkeapclte
10
10
10
0
166.11
AIGSolve
ISCAS89
8
8
7
1
38.87
qestos
ITC99
7
4
3
1
45.99
ghostq-cegar
jmc_quant_squaring
10
8
4
4
48.8
AIGSolve
k_branch_n
10
9
9
0
12.54
hiqqer3
k_branch_p
10
10
0
10
53.31
hiqqer1
k_d4_n
10
10
10
0
0.57
qsts
k_d4_p
10
10
0
10
0.26
aqua-f3v
k_dum_n
10
10
10
0
0.09
qesto
k_dum_p
10
10
0
10
0.09
rareqs
k_grz_n
10
10
10
0
0.26
qsts
k_grz_p
10
10
0
10
0.25
qesto
k_lin_n
10
10
10
0
3.89
qsts
k_lin_p
10
10
0
10
0.21
qestos
k_path_n
10
10
10
0
0.18
rareqs
k_path_p
10
10
0
10
0.23
qesto
k_ph_n
10
10
10
0
17.92
qsts
k_ph_p
10
6
0
6
244.78
xb-bid-qsts
k_poly_n
10
10
10
0
0.07
qesto
k_poly_p
10
10
0
10
0.08
qesto
k_t4p_n
10
10
10
0
0.49
qesto
k_t4p_p
10
10
0
10
0.38
qestos
LinearBitvectorRankingFunction
10
5
5
0
292.6
xb-bid-qsts
Logn
4
4
0
4
0.86
AIGSolve
mqm
10
10
5
5
109.15
qsts
MutexP
7
7
7
0
0.19
qsts
Planning-CTE
7
7
2
5
182.39
AIGSolve
QBF-Hardness
10
10
1
9
36.39
xb-qsts
qbfeval12
5
5
1
4
0.11
AIGSolve
Qshifter
6
6
6
0
1.62
struqs-10
RankingFunctions
10
10
10
0
0.31
qestos
Reduction-finding
10
9
2
7
49.04
rareqs
Rewriting
10
10
0
10
0.02
qestos
s1196
6
6
6
0
1.07
qsts
s1269
10
5
5
0
138.08
ghostq-plain
s27
4
4
1
3
0
qsts
s298
10
10
6
4
2.22
qsts
s3330
10
6
4
2
291.93
qsts
s386
10
10
5
5
0.93
qsts
s499
10
10
0
10
2.66
qsts
s510
10
10
9
1
11.07
qsts
s641
9
9
0
9
0.74
qsts
s713
10
10
0
10
1.06
qsts
s820
10
10
6
4
3.21
qsts
Sorting_networks
10
10
5
5
256.92
rareqs
SzymanskiP
10
10
0
10
35.87
hiqqer1ldsq
term1
8
8
4
4
1.16
AIGSolve
terminator
10
10
1
9
368.68
AIGSolve
tipdiam
10
9
6
3
356.15
AIGSolve
tipfixpoint
10
10
7
3
46.68
ghostq-plain
ToiletA
10
10
3
7
1.38
rareqs
ToiletC
10
10
1
9
0.8
depqbf-v3
ToiletG
7
7
7
0
0
qesto
trafficlight-controller
10
10
0
10
23.02
rareqs
Tree
10
10
2
8
0
AIGSolve
uclid
3
2
1
1
2.68
ghostq-plain
VonNeumann
10
10
0
10
2.79
depqbf-v3
wmiforward
10
10
10
0
0.17
qestos
z4ml
8
8
4
4
0
AIGSolve
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org