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'16 - Evaluate & Certify (non-competitive) Track.
Family
Overall
Time
Reference solver
N
#
S
U
Abduction
10
9
4
5
103.67
caqe-picosat-cert
Adder
10
2
0
2
0.16
depqbf-cert-v2
blackbox-01X-QBF
10
7
0
7
100.76
depqbf-cert-v1
Blocks
10
10
3
7
73.18
caqe-minisat-cert
BMC
10
5
2
3
284.76
depqbf-cert-v2
bomb
10
3
3
0
7.25
depqbf-cert-v2
C432
8
4
3
1
31.86
depqbf-cert-v2
C499
8
4
3
1
197.26
caqe-picosat-cert
C5315
8
3
2
1
4.1
caqe-minisat-cert
C880
8
2
2
0
1.22
depqbf-cert-v2
Chain
10
4
4
0
558.66
cheq
circuits
10
1
1
0
0.11
depqbf-cert-v2
conformant_planning
10
5
4
1
108.57
depqbf-cert-v2
Connect4
10
6
0
6
58.56
depqbf-cert-v2
Counter
10
8
8
0
731.76
caqe-picosat-cert
DFlipFlop
10
10
0
10
16.36
depqbf-cert-v2
dungeon
10
3
0
3
31.53
depqbf-cert-v1
evader-pursuer-4x4-logarithmic
7
7
7
0
6.38
depqbf-cert-v2
evader-pursuer-6x6-logarithmic
8
4
0
4
109.05
depqbf-cert-v1
evader-pursuer-6x6-standard
8
1
0
1
68.82
depqbf-cert-v1
evader-pursuer-8x8-logarithmic
8
4
0
4
119.64
depqbf-cert-v1
FPGA_PLB_FIT_FAST
5
5
4
1
4.06
depqbf-cert-v2
FPGA_PLB_FIT_SLOW
3
2
1
1
98.66
cheq
fpu
10
10
0
10
452.83
depqbf-cert-v2
Generalized-Tic-Tac-Toe
10
7
1
6
170.1
caqe-picosat-cert
Impl
10
10
10
0
0.1
cheq
incrementer-encoder
10
6
0
6
16.14
depqbf-cert-v2
ISCAS89
8
6
5
1
29.97
depqbf-cert-v2
ITC99
7
2
1
1
0.71
depqbf-cert-v2
k_branch_n
10
2
2
0
15.72
cheq
k_branch_p
10
1
0
1
118.72
depqbf-cert-v1
k_d4_n
10
3
3
0
47.22
cheq
k_d4_p
10
10
0
10
1.22
depqbf-cert-v1
k_dum_n
10
4
4
0
132.4
cheq
k_dum_p
10
9
0
9
120.1
depqbf-cert-v1
k_grz_n
10
3
3
0
521.84
cheq
k_grz_p
10
8
0
8
193.09
depqbf-cert-v1
k_lin_n
10
6
6
0
793.21
cheq
k_lin_p
10
10
0
10
4.83
depqbf-cert-v2
k_path_n
10
2
2
0
22.35
cheq
k_path_p
10
2
0
2
0.4
depqbf-cert-v1
k_ph_n
10
10
10
0
674.8
cheq
k_ph_p
10
3
0
3
0.23
caqe-minisat-cert
k_poly_n
10
1
1
0
1.06
cheq
k_poly_p
10
10
0
10
0.93
depqbf-cert-v2
k_t4p_p
10
1
0
1
25.81
depqbf-cert-v1
Logn
4
4
0
4
33.48
caqe-minisat-cert
mqm
10
6
2
4
139.93
cheq
MutexP
7
3
3
0
73.22
cheq
Planning-CTE
7
2
2
0
0.72
depqbf-cert-v2
QBF-Hardness
10
7
0
7
448.76
caqe-picosat-cert
qbfeval12
5
5
1
4
1.09
caqe-minisat-cert
Qshifter
6
1
1
0
0.17
cheq
Reduction-finding
10
4
1
3
9.55
depqbf-cert-v2
Rewriting
10
10
0
10
0.47
cheq
s27
4
4
1
3
32.6
caqe-picosat-cert
Sorting_networks
10
5
3
2
131.25
depqbf-cert-v2
SzymanskiP
10
9
0
9
453.42
cheq
term1
8
7
4
3
335.28
depqbf-cert-v2
terminator
10
7
0
7
6.47
depqbf-cert-v1
tipdiam
10
4
4
0
57.69
cheq
tipfixpoint
10
3
0
3
2.44
depqbf-cert-v2
ToiletA
10
10
3
7
2.27
cheq
ToiletC
10
10
1
9
178.39
caqe-minisat-cert
ToiletG
7
7
7
0
0.12
cheq
trafficlight-controller
10
8
0
8
265.02
cheq
Tree
10
10
2
8
6.76
cheq
VonNeumann
10
10
0
10
184.24
caqe-minisat-cert
wmiforward
10
3
3
0
0.03
cheq
z4ml
8
8
4
4
0.21
caqe-minisat-cert
Contact
|
Organization
|
Links
|
Citing QBFLIB