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'06
Family
Overall
Time
Reference solver
N
#
S
U
Adder
16
10
10
0
4865.62
sKizzo-0.9-std
ASP_Program_Inclusion
40
40
0
40
113.11
semprop
blackbox_design
28
28
27
1
19.98
qube5.0
Blocks
11
11
4
7
8.31
sKizzo-0.9-grn
C432
4
3
1
2
779.9
semprop
C499
3
3
1
2
18.15
SQBF
C5315
4
4
2
2
0.42
QUANTOR
C6288
1
1
1
0
0.64
sKizzo-0.9-grn
C880
2
2
2
0
7.13
semprop
Chain
4
4
4
0
0.13
SQBF
comp
2
2
0
2
0.02
SQBF
Connect4
13
13
0
13
4.93
preQuantor
Counter
5
5
5
0
7.99
sKizzo-0.9-std
CounterFactual
400
355
201
154
57431.1
sSolve
evader-pursuer-4x4-logarithmic
4
4
4
0
1.62
Quaffle
evader-pursuer-6x6-logarithmic
2
2
0
2
14.98
sKizzo-0.9-grn
evader-pursuer-8x8-logarithmic
4
4
0
4
5.6
sKizzo-0.9-grn
FPGA_PLB_FIT_FAST
3
3
3
0
0.85
yQuaffle
FPGA_PLB_FIT_SLOW
3
3
1
2
5.96
2clsQ
jmc_quant
4
2
2
0
1443.91
ssolve-ut
k_branch_n
2
2
0
2
0.03
QUANTOR_hc
k_branch_p
3
3
0
3
0.16
QUANTOR_hc
k_d4_n
6
6
0
6
0.11
QUANTOR_hc
k_d4_p
5
5
0
5
0.06
QUANTOR_hc
k_dum_n
5
5
0
5
0.05
QUANTOR_hc
k_dum_p
4
4
0
4
0.03
QUANTOR_hc
k_grz_n
5
5
0
5
0.04
QUANTOR_hc
k_grz_p
6
6
0
6
0.08
QUANTOR_hc
k_lin_n
6
6
0
6
5.44
QUANTOR_hc
k_lin_p
5
5
0
5
0.11
QUANTOR_hc
k_path_n
5
5
0
5
0.07
QUANTOR_hc
k_path_p
5
5
0
5
0.09
QUANTOR_hc
k_ph_n
3
3
3
0
5.52
qube5.0
k_ph_p
1
1
0
1
0.03
QUANTOR_hc
k_poly_n
6
6
0
6
0.04
QUANTOR_hc
k_poly_p
3
3
0
3
0.05
QUANTOR
k_t4p_n
6
6
0
6
0.14
QUANTOR_hc
k_t4p_p
6
6
0
6
0.1
QUANTOR_hc
Logn
2
2
0
2
1
yQuaffle
mA-t2-1qbf-5cnf-160var-2560cl
10
10
10
0
13.17
sSolve
mA-t2-1qbf-5cnf-80var-2560cl
10
10
0
10
398.64
ssolve-ut
mA-t2-2qbf-5cnf-160var-2560cl
10
10
0
10
0.17
semprop
mA-t2-2qbf-5cnf-160var-320cl
10
10
10
0
1.75
sSolve
mA-t2-2qbf-5cnf-160var-5120cl
10
10
0
10
0.22
semprop
mA-t2-2qbf-5cnf-40var-160cl
10
10
6
4
2.04
ssolve-ut
mA-t2-2qbf-5cnf-40var-320cl
10
10
0
10
1.88
ssolve+ut
mA-t2-2qbf-5cnf-40var-640cl
10
10
0
10
0.05
semprop
mA-t2-2qbf-5cnf-80var-1280cl
10
10
0
10
0.09
semprop
mA-t2-2qbf-5cnf-80var-320cl
10
10
4
6
5145.92
ssolve-ut
mA-t2-2qbf-5cnf-80var-640cl
10
10
0
10
3.84
ssolve+ut
mA-t2-3qbf-5cnf-160var-2560cl
10
10
0
10
1.86
ssolve-ut
mA-t2-3qbf-5cnf-160var-640cl
10
10
10
0
0.05
semprop
mA-t2-3qbf-5cnf-20var-160cl
10
10
10
0
0.08
semprop
mA-t2-3qbf-5cnf-20var-320cl
10
10
0
10
0.14
semprop
mA-t2-3qbf-5cnf-40var-320cl
10
10
9
1
0.44
semprop
mA-t2-3qbf-5cnf-40var-640cl
10
10
0
10
0.24
semprop
mA-t2-3qbf-5cnf-80var-1280cl
10
10
0
10
2.07
ssolve-ut
mA-t2-3qbf-5cnf-80var-2560cl
10
10
0
10
0.1
2clsQ
mA-t2-3qbf-5cnf-80var-320cl
10
10
10
0
0.04
semprop
mA-t2-4qbf-5cnf-160var-2560cl
10
10
0
10
1.01
qube3.0
mA-t2-4qbf-5cnf-160var-5120cl
10
10
0
10
0.27
semprop
mA-t2-4qbf-5cnf-160var-640cl
10
10
10
0
1.84
ssolve+ut
mA-t2-4qbf-5cnf-20var-160cl
10
10
2
8
1.55
ssolve-ut
mA-t2-4qbf-5cnf-20var-320cl
10
10
0
10
0.09
semprop
mA-t2-4qbf-5cnf-20var-640cl
10
10
0
10
0.06
semprop
mA-t2-4qbf-5cnf-40var-1280cl
10
10
0
10
0.09
WalkQSAT
mA-t2-4qbf-5cnf-40var-320cl
10
10
0
10
6.49
ssolve-ut
mA-t2-4qbf-5cnf-40var-640cl
10
10
0
10
0.1
semprop
mA-t2-4qbf-5cnf-80var-1280cl
10
10
0
10
0.15
semprop
mA-t2-4qbf-5cnf-80var-2560cl
10
10
0
10
0.13
semprop
mA-t2-4qbf-5cnf-80var-320cl
10
10
10
0
1.67
sSolve
mA-t2-5qbf-5cnf-160var-2560cl
10
10
0
10
2.26
ssolve-ut
mA-t2-5qbf-5cnf-160var-5120cl
10
10
0
10
0.45
yQuaffle
mA-t2-5qbf-5cnf-160var-640cl
10
10
10
0
0.04
sKizzo-0.9-grn
mA-t2-5qbf-5cnf-20var-320cl
10
10
0
10
0.19
semprop
mA-t2-5qbf-5cnf-20var-640cl
10
10
0
10
0.05
semprop
mA-t2-5qbf-5cnf-40var-1280cl
10
10
0
10
0.09
semprop
mA-t2-5qbf-5cnf-40var-320cl
10
10
10
0
0.07
Qbfl
mA-t2-5qbf-5cnf-40var-640cl
10
10
0
10
0.32
semprop
mA-t2-5qbf-5cnf-80var-1280cl
10
10
0
10
1.84
ssolve-ut
mA-t2-5qbf-5cnf-80var-2560cl
10
10
0
10
0.23
yQuaffle
mA-t2-5qbf-5cnf-80var-640cl
10
10
10
0
0.1
Qbfl
mA-t2-6qbf-5cnf-160var-2560cl
10
10
0
10
2.04
sSolve
mA-t2-6qbf-5cnf-160var-5120cl
10
10
0
10
0.26
semprop
mA-t2-6qbf-5cnf-160var-640cl
10
10
10
0
0.04
semprop
mA-t2-6qbf-5cnf-20var-160cl
10
10
9
1
0.65
qube3.0
mA-t2-6qbf-5cnf-20var-320cl
10
10
0
10
0.18
semprop
mA-t2-6qbf-5cnf-20var-640cl
10
10
0
10
0.06
semprop
mA-t2-6qbf-5cnf-40var-1280cl
10
10
0
10
0.11
semprop
mA-t2-6qbf-5cnf-40var-320cl
10
10
9
1
669
sSolve
mA-t2-6qbf-5cnf-40var-640cl
10
10
0
10
0.48
semprop
mA-t2-6qbf-5cnf-80var-1280cl
10
10
0
10
1.67
ssolve-ut
mA-t2-6qbf-5cnf-80var-2560cl
10
10
0
10
0.15
semprop
mA-t2-6qbf-5cnf-80var-640cl
10
10
8
2
1770.01
sSolve
MutexP
4
4
4
0
0.27
sKizzo-0.9-grn
Qq2k1k4v40v40m16
10
10
5
5
0.01
2clsQ
Qq2k1k4v40v40m2
10
10
10
0
0.01
QUANTOR
Qq2k1k4v40v40m32
10
10
0
10
0.02
GRL
Qq2k1k4v40v40m4
10
10
9
1
0.01
sKizzo-0.9-grn
Qq2k1k4v40v40m8
10
10
8
2
0
QUANTOR
Qq2k1k4v80v80m16
10
10
7
3
0.01
sKizzo-0.9-abs
Qq2k1k4v80v80m2
10
10
10
0
0
Quaffle
Qq2k1k4v80v80m32
10
10
2
8
0.01
sKizzo-0.9-grn
Qq2k1k4v80v80m4
10
10
10
0
0.02
QUANTOR
Qq2k1k4v80v80m8
10
10
10
0
0.01
GRL
Qq2k2k3v40v40m16
10
10
10
0
0
sKizzo-0.9-abs
Qq2k2k3v40v40m2
10
10
10
0
0.01
sKizzo-0.9-std
Qq2k2k3v40v40m32
10
10
10
0
0.02
QUANTOR
Qq2k2k3v40v40m4
10
10
10
0
0
GRL
Qq2k2k3v40v40m8
10
10
10
0
0.01
sKizzo-0.9-abs
Qq2k2k3v80v80m16
10
10
10
0
0.02
GRL
Qq2k2k3v80v80m2
10
10
10
0
0.02
GRL
Qq2k2k3v80v80m32
10
10
10
0
0.01
GRL
Qq2k2k3v80v80m4
10
10
10
0
0.01
QUANTOR
Qq2k2k3v80v80m8
10
10
10
0
0.02
GRL
Qq2k3k2v40v40m16
10
10
10
0
0.01
sKizzo-0.9-std
Qq2k3k2v40v40m2
10
10
10
0
0.01
sKizzo-0.9-abs
Qq2k3k2v40v40m32
10
10
10
0
0.01
QUANTOR
Qq2k3k2v40v40m4
10
10
10
0
0
GRL
Qq2k3k2v40v40m8
10
10
10
0
0
2clsQ
Qq2k3k2v80v80m16
10
10
10
0
0
GRL
Qq2k3k2v80v80m2
10
10
10
0
0
sKizzo-0.9-abs
Qq2k3k2v80v80m32
10
10
10
0
0.01
semprop
Qq2k3k2v80v80m4
10
10
10
0
0
WalkQSAT
Qq2k3k2v80v80m8
10
10
10
0
0.01
QUANTOR
Qq3k1k1k3v40v40v40m16
10
10
10
0
0.01
sKizzo-0.9-std
Qq3k1k1k3v40v40v40m2
10
10
10
0
0.01
GRL
Qq3k1k1k3v40v40v40m32
10
10
10
0
0.01
Qbfl
Qq3k1k1k3v40v40v40m4
10
10
10
0
0
sKizzo-0.9-abs
Qq3k1k1k3v40v40v40m8
10
10
10
0
0.01
sKizzo-0.9-std
Qq3k1k1k3v80v80v80m16
10
10
10
0
0.01
sKizzo-0.9-abs
Qq3k1k1k3v80v80v80m2
10
10
10
0
0
sKizzo-0.9-std
Qq3k1k1k3v80v80v80m32
10
10
10
0
0
sKizzo-0.9-abs
Qq3k1k1k3v80v80v80m4
10
10
10
0
0.01
sKizzo-0.9-grn
Qq3k1k1k3v80v80v80m8
10
10
10
0
0
sKizzo-0.9-grn
Qq3k1k2k2v40v40v40m16
10
10
10
0
0.01
QUANTOR
Qq3k1k2k2v40v40v40m2
10
10
10
0
0.02
QUANTOR
Qq3k1k2k2v40v40v40m32
10
10
10
0
0
QUANTOR_hc
Qq3k1k2k2v40v40v40m4
10
10
10
0
0.01
WalkQSAT
Qq3k1k2k2v40v40v40m8
10
10
10
0
0.01
GRL
Qq3k1k2k2v80v80v80m16
10
10
10
0
0
sKizzo-0.9-abs
Qq3k1k2k2v80v80v80m2
10
10
10
0
0
sKizzo-0.9-grn
Qq3k1k2k2v80v80v80m32
10
10
10
0
0.02
QUANTOR
Qq3k1k2k2v80v80v80m4
10
10
10
0
0.01
sKizzo-0.9-std
Qq3k1k2k2v80v80v80m8
10
10
10
0
0.01
GRL
Qq3k1k3k1v40v40v40m16
10
10
10
0
0.02
QUANTOR
Qq3k1k3k1v40v40v40m2
10
10
10
0
0.01
QUANTOR
Qq3k1k3k1v40v40v40m32
10
10
10
0
0.01
QUANTOR
Qq3k1k3k1v40v40v40m4
10
10
10
0
0
semprop
Qq3k1k3k1v40v40v40m8
10
10
10
0
0.01
QUANTOR
Qq3k1k3k1v80v80v80m16
10
10
10
0
0.01
WalkQSAT
Qq3k1k3k1v80v80v80m2
10
10
10
0
0
sKizzo-0.9-std
Qq3k1k3k1v80v80v80m32
10
10
10
0
0.01
sKizzo-0.9-abs
Qq3k1k3k1v80v80v80m4
10
10
10
0
0.01
2clsQ
Qq3k1k3k1v80v80v80m8
10
10
10
0
0
2clsQ
Qq3k2k1k2v40v40v40m16
10
10
10
0
0
sKizzo-0.9-grn
Qq3k2k1k2v40v40v40m2
10
10
10
0
0.02
sKizzo-0.9-abs
Qq3k2k1k2v40v40v40m32
10
10
10
0
0.01
QUANTOR
Qq3k2k1k2v40v40v40m4
10
10
10
0
0
QUANTOR
Qq3k2k1k2v40v40v40m8
10
10
10
0
0.02
GRL
Qq3k2k1k2v80v80v80m16
10
10
10
0
0.01
QUANTOR_hc
Qq3k2k1k2v80v80v80m2
10
10
10
0
0.02
QUANTOR
Qq3k2k1k2v80v80v80m32
10
10
10
0
0.01
sKizzo-0.9-abs
Qq3k2k1k2v80v80v80m4
10
10
10
0
0.01
QUANTOR
Qq3k2k1k2v80v80v80m8
10
10
10
0
0.01
QUANTOR
Qq3k2k2k1v40v40v40m16
10
10
10
0
0.02
GRL
Qq3k2k2k1v40v40v40m2
10
10
10
0
0.01
sKizzo-0.9-std
Qq3k2k2k1v40v40v40m32
10
10
10
0
0.01
sKizzo-0.9-std
Qq3k2k2k1v40v40v40m4
10
10
10
0
0.01
SQBF
Qq3k2k2k1v40v40v40m8
10
10
10
0
0.01
GRL
Qq3k2k2k1v80v80v80m16
10
10
10
0
0.01
GRL
Qq3k2k2k1v80v80v80m2
10
10
10
0
0
GRL
Qq3k2k2k1v80v80v80m32
10
10
10
0
0.01
2clsQ
Qq3k2k2k1v80v80v80m4
10
10
10
0
0.01
GRL
Qq3k2k2k1v80v80v80m8
10
10
10
0
0
GRL
Qq3k3k1k1v40v40v40m16
10
10
10
0
0.01
sKizzo-0.9-std
Qq3k3k1k1v40v40v40m2
10
10
10
0
0.01
GRL
Qq3k3k1k1v40v40v40m32
10
10
10
0
0.01
yQuaffle
Qq3k3k1k1v40v40v40m4
10
10
10
0
0.01
sKizzo-0.9-abs
Qq3k3k1k1v40v40v40m8
10
10
10
0
0.01
QUANTOR_hc
Qq3k3k1k1v80v80v80m16
10
10
10
0
0.01
sKizzo-0.9-grn
Qq3k3k1k1v80v80v80m2
10
10
10
0
0
sKizzo-0.9-std
Qq3k3k1k1v80v80v80m32
10
10
10
0
0.01
QUANTOR_hc
Qq3k3k1k1v80v80v80m4
10
10
10
0
0.02
GRL
Qq3k3k1k1v80v80v80m8
10
10
10
0
0.03
yQuaffle
Qshifter
4
4
4
0
5.38
sKizzo-0.9-std
RobotsD2
10
10
10
0
19.54
sKizzo-0.9-abs
RobotsD3
10
10
10
0
22.69
sKizzo-0.9-abs
RobotsD4
10
10
10
0
17.31
sKizzo-0.9-abs
RobotsD5
10
10
10
0
16.53
sKizzo-0.9-abs
s27
3
3
0
3
0.07
qube5.0
s298
2
2
0
2
0.09
QUANTOR_hc
s386
1
1
1
0
0.22
qube5.0
s499
2
2
2
0
5.05
qube5.0
s510
1
1
0
1
0.13
QUANTOR_hc
s713
1
1
1
0
0.81
qube5.0
s820
1
1
0
1
0.43
QUANTOR_hc
Sorting_networks
84
48
29
19
13809
2clsQ
Strategic_Companies
530
377
27
350
121480
qube3.0
SzymanskiP
9
9
0
9
239.27
qube3.0
term1
4
4
0
4
510.73
2clsQ
tipdiam
30
30
30
0
7.58
ssolve-ut
tipfixpoint
74
38
29
9
7390.9
qube5.0
Toilet
3
3
2
1
0.76
sKizzo-0.9-abs
ToiletA
2
2
1
1
10.19
ssolve+ut
ToiletC
1
1
1
0
0.01
GRL
Tree
1
1
0
1
0
QUANTOR
Contact
|
Organization
|
Links
|
Citing QBFLIB
qbflib.org