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'17 - Prenex CNF Track
Family
Overall
Time
Reference solver
N
#
S
U
Abduction
5
2
1
1
638.16
xb-qsts_bqsts2.0
Adder
10
9
7
2
394.37
AIGSolve
amba
4
3
1
2
185.89
rareqs
arithmetic
5
5
5
0
9.46
dynQBF-bloqqer-hqspre
blackbox-01X-QBF
20
20
0
20
32.52
rareqs
BMC
13
6
4
2
156.08
rareqs
C432
2
2
0
2
0.28
QELL_unit
C499
3
3
0
3
33.27
AIGSolve
C5315
5
2
1
1
4.48
GhostQ-PG_plain
C6288
7
2
2
0
27.79
rev_qfun0.1
C880
6
6
0
6
596
GhostQ-PG_plain
circuits
14
3
3
0
99.49
qbfrelay
conformant_planning
10
8
3
5
1384.16
QELL_unit
Connect2
1
1
1
0
9.56
caqe_2017_v1
Connect3
1
0
0
0
-
-
Connect4
8
1
0
1
0.05
AIGSolve
Connect5
2
2
0
2
130.53
xb-qsts_bqsts2.0
Connect6
2
1
0
1
0.05
qesto
Connect7
2
0
0
0
-
-
Connect8
2
2
0
2
0.36
AIGSolve
Counter
5
3
3
0
95.06
AIGSolve
cycle-sched
4
3
2
1
392.39
rareqs
Debug
14
6
6
0
1987.14
Qute_random
disjunctive_decomposition
5
4
3
1
58.51
rareqs
driver
4
4
2
2
0.37
rev_qfun0.1
dungeon
26
26
1
25
493.64
HQSpre_solver
evader-pursuer-4x4-logarithmic
1
1
1
0
0.48
prefix-opt-depqbf
evader-pursuer-4x4-standard
7
7
7
0
20.28
HQSpre_solver
evader-pursuer-6x6-logarithmic
5
3
0
3
1102.86
qbfrelay-limited-depqbf
evader-pursuer-6x6-standard
8
2
0
2
187.68
prefix-opt-depqbf
evader-pursuer-8x8-logarithmic
5
2
0
2
420.86
prefix-opt-depqbf
formula_add
12
8
8
0
1010.32
rareqs
fpu
20
20
0
20
23.38
rev_qfun0.1
genbuf
4
3
1
2
893.04
AIGSolve
Generalized-Tic-Tac-Toe
7
7
1
6
159.81
xb-qsts_xbqsts1.0
genpatch
5
5
3
2
110.24
rev_qfun0.1
HardwareFixpoint
26
16
2
14
126.86
GhostQ-PG_cegar
hwmcc
4
4
2
2
319.03
qbfrelay
hyperLTL
2
2
1
1
0
qesto
incrementer-encoder
13
13
2
11
32.75
caqe_2017_v1
irqlkeapclte
10
10
10
0
119.69
dynQBF-bloqqer-hqspre
ISCAS89
4
4
2
2
2.27
prefix-opt-depqbf
ITC99
9
8
7
1
1047.7
rev_qfun0.1
jmc_quant
1
0
0
0
-
-
jmc_quant_squaring
8
6
3
3
16.73
AIGSolve
k_branch_n
6
6
6
0
516.17
HQSpre_solver
k_branch_p
8
8
0
8
37.15
prefix-opt-depqbf
k_ph_p
10
5
0
5
673.72
dynQBF-bloqqer-hqspre
LinearBitvectorRankingFunction
23
7
4
3
579.78
caqe_2017_v3
ltl2aig-comp
4
2
0
2
28.06
AIGSolve
LTL2DBA
2
2
1
1
0.29
qesto
LTL2DPA
2
2
1
1
1.68
qesto
mqm
3
3
3
0
47.87
caqe_2017_v2
mult-matrix
4
4
2
2
56.33
AIGSolve
Planning-CTE
29
29
2
27
614.39
QELL_default
QBF-Hardness
10
10
1
9
153.9
xb-qsts_bqsts2.0
qbfeval12
3
3
3
0
14.03
rev_qfun0.1
RankingFunctions
2
2
2
0
0.08
prefix-opt-depqbf
Reduction-finding
6
5
2
3
163.5
rareqs
s1196
2
2
0
2
145.4
GhostQ-PG_plain
s1269
2
1
1
0
3.33
GhostQ-PG_plain
s298
2
2
1
1
9.76
QELL_unit
s3330
2
1
1
0
2.92
QELL_unit
s499
2
2
1
1
2.35
QELL_unit
s510
2
2
2
0
36.64
QELL_default
s641
2
2
1
1
10.49
GhostQ-PG_plain
s713
2
2
0
2
51.37
GhostQ-PG_plain
s820
2
2
1
1
3.4
QELL_default
sketch
5
2
0
2
924.77
caqe_2017_v3
Sorting_networks
6
6
2
4
251.39
rareqs
SzymanskiP
2
2
0
2
42.38
AIGSolve
terminator
9
9
1
8
29.54
Qute_default
tipdiam
10
8
3
5
463.99
AIGSolve
tipfixpoint
13
10
9
1
237.45
GhostQ-PG_plain
toy
4
4
2
2
0.55
rareqs
trafficlight-controller
10
10
0
10
13.01
rareqs
uclid
3
2
1
1
2.89
GhostQ-PG_plain
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org