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 - Prenex non-CNF Track.
Family
Overall
Time
Reference solver
N
#
S
U
Abduction
5
4
1
3
0.52
qsts
Adder
5
4
0
4
388.13
xb-bid-qsts
blackbox-01X-QBF
5
5
1
4
5.66
xb-qsts
blackbox_design
5
5
5
0
0.84
quabs-picosat
Blocks
5
5
2
3
0.19
qsts
BMC
5
2
0
2
0.02
qsts
bomb
5
3
1
2
710.42
xb-bid-qsts
C432
4
4
4
0
0.57
xb-qsts
C499
4
4
4
0
0.36
xb-bid-qsts
C5315
4
3
3
0
0.47
xb-bid-qsts
C6288
4
3
3
0
1.19
xb-qsts
C880
4
4
2
2
0.56
qsts
Chain
5
5
0
5
0.11
qsts
circuits
5
3
3
0
451.84
xb-bid-qsts
conformant_planning
6
4
3
1
103.02
xb-qsts
Connect4
5
4
1
3
429.39
xb-bid-qsts
Counter
5
4
4
0
2.29
xb-qsts
DFlipFlop
5
5
0
5
7.79
qsts
dungeon
5
5
0
5
20.92
qsts
evader-pursuer-4x4-logarithmic
4
4
4
0
29.2
ghostq-plain
evader-pursuer-6x6-logarithmic
4
2
0
2
95.54
xb-qsts
evader-pursuer-8x8-logarithmic
4
2
0
2
570.36
xb-qsts
FPGA_PLB_FIT_FAST
3
3
2
1
2.03
xb-qsts
FPGA_PLB_FIT_SLOW
2
2
0
2
6.56
xb-qsts
fpu
5
5
0
5
8.3
qsts
Generalized-Tic-Tac-Toe
5
5
0
5
9.82
qsts
HardwareFixpoint
5
5
2
3
60.67
xb-bid-qsts
Impl
5
5
5
0
0.08
qsts
incrementer-encoder
5
5
1
4
3.96
qsts
irqlkeapclte
5
4
4
0
1604.25
ghostq-cegar
ISCAS89
3
3
3
0
62.46
xb-qsts
ITC99
5
3
3
0
123.74
ghostq-cegar
jmc_quant_squaring
5
1
0
1
8
xb-qsts
k_branch_n
5
5
5
0
7.94
xb-qsts
k_branch_p
5
5
0
5
16.38
xb-qsts
k_d4_n
5
5
5
0
0.34
qsts
k_d4_p
5
5
0
5
0.23
qsts
k_dum_n
5
5
5
0
0.14
qsts
k_dum_p
5
5
0
5
0.09
qsts
k_grz_n
5
5
5
0
0.14
qsts
k_grz_p
5
5
0
5
0.17
qsts
k_lin_n
5
5
5
0
0.8
qsts
k_lin_p
5
5
0
5
0.08
qsts
k_path_n
5
5
5
0
0.13
qsts
k_path_p
5
5
0
5
0.11
qsts
k_ph_n
5
5
3
2
0.22
qsts
k_ph_p
5
4
0
4
59.15
xb-bid-qsts
k_poly_n
5
5
5
0
0.28
qsts
k_poly_p
5
5
0
5
0.24
qsts
k_t4p_n
5
5
5
0
0.53
qsts
k_t4p_p
5
5
0
5
0.37
qsts
LinearBitvectorRankingFunction
5
1
0
1
30.25
rareqs-nn
Logn
2
2
0
2
2.12
qsts
mqm
136
136
5
131
31.38
qsts
MutexP
4
4
4
0
0.1
qsts
NuSMV_diam
92
92
81
11
2.77
qsts
Planning-CTE
3
1
1
0
0.52
qsts
QBF-Hardness
5
4
1
3
30.14
quabs-picosat
qbfeval12
2
2
0
2
0.45
ghostq-plain
QLTL_safety
250
250
250
0
23.53
xb-qsts
Qshifter
3
2
2
0
28.08
xb-bid-qsts
RankingFunctions
5
5
5
0
3.4
xb-qsts
Reduction-finding
5
3
0
3
3.34
ghostq-cegar
Rewriting
5
5
0
5
0.02
quabs-minisat
s1196
3
3
1
2
1.67
qsts
s1269
5
5
1
4
0.36
qsts
s27
2
2
0
2
0
quabs-minisat
s298
5
5
2
3
0.56
qsts
s3330
5
5
0
5
0.5
qsts
s386
5
5
2
3
0.2
qsts
s499
5
5
2
3
0.25
qsts
s510
5
5
2
3
0.35
qsts
s641
5
5
3
2
0.66
qsts
s713
5
5
3
2
1.23
qsts
s820
5
5
2
3
0.26
qsts
Sorting_networks
5
3
2
1
181.51
xb-bid-qsts
SzymanskiP
5
5
0
5
700.77
qsts
term1
4
4
4
0
0.62
xb-qsts
terminator
5
5
0
5
0.51
quabs-minisat
tipdiam
5
5
3
2
0.14
qsts
tipfixpoint
5
5
4
1
0.45
qsts
ToiletA
5
5
0
5
3.81
ghostq-plain
ToiletC
5
5
1
4
11.24
quabs-minisat
ToiletG
4
4
4
0
0.02
quabs-minisat
trafficlight-controller
5
5
0
5
6.57
qsts
Tree
5
5
1
4
0.11
qsts
uclid
2
2
2
0
0.24
xb-bid-qsts
VonNeumann
5
5
0
5
12.3
qsts
wmiforward
5
5
5
0
1.02
ghostq-cegar
z4ml
4
4
3
1
0
quabs-picosat
Contact
|
Organization
|
Links
|
Citing QBFLIB