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'05
Family
Overall
Time
Reference solver
N
#
S
U
Adder
32
20
12
8
1221.49
QMRes
Blocks
13
13
4
9
37.61
QUANTOR
C432
8
6
3
3
799.03
semprop
C499
8
6
2
4
20.48
QChaffLearn
C5315
8
4
2
2
0.42
QUANTOR
C6288
8
1
1
0
1.43
skizzo_v0.5
C880
8
6
2
4
156.64
QChaffLearn
Chain
12
12
12
0
0.33
semprop
comp
8
8
4
4
0.09
QUANTOR
Connect4
60
48
1
47
2336.38
GRL
Counter
24
24
0
24
3
QChaffLearn
CounterFactual
1080
445
223
222
12395.9
WalkQSAT
DFlipFlop
10
10
0
10
2.75
sSolve
evader-pursuer-4x4-logarithmic
7
7
7
0
2.51
WalkQSAT
evader-pursuer-4x4-standard
7
1
1
0
5.78
skizzo_v0.5
evader-pursuer-6x6-logarithmic
8
4
0
4
492.33
QChaffLearn
evader-pursuer-6x6-standard
8
0
0
0
-
-
evader-pursuer-8x8-logarithmic
8
4
0
4
94.27
skizzo_v0.5
FPGA_PLB_FIT_FAST
5
5
4
1
0.81
skizzo_v0.4
FPGA_PLB_FIT_SLOW
3
3
1
2
4.18
skizzo_v0.4
horn
156
156
79
77
3.33
QbflHR
Impl
10
10
10
0
0.02
GRL
jmc_quant
10
4
2
2
61.53
QMRes
jmc_quant_squaring
10
3
2
1
11.37
QMRes
k_branch_n
6
2
2
0
46.29
semprop
k_branch_p
6
6
0
6
24.28
skizzo_v0.5
k_d4_n
6
6
6
0
36.8
QMRes
k_d4_p
6
6
0
6
1.02
skizzo_v0.5
k_dum_n
6
6
6
0
0.13
QUANTOR
k_dum_p
6
6
0
6
0.14
QUANTOR
k_grz_n
6
6
6
0
14.64
QUANTOR
k_grz_p
6
6
0
6
6.74
QUANTOR
k_lin_n
6
6
6
0
11.84
QUANTOR
k_lin_p
6
6
0
6
0.69
skizzo_v0.4
k_path_n
6
6
6
0
0.28
QUANTOR
k_path_p
6
6
0
6
0.26
QUANTOR
k_ph_n
6
6
3
3
20.85
QChaffLearn
k_ph_p
6
6
0
6
50.07
QChaffLearn
k_poly_n
6
6
6
0
0.11
QUANTOR
k_poly_p
6
6
0
6
0.08
sSolve
k_t4p_n
6
6
6
0
86.77
QMRes
k_t4p_p
6
6
0
6
8.69
skizzo_v0.5
Logn
2
2
0
2
0.85
yQuaffle
mA-t2-1qbf-5cnf-160var-1280cl
10
10
10
0
0.01
qbfbdd
mA-t2-1qbf-5cnf-160var-2560cl
10
10
10
0
2.29
sSolve
mA-t2-1qbf-5cnf-160var-320cl
10
10
10
0
0.01
GRL
mA-t2-1qbf-5cnf-160var-5120cl
10
0
0
0
-
-
mA-t2-1qbf-5cnf-160var-640cl
10
10
10
0
0.03
qbfbdd
mA-t2-1qbf-5cnf-20var-160cl
10
10
10
0
0.01
QChaffLearn
mA-t2-1qbf-5cnf-20var-320cl
10
10
10
0
0.01
yQuaffle
mA-t2-1qbf-5cnf-20var-40cl
10
10
10
0
0.01
GRL
mA-t2-1qbf-5cnf-20var-640cl
10
10
0
10
0.02
qbfbdd
mA-t2-1qbf-5cnf-20var-80cl
10
10
10
0
0.01
QbflHR
mA-t2-1qbf-5cnf-40var-1280cl
10
10
0
10
0.7
sSolve
mA-t2-1qbf-5cnf-40var-160cl
10
10
10
0
0.01
qbfbdd
mA-t2-1qbf-5cnf-40var-320cl
10
10
10
0
0.03
GRL
mA-t2-1qbf-5cnf-40var-640cl
10
10
10
0
0.07
QbflHR
mA-t2-1qbf-5cnf-40var-80cl
10
10
10
0
0.01
QUANTOR
mA-t2-1qbf-5cnf-80var-1280cl
10
10
10
0
0.12
sSolve
mA-t2-1qbf-5cnf-80var-160cl
10
10
10
0
0.02
qbfbdd
mA-t2-1qbf-5cnf-80var-2560cl
10
10
0
10
220.18
sSolve
mA-t2-1qbf-5cnf-80var-320cl
10
10
10
0
0.01
qbfbdd
mA-t2-1qbf-5cnf-80var-640cl
10
10
10
0
0.01
sSolve
mA-t2-2qbf-5cnf-160var-1280cl
10
10
0
10
1567.1
skizzo_v0.4
mA-t2-2qbf-5cnf-160var-2560cl
10
10
0
10
0.15
semprop
mA-t2-2qbf-5cnf-160var-320cl
10
10
10
0
0.03
sSolve
mA-t2-2qbf-5cnf-160var-5120cl
10
10
0
10
0.26
semprop
mA-t2-2qbf-5cnf-160var-640cl
10
8
0
8
1132.83
skizzo_v0.4
mA-t2-2qbf-5cnf-20var-160cl
10
10
0
10
0.06
sSolve
mA-t2-2qbf-5cnf-20var-320cl
10
10
0
10
0.02
sSolve
mA-t2-2qbf-5cnf-20var-40cl
10
10
10
0
0.01
GRL
mA-t2-2qbf-5cnf-20var-640cl
10
10
0
10
0.02
qbfbdd
mA-t2-2qbf-5cnf-20var-80cl
10
10
10
0
0.04
sSolve
mA-t2-2qbf-5cnf-40var-1280cl
10
10
0
10
0.06
qbfbdd
mA-t2-2qbf-5cnf-40var-160cl
10
10
6
4
0.29
sSolve
mA-t2-2qbf-5cnf-40var-320cl
10
10
0
10
0.1
sSolve
mA-t2-2qbf-5cnf-40var-640cl
10
10
0
10
0.07
QChaffLearn
mA-t2-2qbf-5cnf-40var-80cl
10
10
10
0
0.03
QUANTOR
mA-t2-2qbf-5cnf-80var-1280cl
10
10
0
10
0.11
sSolve
mA-t2-2qbf-5cnf-80var-160cl
10
10
10
0
0.03
sSolve
mA-t2-2qbf-5cnf-80var-2560cl
10
10
0
10
0.07
qbfbdd
mA-t2-2qbf-5cnf-80var-320cl
10
7
2
5
616.29
sSolve
mA-t2-2qbf-5cnf-80var-640cl
10
10
0
10
3.11
sSolve
mA-t2-3qbf-5cnf-160var-1280cl
10
9
9
0
11.47
QbflHR
mA-t2-3qbf-5cnf-160var-2560cl
10
10
0
10
0.2
sSolve
mA-t2-3qbf-5cnf-160var-320cl
10
10
10
0
0.01
QUANTOR
mA-t2-3qbf-5cnf-160var-5120cl
10
10
0
10
0.23
semprop
mA-t2-3qbf-5cnf-160var-640cl
10
10
10
0
0.06
QbflHR
mA-t2-3qbf-5cnf-20var-160cl
10
10
10
0
0.05
sSolve
mA-t2-3qbf-5cnf-20var-320cl
10
10
0
10
0.06
sSolve
mA-t2-3qbf-5cnf-20var-40cl
10
10
10
0
0.02
QChaffLearn
mA-t2-3qbf-5cnf-20var-640cl
10
10
0
10
0.02
semprop
mA-t2-3qbf-5cnf-20var-80cl
10
10
10
0
0.01
GRL
mA-t2-3qbf-5cnf-40var-1280cl
10
10
0
10
0.1
yQuaffle
mA-t2-3qbf-5cnf-40var-160cl
10
10
10
0
0
QChaffLearn
mA-t2-3qbf-5cnf-40var-320cl
10
10
9
1
0.44
semprop
mA-t2-3qbf-5cnf-40var-640cl
10
10
0
10
0.02
sSolve
mA-t2-3qbf-5cnf-40var-80cl
10
10
10
0
0.01
sSolve
mA-t2-3qbf-5cnf-80var-1280cl
10
10
0
10
0.09
sSolve
mA-t2-3qbf-5cnf-80var-160cl
10
10
10
0
0.01
QUANTOR
mA-t2-3qbf-5cnf-80var-2560cl
10
10
0
10
0.1
sSolve
mA-t2-3qbf-5cnf-80var-320cl
10
10
10
0
0.04
sSolve
mA-t2-3qbf-5cnf-80var-640cl
10
10
10
0
0.08
QbflHR
mA-t2-4qbf-5cnf-160var-1280cl
10
10
0
10
623.02
skizzo_v0.4
mA-t2-4qbf-5cnf-160var-2560cl
10
10
0
10
0.31
sSolve
mA-t2-4qbf-5cnf-160var-320cl
10
10
10
0
0.03
semprop
mA-t2-4qbf-5cnf-160var-5120cl
10
10
0
10
0.29
semprop
mA-t2-4qbf-5cnf-160var-640cl
10
10
10
0
0.04
sSolve
mA-t2-4qbf-5cnf-20var-160cl
10
10
2
8
0.32
sSolve
mA-t2-4qbf-5cnf-20var-320cl
10
10
0
10
0.03
sSolve
mA-t2-4qbf-5cnf-20var-40cl
10
10
10
0
0.01
semprop
mA-t2-4qbf-5cnf-20var-640cl
10
10
0
10
0.01
sSolve
mA-t2-4qbf-5cnf-20var-80cl
10
10
10
0
0.04
sSolve
mA-t2-4qbf-5cnf-40var-1280cl
10
10
0
10
0.1
sSolve
mA-t2-4qbf-5cnf-40var-160cl
10
10
10
0
0.02
sSolve
mA-t2-4qbf-5cnf-40var-320cl
10
10
0
10
325.55
sSolve
mA-t2-4qbf-5cnf-40var-640cl
10
10
0
10
0.05
sSolve
mA-t2-4qbf-5cnf-40var-80cl
10
10
10
0
0.01
QUANTOR
mA-t2-4qbf-5cnf-80var-1280cl
10
10
0
10
0.11
sSolve
mA-t2-4qbf-5cnf-80var-160cl
10
10
10
0
0.01
QChaffLearn
mA-t2-4qbf-5cnf-80var-2560cl
10
10
0
10
0.14
semprop
mA-t2-4qbf-5cnf-80var-320cl
10
10
10
0
0.04
sSolve
mA-t2-4qbf-5cnf-80var-640cl
10
10
0
10
1745.36
skizzo_v0.4
mA-t2-5qbf-5cnf-160var-1280cl
10
10
10
0
0.11
QbflHR
mA-t2-5qbf-5cnf-160var-2560cl
10
10
0
10
0.46
sSolve
mA-t2-5qbf-5cnf-160var-320cl
10
10
10
0
0.05
semprop
mA-t2-5qbf-5cnf-160var-5120cl
10
10
0
10
0.38
sSolve
mA-t2-5qbf-5cnf-160var-640cl
10
10
10
0
0.03
QbflHR
mA-t2-5qbf-5cnf-20var-160cl
10
10
10
0
0.02
sSolve
mA-t2-5qbf-5cnf-20var-320cl
10
10
0
10
0.08
sSolve
mA-t2-5qbf-5cnf-20var-40cl
10
10
10
0
0.01
GRL
mA-t2-5qbf-5cnf-20var-640cl
10
10
0
10
0.06
QChaffLearn
mA-t2-5qbf-5cnf-20var-80cl
10
10
10
0
0.02
GRL
mA-t2-5qbf-5cnf-40var-1280cl
10
10
0
10
0.08
WalkQSAT
mA-t2-5qbf-5cnf-40var-160cl
10
10
10
0
0.02
QChaffLearn
mA-t2-5qbf-5cnf-40var-320cl
10
10
10
0
0.02
QbflHR
mA-t2-5qbf-5cnf-40var-640cl
10
10
0
10
0.05
sSolve
mA-t2-5qbf-5cnf-40var-80cl
10
10
10
0
0.02
GRL
mA-t2-5qbf-5cnf-80var-1280cl
10
10
0
10
0.14
sSolve
mA-t2-5qbf-5cnf-80var-160cl
10
10
10
0
0.03
QUANTOR
mA-t2-5qbf-5cnf-80var-2560cl
10
10
0
10
0.14
sSolve
mA-t2-5qbf-5cnf-80var-320cl
10
10
10
0
0.02
QbflHR
mA-t2-5qbf-5cnf-80var-640cl
10
10
10
0
0.09
QbflHR
mA-t2-6qbf-5cnf-160var-1280cl
10
4
4
0
1.07
sSolve
mA-t2-6qbf-5cnf-160var-2560cl
10
10
0
10
0.49
sSolve
mA-t2-6qbf-5cnf-160var-320cl
10
10
10
0
0.01
QUANTOR
mA-t2-6qbf-5cnf-160var-5120cl
10
10
0
10
0.23
semprop
mA-t2-6qbf-5cnf-160var-640cl
10
10
10
0
0.03
sSolve
mA-t2-6qbf-5cnf-20var-160cl
10
10
9
1
0.05
sSolve
mA-t2-6qbf-5cnf-20var-320cl
10
10
0
10
0.08
sSolve
mA-t2-6qbf-5cnf-20var-40cl
10
10
10
0
0
QUANTOR
mA-t2-6qbf-5cnf-20var-640cl
10
10
0
10
0.02
sSolve
mA-t2-6qbf-5cnf-20var-80cl
10
10
10
0
0
GRL
mA-t2-6qbf-5cnf-40var-1280cl
10
10
0
10
0.09
semprop
mA-t2-6qbf-5cnf-40var-160cl
10
10
10
0
0.02
GRL
mA-t2-6qbf-5cnf-40var-320cl
10
9
8
1
11.7
sSolve
mA-t2-6qbf-5cnf-40var-640cl
10
10
0
10
0.13
sSolve
mA-t2-6qbf-5cnf-40var-80cl
10
10
10
0
0.01
QUANTOR
mA-t2-6qbf-5cnf-80var-1280cl
10
10
0
10
0.14
sSolve
mA-t2-6qbf-5cnf-80var-160cl
10
10
10
0
0.03
QUANTOR
mA-t2-6qbf-5cnf-80var-2560cl
10
10
0
10
0.13
semprop
mA-t2-6qbf-5cnf-80var-320cl
10
10
10
0
0.02
QUANTOR
mA-t2-6qbf-5cnf-80var-640cl
10
8
7
1
0.78
sSolve
MutexP
7
7
7
0
0.09
sSolve
Qshifter
6
6
6
0
5.19
skizzo_v0.4
renHorn
84
84
56
28
2.08
QbflHR
RobotsD2
30
25
25
0
2355.03
qbfbdd
RobotsD3
30
26
21
5
1898.81
GRL
RobotsD4
30
24
20
4
1481.23
GRL
RobotsD5
30
25
21
4
1875.77
GRL
s1196
2
0
0
0
-
-
s1269
5
0
0
0
-
-
s27
4
4
1
3
0.47
QUANTOR
s298
6
2
2
0
25.31
skizzo_v0.4
s3330
5
0
0
0
-
-
s386
4
1
1
0
3.56
skizzo_v0.5
s499
6
2
2
0
62.73
skizzo_v0.5
s510
7
1
1
0
1.13
skizzo_v0.4
s641
4
0
0
0
-
-
s713
4
1
1
0
17.47
skizzo_v0.4
s820
5
1
1
0
32.5
skizzo_v0.5
SzymanskiP
12
12
0
12
312.89
GRL
term1
8
7
3
4
3.69
QChaffLearn
Toilet
8
8
5
3
0.62
QChaffLearn
ToiletA
18
18
8
10
33.07
skizzo_v0.4
ToiletC
20
20
11
9
2.82
GRL
Tree
14
14
5
9
0.04
QUANTOR
uclid
3
1
0
1
0.3
QbflHR
VonNeumann
10
10
0
10
5.45
QbflHR
z4ml
8
8
4
4
0.01
QbflHR
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org