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
Instances solved by
qfun0.1
QBFEVAL'17 - Prenex non-CNF Track
Instance
Result
Time
halfadder_match2.sat
SAT
0.06
halfadder_match2.unsat
UNSAT
0.06
mvs16y.unsat
UNSAT
0.08
mutex-4-s
SAT
0.1
C499.blif_0.10_1.00_0_0_out_exact
UNSAT
0.16
stmt16_950_951
SAT
0.19
klieber2017q-076-19-t1
UNSAT
0.22
stmt41_738_749
SAT
0.26
ltl2dba_C2-6_comp3_REAL.unsat
UNSAT
0.27
klieber2017q-074-18-t1
UNSAT
0.3
klieber2017q-086-21-t1
UNSAT
0.31
klieber2017q-082-20-t1
UNSAT
0.33
klieber2017q-092-23-t1
UNSAT
0.36
klieber2017q-084-21-eq
SAT
0.39
klieber2017q-078-19-t1
UNSAT
0.39
szymanski-5-s
UNSAT
0.41
klieber2017q-080-20-t1
UNSAT
0.41
klieber2017q-086-21-eq
SAT
0.42
klieber2017q-088-22-t1
UNSAT
0.42
klieber2017q-100-25-t1
UNSAT
0.43
driver_d9y.unsat
UNSAT
0.45
klieber2017q-074-18-eq
SAT
0.46
mutex-32-s
SAT
0.46
klieber2017q-078-19-eq
SAT
0.48
klieber2017q-108-27-t1
UNSAT
0.5
klieber2017q-082-20-eq
SAT
0.5
klieber2017q-080-20-eq
SAT
0.5
klieber2017q-076-19-eq
SAT
0.51
klieber2017q-084-21-t1
UNSAT
0.51
klieber2017q-104-26-t1
UNSAT
0.54
klieber2017q-116-29-t1
UNSAT
0.55
klieber2017q-092-23-eq
SAT
0.58
klieber2017q-088-22-eq
SAT
0.59
stay24n.unsat
UNSAT
0.61
klieber2017q-096-24-eq
SAT
0.61
klieber2017q-096-24-t1
UNSAT
0.62
klieber2017q-112-28-t1
UNSAT
0.64
ltl2dpa_C26_comp2_REAL.unsat
UNSAT
0.64
klieber2017q-112-28-eq
SAT
0.75
consistency_0_2
FAIL
0.81
possibility10_0_2
FAIL
0.81
klieber2017q-100-25-eq
SAT
0.81
assertion12_0_2
FAIL
0.82
klieber2017q-104-26-eq
SAT
0.87
klieber2017q-108-27-eq
SAT
0.88
mutex-64-s
SAT
0.91
BLOCKS4iii.6
UNSAT
1.03
CHAIN20v.21
SAT
1.1
assertion12_0_1
UNSAT
1.14
possibility6_0_3
FAIL
1.16
consistency_0_3
FAIL
1.16
possibility7_0_3
FAIL
1.17
assertion7_0_3
FAIL
1.18
possibility3_0_3
FAIL
1.18
possibility1_0_3
FAIL
1.18
assertion9_0_3
FAIL
1.18
incrementer-enc07-uniform-depth-25
UNSAT
1.19
assertion6_0_3
FAIL
1.19
assertion2_0_3
FAIL
1.19
C499.blif_0.10_0.20_0_1_out_exact
UNSAT
1.36
szymanski-6-s
UNSAT
1.38
CHAIN22v.23
SAT
1.44
incrementer-enc08-uniform-depth-33
SAT
1.47
C499.blif_0.10_0.20_0_0_out_exact
UNSAT
1.5
consistency_0_4
FAIL
1.57
assertion7_0_4
FAIL
1.59
possibility5_0_4
FAIL
1.59
assertion1_0_4
FAIL
1.6
CHAIN23v.24
SAT
1.66
SR-unsat-03-01-07-1
UNSAT
2.03
consistency_0_5
FAIL
2.05
assertion2_0_5
FAIL
2.07
possibility4_0_5
FAIL
2.08
C880.blif_0.10_1.00_0_0_inp_exact
UNSAT
2.44
consistency_0_6
FAIL
2.62
assertion3_0_6
FAIL
2.63
assertion10_0_6
FAIL
2.64
possibility7_0_6
FAIL
2.64
possibility3_0_6
FAIL
2.65
assertion2_0_6
FAIL
2.65
klieber2017q-116-29-eq
SAT
2.85
incrementer-enc02-uniform-depth-58
UNSAT
3.18
possibility4_0_7
FAIL
3.26
possibility11_0_7
FAIL
3.26
assertion11_0_7
FAIL
3.27
assertion9_0_7
FAIL
3.27
consistency_0_7
FAIL
3.27
possibility6_0_7
FAIL
3.28
possibility10_0_7
FAIL
3.3
possibility8_0_7
FAIL
3.37
JP-unsat-02-07-2
UNSAT
3.78
consistency_0_8
FAIL
3.99
possibility1_0_8
FAIL
3.99
assertion2_0_8
FAIL
4.03
assertion1_0_9
FAIL
4.87
consistency_0_9
FAIL
4.88
assertion5_0_9
FAIL
4.91
possibility5_0_9
FAIL
4.92
assertion10_0_9
FAIL
4.95
load_3c_comp_comp7_REAL.unsat
UNSAT
5.21
assertion1_0_10
FAIL
5.89
consistency_0_10
FAIL
5.92
possibility6_0_10
FAIL
5.93
assertion4_0_10
FAIL
5.97
sortnetsort9.AE.stepl.012
UNSAT
6.19
szymanski-8-s
UNSAT
6.91
driver_a9n.unsat
UNSAT
7.01
b20_PR_7_20
SAT
7.09
cube_c7_ser--opt-24_
SAT
7.89
oski3ub5i_c0to255.unsat
UNSAT
7.89
beemldelec4b1_c0to127.unsat
UNSAT
8.11
b21_C_3_206
SAT
8.64
filesys_smbmrx_cvsndrcv.c
UNSAT
10.05
amba2f9n.unsat
UNSAT
15.21
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
20.57
JP-unsat-02-06-3
UNSAT
20.7
sortnetsort9.v.stepl.007
SAT
26.97
b22_PR_8_20
SAT
28.58
k_ph_p-12
UNSAT
31.59
uclid-pipe3a
SAT
37.26
stmt28_68_81
SAT
39.52
stmt17_63_82
SAT
45.21
stmt17_70_90
SAT
48.81
stmt19_64_99
SAT
50.58
DW-sat-08-23-1
SAT
50.75
SR-unsat-04-01-08-1
UNSAT
54.19
DW-sat-08-24-1
SAT
57.07
stay24n.sat
SAT
64.92
fpu-10Xe-correct01-nonuniform-depth-24
UNSAT
72.62
p20-1.pddl_planlen=24
UNSAT
80.37
stmt17_86_98
SAT
88.31
fpu-10Xh-correct04-nonuniform-depth-27
UNSAT
93.23
DWs-sat-10-24-1
SAT
94.19
k_ph_n-21
SAT
97.07
c2_BMC_p1_k2048
SAT
106.98
emptyroom_e4_ser--opt-44_
SAT
109.72
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
109.8
load_full_4_comp3_REAL.unsat
UNSAT
111.07
DW-sat-08-22-1
SAT
136.32
CM-sat-07-01-07-3
SAT
137.68
mvs16y.sat
SAT
146.82
CM-sat-07-01-06-3
SAT
161.58
p20-20.pddl_planlen=23
SAT
189.02
genbuf9b4n.unsat
UNSAT
189.67
DW-unsat-08-21-1
UNSAT
204.14
b20_C_3_2
SAT
205.56
driver_d9y.sat
SAT
206.82
vonNeumann-ripple-carry-12-c
UNSAT
247.06
DW-unsat-09-22-1
UNSAT
255.53
genbuf10b4n.unsat
UNSAT
292.61
DWs-sat-10-25-1
SAT
313.86
dungeon_i15-m7-u4-v0.pddl_planlen=81
UNSAT
318.3
DWs-sat-10-23-1
SAT
323.67
k5_2_3
SAT
360.12
ken.flash^08.C-d4
UNSAT
377.82
pipesnotankage14_10
UNSAT
478.93
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
531.18
DW-unsat-09-23-1
UNSAT
558.27
CM-sat-07-01-06-4
SAT
763.52
cycle_sched_4_7_1.unsat
UNSAT
796.48
szymanski-14-s
UNSAT
836.39
SR-sat-03-01-07-3
FAIL
882.05
c3_Debug_s3_f2_e2_v2
FAIL
882.61
pipesnotankage18_8
FAIL
885.12
CM-sat-17-01-06-4
FAIL
885.22
SR-sat-04-01-08-2
FAIL
891.83
CM-sat-17-01-07-3
FAIL
892.59
SR-unsat-04-01-07-2
FAIL
893.05
CM-sat-17-01-06-3
FAIL
893.83
CM-unsat-18-01-05-3
FAIL
894.31
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
894.75
CM-unsat-17-01-05-3
FAIL
895.01
c4_Debug_s5_f2_e2_v1
FAIL
895.04
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
895.41
c2_Debug_s3_f1_e1_v2
FAIL
895.83
ev-pr-6x6-17-5-0-1-2-s
FAIL
895.84
c1_Debug_s5_f1_e1_v2
FAIL
896.43
ev-pr-6x6-13-5-0-1-2-s
FAIL
896.91
DWs-unsat-11-23-1
UNSAT
898.65
mult_bool_matrix_17_17_17.unsat
FAIL
900
oski3ub5i_c0to255.sat
FAIL
900
CM-unsat-07-01-05-3
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
mult_bool_matrix_17_17_17.sat
FAIL
900
genbuf9b4n.sat
FAIL
900
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
mult_bool_matrix_10_9_11.sat
FAIL
900
genbuf10b4n.sat
FAIL
900
mult_bool_matrix_10_9_11.unsat
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
CM-unsat-08-01-05-3
FAIL
900
driver_a9n.sat
FAIL
900
cycle_sched_6_7_1.unsat
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
CM-unsat-07-01-06-2
FAIL
900
JP-sat-03-09-5
FAIL
900
load_3c_comp_comp7_REAL.sat
FAIL
900
DW-sat-19-44-1
FAIL
900
DW-sat-19-45-1
FAIL
900
DW-sat-19-46-1
FAIL
900
SR-sat-03-01-08-2
FAIL
900
CM-unsat-17-01-06-2
FAIL
900
JP-unsat-03-07-4
FAIL
900
DWs-unsat-11-24-1
FAIL
900
DWs-unsat-12-25-1
FAIL
900
connect_9x8_6_R
FAIL
900
DW-unsat-19-42-1
FAIL
900
load_full_4_comp3_REAL.sat
FAIL
900
DW-unsat-19-43-1
FAIL
900
DW-unsat-20-44-1
FAIL
900
JP-sat-03-08-5
FAIL
900
JP-sat-03-09-4
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
amba4b9y.unsat
FAIL
900
c5_BMC_p2_k64
FAIL
900
k_branch_p-10
FAIL
900
k_branch_n-10
FAIL
900
adder-12-unsat
FAIL
900
ev-pr-8x8-15-7-0-1-2-lg
FAIL
900
szymanski-16-s
FAIL
900
test3_quant_squaring2
FAIL
900
test3_quant_squaring4
FAIL
900
Adder2-16-s
FAIL
900
s3330_d9_s
FAIL
900
test1_quant_squaring3
FAIL
900
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
900
k_branch_p-11
FAIL
900
k_ph_p-19
FAIL
900
c5_BMC_p2_k128
FAIL
900
ring_r6_ser--opt-17_
FAIL
900
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900
c4_Debug_s3_f2_e2_v2
FAIL
900
sortnetsort9.v.stepl.005
FAIL
900
sortnetsort10.v.stepl.005
FAIL
900
ken.oop^2.C-d4
FAIL
900
s3330_d12_u
FAIL
900
s1269_d15_u
FAIL
900
cnt16r
FAIL
900
cnt14
FAIL
900
ev-pr-4x4-11-3-0-0-1-lg
FAIL
900
ev-pr-4x4-13-3-0-0-1-s
FAIL
900
ev-pr-4x4-17-3-0-0-1-s
FAIL
900
ev-pr-8x8-13-7-0-1-2-lg
FAIL
900
qshifter_7
FAIL
900
k_branch_n-12
FAIL
900
k_branch_p-16
FAIL
900
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
900
ev-pr-6x6-11-5-0-1-2-s
FAIL
900
ev-pr-4x4-15-3-0-0-1-s
FAIL
900
adder-10-sat
FAIL
900
connect_8x7_6_R
FAIL
900
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900
adder-14-sat
FAIL
900
ev-pr-4x4-13-3-0-0-1-lg
FAIL
900
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
900
uclid-pipe2
FAIL
900
C6288.blif_0.10_0.20_0_1_out_exact
FAIL
900
ev-pr-8x8-19-7-0-1-2-lg
FAIL
900
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
900
ev-pr-6x6-9-5-0-1-2-lg
FAIL
900
test2_quant_squaring3
FAIL
900
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
900
ev-pr-4x4-7-3-0-0-1-s
FAIL
900
ev-pr-6x6-9-5-0-1-2-s
FAIL
900
test2_quant_squaring2
FAIL
900
ev-pr-6x6-19-5-0-1-2-lg
FAIL
900
qshifter_8
FAIL
900
amba4b9y.sat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
FAIL
900
possibility8_0_1
FAIL
900
possibility5_0_1
FAIL
900
possibility10_0_1
FAIL
900
consistency_0_1
FAIL
900
s15850_PR_8_50
FAIL
900
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
900
amba2f9n.sat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#408.w#4.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.asp
FAIL
900
query44_query26_1344n
FAIL
900
query42_query06_1344n
FAIL
900
p20-5.pddl_planlen=32
FAIL
900
rankfunc14_signed_64
FAIL
900
rankfunc5_unsigned_64
FAIL
900
rankfunc33_signed_32
FAIL
900
rankfunc17_unsigned_16
FAIL
900
rankfunc13_unsigned_64
FAIL
900
s1269_d12_u
FAIL
900
s1269_d13_u
FAIL
900
k14_2_3
FAIL
900
k8_2_3
FAIL
900
k12_4_2
FAIL
900
stmt41_160_235
FAIL
900
Umbrella_tbm_05.tex.module.000039
FAIL
900
Core1108_tbm_02.tex.moduleQ3.2S.000015
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
900
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
900
audio_ddksynth_csynth2.cpp
FAIL
900
network_irda_miniport_nscirda_comm.c
FAIL
900
input_pnpi8042_moudep.c
FAIL
900
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
900
small-swap2-fixpoint-4
FAIL
900
small-synabs-fixpoint-9
FAIL
900
small-swap1-fixpoint-3
FAIL
900
sdlx-fixpoint-3
FAIL
900
cache-coherence-2-fixpoint-6
FAIL
900
f600-50
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB