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
prefix-opt-depqbf results solving families - 2017
Family
# Total
# Sat
# Unsat
Time
Abduction
26
1
0
21911.56
Adder
114
0
0
102600
amba
22
0
0
19800
arithmetic
22
3
0
9000.37
blackbox-01X-QBF
133
0
12
54408.14
BMC
98
1
2
65098.83
C432
21
0
2
205.02
C499
31
0
1
22876.11
C5315
57
0
1
40914.72
C6288
76
0
0
68400
C880
60
0
3
27919.87
circuits
84
0
0
75600
conformant_planning
60
0
0
54000
Connect2
1
1
0
14.61
Connect3
2
0
0
1800
Connect4
43
0
1
37800.29
Connect5
2
0
1
904.08
Connect6
3
0
1
1800.36
Connect7
4
0
0
3600
Connect8
2
0
2
3.08
Counter
22
0
0
19800
cycle-sched
24
0
0
21600
Debug
125
0
0
112500
disjunctive_decomposition
23
1
0
16200.05
driver
18
0
1
14401.06
dungeon
115
1
9
86975.31
evader-pursuer-4x4-logarithmic
10
1
0
4.8
evader-pursuer-4x4-standard
65
5
0
28545.52
evader-pursuer-6x6-logarithmic
50
0
2
30467.49
evader-pursuer-6x6-standard
77
0
2
56401.44
evader-pursuer-8x8-logarithmic
51
0
2
32108.6
formula_add
39
3
0
30339.46
fpu
20
0
20
167.97
genbuf
22
0
0
19800
Generalized-Tic-Tac-Toe
32
1
5
8431.79
genpatch
20
0
1
14458
HardwareFixpoint
125
1
0
111600
hwmcc
16
0
2
10821.34
hyperLTL
4
1
1
0.02
incrementer-encoder
55
2
7
30837.18
irqlkeapclte
121
0
0
108900
ISCAS89
7
2
2
3.74
ITC99
57
4
1
33737.22
jmc_quant
6
0
0
5400
jmc_quant_squaring
98
1
0
76784.44
k_branch_n
56
0
0
50400
k_branch_p
85
0
8
354.51
k_ph_p
80
0
0
72000
LinearBitvectorRankingFunction
119
1
0
103599.08
ltl2aig-comp
19
0
0
17100
LTL2DBA
9
0
1
6389.48
LTL2DPA
10
0
0
9000
mqm
34
3
0
1669.7
mult-matrix
24
0
0
21600
Planning-CTE
131
0
4
112797.32
QBF-Hardness
60
0
4
41963.32
qbfeval12
7
2
0
4708.49
RankingFunctions
2
2
0
0.08
Reduction-finding
45
0
0
40500
s1196
15
0
0
13500
s1269
17
0
0
15300
s298
14
0
0
12600
s3330
21
0
0
18900
s499
13
0
0
11700
s510
9
0
0
8100
s641
16
0
0
14400
s713
15
0
0
13500
s820
15
0
0
13500
sketch
16
0
0
14400
Sorting_networks
81
1
0
63111.98
SzymanskiP
25
0
0
22500
terminator
78
0
6
30480.74
tipdiam
85
1
0
72000.35
tipfixpoint
93
2
0
68532.42
toy
14
0
2
9000.58
trafficlight-controller
10
0
10
193.58
uclid
30
0
0
27000
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org