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
iProver-qbf-2017-07-27-v3 results solving families - 2017
Family
# Total
# Sat
# Unsat
Time
Abduction
26
23400
Adder
114
2
88794.36
amba
22
19800
arithmetic
22
4
4691.74
blackbox-01X-QBF
133
7
94075.25
BMC
98
76918.57
C432
21
18900
C499
31
27900
C5315
57
1
42244.08
C6288
76
68400
C880
60
54000
circuits
84
75600
conformant_planning
60
54000
Connect2
1
900
Connect3
2
1800
Connect4
43
1
37801.53
Connect5
2
1
933.53
Connect6
3
1
1804.23
Connect7
4
3600
Connect8
2
2
30.66
Counter
22
1
16399.4
cycle-sched
24
21600
Debug
125
112500
disjunctive_decomposition
23
1
15947.43
driver
18
1
14491.66
dungeon
115
1
14
67630.69
evader-pursuer-4x4-logarithmic
10
1
4726.3
evader-pursuer-4x4-standard
65
58500
evader-pursuer-6x6-logarithmic
50
45000
evader-pursuer-6x6-standard
77
69300
evader-pursuer-8x8-logarithmic
51
45900
formula_add
39
35100
fpu
20
20
512.54
genbuf
22
19800
Generalized-Tic-Tac-Toe
32
28800
genpatch
20
18000
HardwareFixpoint
125
1
104955.08
hwmcc
16
2
9230.6
hyperLTL
4
1
1
0.66
incrementer-encoder
55
2
11
15805.18
irqlkeapclte
121
108900
ISCAS89
7
2
2
534.85
ITC99
57
4
1
32200.73
jmc_quant
6
5400
jmc_quant_squaring
98
88200
k_branch_n
56
50400
k_branch_p
85
76500
k_ph_p
80
72000
LinearBitvectorRankingFunction
119
2
95330.69
ltl2aig-comp
19
17100
LTL2DBA
9
1
6316.22
LTL2DPA
10
1
6438.36
mqm
34
30600
mult-matrix
24
21600
Planning-CTE
131
6
105069.37
QBF-Hardness
60
54000
qbfeval12
7
6300
RankingFunctions
2
1800
Reduction-finding
45
1
35749.03
s1196
15
11568.72
s1269
17
15300
s298
14
12600
s3330
21
18900
s499
13
11700
s510
9
8100
s641
16
14400
s713
15
13500
s820
15
13500
sketch
16
14400
Sorting_networks
81
72900
SzymanskiP
25
10074.34
terminator
78
70200
tipdiam
85
76500
tipfixpoint
93
83700
toy
14
2
9015.1
trafficlight-controller
10
10
868.19
uclid
30
27000
Contact
|
Organization
|
Links
|
Citing QBFLIB