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'18 - Prenex CNF Track
Family
Overall
Time
Reference solver
N
#
S
U
Adder
10
10
10
0
226.37
Qute_opt500
amba
2
2
1
1
191.1
Rareqs_2018
arithmetic
4
4
4
0
12.69
predyndep
blackbox-01X-QBF
20
20
0
20
32.22
Rareqs_2018
BMC
10
10
7
3
176.2
Rareqs_2018
CombinationalEquivalence
20
20
10
10
1214.31
GhostQ-PG_cegar
cycle-sched
4
3
2
1
424.25
Rareqs_2018
Debug
10
7
7
0
2852.22
Caqe-hqspre
disjunctive_decomposition
4
4
3
1
1.97
Caqe-bloqqer
driver
2
2
2
0
0
Caqe-bloqqer
dungeon
21
21
0
21
443.04
Iprover-HQSpre-Bloqqer
formula_add
7
6
6
0
1062.41
Rareqs_2018
fpu
10
10
0
10
12.76
Rareqs_2018
genbuf
3
3
3
0
352.12
Qute_random
Generalized-Tic-Tac-Toe
10
10
3
7
561.8
Caqe-bloqqer
genpatch
5
5
3
2
710.66
GhostQ-PG_cegar
HardwareFixpoint
15
14
1
13
127.67
GhostQ-PG_cegar
hwmcc
2
1
1
0
94.78
Caqe-hqspre
incrementer-encoder
10
10
1
9
15.85
Heretiq-simple
irqlkeapclte
10
10
10
0
194.59
predyndep
ISCAS89
10
10
6
4
3.79
depqbf_prefix_opt_qdo
ITC99
10
8
5
3
221.55
depqbf_pre_QxQBH
jmc_quant_squaring
6
6
6
0
0
Qute_opt500
k_branch_n
6
6
6
0
50.79
predyndep
k_branch_p
8
8
0
8
2.65
depqbf_prefix_opt_qdo
k_ph_p
5
2
0
2
395.9
predyndep
LinearBitvectorRankingFunction
15
10
6
4
880.74
Caqe-hqspre
ltl2aig-comp
2
2
0
2
32.13
Rareqs_2018
LTL2DBA
1
1
1
0
0
Qute_opt500
LTL2DPA
1
1
1
0
1.07
ijtihad
Model_instances
6
5
1
4
59.89
PortfolioDepQBFGhostQRaReQSQute___pf
mqm
10
10
10
0
112.8
Qute_default
mult-matrix
4
2
2
0
1.82
Caqe-hqspre
Planning-CTE
26
26
2
24
2197.71
Iprover-HQSpre-Bloqqer
PositionalGames_gttt
15
13
13
0
449.08
predyndep
PositionalGames_hex
15
10
7
3
3118.54
Caqe-bloqqer
QBF-Hardness
10
10
1
9
377.7
Caqe-bloqqer
Q_2_3
20
18
0
18
989.77
PortfolioDepQBFGhostQRaReQSQute___pf
RankingFunctions
15
15
15
0
0
Qute_default
Reduction-finding
10
7
3
4
827.89
Caqe-bloqqer
Selection-hard
5
5
5
0
192.27
Caqe-hqspre
sketch
10
6
0
6
1346.96
Rareqs_2018
Sorting_networks
10
10
3
7
880.16
Caqe-bloqqer-qdo
SzymanskiP
2
2
0
2
86.3
Caqe-bloqqer
terminator
10
10
1
9
16.53
Caqe-hqspre
tipdiam
10
6
5
1
207.08
GhostQ-PG_plain
tipfixpoint
12
10
9
1
241.91
GhostQ-PG_plain
toy
1
1
1
0
0
Caqe-bloqqer
trafficlight-controller
10
10
0
10
13.38
Heretiq-cube
wgrowing
9
8
8
0
1006.34
Caqe-bloqqer
wmiforward
10
10
10
0
1.69
Rareqs_2018
Contact
|
Organization
|
Links
|
Citing QBFLIB