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
Prenex CNF Track
Family
Overall
Time
Reference solver
N
#
S
U
Adder
8
7
5
2
423.69
Caqe-hqspre
amba
4
4
3
1
398.42
Rareqs_2018
arithmetic
10
8
8
0
0
Rareqs_2018
blackbox-01X-QBF
20
20
0
20
35.08
Rareqs_2018
BMC
10
10
7
3
172.48
Rareqs_2018
bomb
10
10
10
0
79.83
depqbf_prefix_opt_qdo
C5315
3
0
0
0
-
-
C6288
5
1
1
0
631.45
GhostQ___plain_pcnf_2019
cycle-sched
7
7
6
1
415.26
Rareqs_2018
Debug
10
7
7
0
2812.09
Caqe-hqspre
disjunctive_decomposition
10
8
7
1
6.74
nanoqbf_bloqqer
driver
6
6
6
0
0
Rareqs_2018
dungeon
10
10
0
10
236.36
nanoqbf_hqspre
evader-pursuer-6x6-logarithmic
2
0
0
0
-
-
evader-pursuer-6x6-standard
5
0
0
0
-
-
evader-pursuer-8x8-logarithmic
3
0
0
0
-
-
formula_add
10
6
6
0
498.28
nanoqbf_bloqqer
fpu
10
10
4
6
177.04
Rareqs_2018
genbuf
2
2
0
2
96.14
Rareqs_2018
genpatch
5
5
3
2
622.63
GhostQ___cegar_pcnf_2019
gttt-4x4_2020
10
10
3
7
727.01
Caqe-bloqqer-qdo
HardwareFixpoint
54
45
12
33
372.82
GhostQ___cegar_pcnf_2019
hwmcc
2
1
1
0
8.35
depqbf_pre_QxQBH
incrementer-encoder
10
10
3
7
120.98
GhostQ___cegar_pcnf_2019
irqlkeapclte
10
10
10
0
869.96
depqbf_pre_QxQBH
ISCAS89
10
10
8
2
3.46
depqbf_prefix_opt_qdo
ITC99
10
7
6
1
89.39
nanoqbf_hqspre
jmc_quant
5
2
1
1
33.43
GhostQ___plain_pcnf_2019
jmc_quant_squaring
5
3
1
2
112.6
Qute_default
k_branch_n
5
5
5
0
580.8
depqbf_pre_QxQBH
k_branch_p
5
5
0
5
2.52
depqbf_prefix_opt_qdo
k_ph_n
5
5
5
0
13.87
nanoqbf_hqspre
k_ph_p
5
1
0
1
134.85
nanoqbf_hqspre
LinearBitvectorRankingFunction
11
8
4
4
230.1
Caqe-hqspre
ltl2aig-comp
3
3
1
2
42.61
Rareqs_2018
LTL2DBA
2
2
2
0
0
Rareqs_2018
LTL2DPA
1
1
1
0
1.17
Rareqs_2018
mqm
10
10
7
3
377.19
Caqe-hqspre
mult-matrix
6
5
5
0
14.42
depqbf_pre_QxQBH
Planning-CTE
40
40
5
35
3972.9
nanoqbf_hqspre
QBF-Hardness
10
10
1
9
461.11
Caqe-bloqqer-qdo
RankingFunctions
10
10
10
0
0
Qute_default
Reduction-finding
55
52
24
28
2491.24
GhostQ___cegar_pcnf_2019
s1269
5
0
0
0
-
-
s3330
3
0
0
0
-
-
s820
2
2
1
1
14.52
GhostQ___plain_pcnf_2019
sketch
10
4
0
4
636.1
Rareqs_2018
Sorting_networks
10
9
2
7
485.27
Caqe-bloqqer-qdo
SzymanskiP
2
2
0
2
87.04
Rareqs_2018
terminator
10
10
1
9
22.2
Qute_rrs
tipdiam
10
8
7
1
204
GhostQ___plain_pcnf_2019
tipfixpoint
10
10
9
1
227.23
GhostQ___plain_pcnf_2019
toy
5
5
5
0
10.22
depqbf_pre_QxQBH
trafficlight-controller
10
10
0
10
13.97
Rareqs_2018
wmiforward
10
10
10
0
1.72
Rareqs_2018
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org