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
Qute_opt617
QBFEVAL'17 - Prenex non-CNF Track
Instance
Result
Time
halfadder_match2.sat
SAT
0
halfadder_match2.unsat
UNSAT
0
mvs16y.unsat
UNSAT
0.01
mutex-4-s
SAT
0.01
szymanski-5-s
UNSAT
0.04
mutex-32-s
SAT
0.07
CHAIN20v.21
SAT
0.09
szymanski-6-s
UNSAT
0.11
CHAIN22v.23
SAT
0.12
stay24n.unsat
UNSAT
0.12
assertion12_0_1
UNSAT
0.13
CHAIN23v.24
SAT
0.14
mutex-64-s
SAT
0.15
mvs16y.sat
SAT
0.26
klieber2017q-108-27-t1
UNSAT
0.32
k_ph_n-21
SAT
0.4
BLOCKS4iii.6
UNSAT
0.47
stay24n.sat
SAT
0.5
szymanski-8-s
UNSAT
0.53
consistency_0_1
SAT
0.56
driver_d9y.unsat
UNSAT
0.6
possibility8_0_1
SAT
0.73
possibility10_0_1
UNSAT
0.91
Core1108_tbm_02.tex.moduleQ3.2S.000015
UNSAT
1.06
SR-unsat-03-01-07-1
UNSAT
1.3
beemldelec4b1_c0to127.unsat
UNSAT
1.37
possibility5_0_1
UNSAT
1.5
oski3ub5i_c0to255.unsat
UNSAT
1.67
consistency_0_2
SAT
2.48
b20_PR_7_20
SAT
2.64
driver_d9y.sat
SAT
3.32
assertion12_0_2
SAT
4.68
klieber2017q-092-23-t1
UNSAT
4.88
consistency_0_3
SAT
6.34
possibility6_0_3
UNSAT
6.43
incrementer-enc07-uniform-depth-25
UNSAT
6.55
fpu-10Xe-correct01-nonuniform-depth-24
UNSAT
6.67
fpu-10Xh-correct04-nonuniform-depth-27
UNSAT
7.75
klieber2017q-078-19-t1
UNSAT
7.79
b22_PR_8_20
SAT
8.62
assertion6_0_3
UNSAT
9.49
filesys_smbmrx_cvsndrcv.c
UNSAT
10.59
szymanski-14-s
UNSAT
13.67
consistency_0_4
SAT
15.3
possibility7_0_3
SAT
15.4
klieber2017q-076-19-t1
UNSAT
16.44
klieber2017q-084-21-t1
UNSAT
16.6
vonNeumann-ripple-carry-12-c
UNSAT
22.92
szymanski-16-s
UNSAT
27.5
consistency_0_5
SAT
27.83
DW-unsat-09-23-1
UNSAT
33.58
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
34.24
JP-unsat-02-07-2
UNSAT
38.21
uclid-pipe3a
SAT
44.03
consistency_0_6
SAT
46.14
assertion10_0_6
SAT
50.43
possibility6_0_7
UNSAT
56.51
ltl2dba_C2-6_comp3_REAL.unsat
UNSAT
57
uclid-pipe2
SAT
66.92
ev-pr-4x4-13-3-0-0-1-lg
SAT
69.53
consistency_0_7
SAT
82.63
consistency_0_8
SAT
115.99
assertion1_0_9
SAT
125.93
klieber2017q-086-21-t1
UNSAT
128.55
assertion1_0_10
SAT
156.4
consistency_0_9
SAT
166.2
possibility6_0_10
UNSAT
183.45
klieber2017q-074-18-t1
UNSAT
208.43
consistency_0_10
SAT
228.76
assertion7_0_3
UNSAT
287.68
s15850_PR_8_50
SAT
290.41
amba2f9n.unsat
UNSAT
299.98
ev-pr-4x4-11-3-0-0-1-lg
SAT
320.27
SR-unsat-04-01-08-1
UNSAT
350.13
k_branch_p-10
UNSAT
371.88
amba2f9n.sat
SAT
384.93
DW-sat-08-24-1
SAT
420.69
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
455.21
assertion1_0_4
SAT
604.39
DW-unsat-08-21-1
UNSAT
796.41
klieber2017q-080-20-t1
UNSAT
827.53
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp
FAIL
900
genbuf10b4n.sat
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#384.w#6.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.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#416.w#2.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900
genbuf10b4n.unsat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
FAIL
900
genbuf9b4n.sat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
FAIL
900
possibility8_0_7
FAIL
900
genbuf9b4n.unsat
FAIL
900
possibility7_0_6
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
FAIL
900
DWs-unsat-11-24-1
FAIL
900
amba4b9y.unsat
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
cycle_sched_4_7_1.unsat
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.asp
FAIL
900
cycle_sched_6_7_1.unsat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.asp
FAIL
900
driver_a9n.sat
FAIL
900
amba4b9y.sat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
FAIL
900
driver_a9n.unsat
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#304.w#6.s#8.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#304.w#4.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
ltl2dpa_C26_comp2_REAL.unsat
FAIL
900
DWs-sat-10-23-1
FAIL
900
DW-sat-19-46-1
FAIL
900
DW-sat-19-45-1
FAIL
900
DW-sat-19-44-1
FAIL
900
DW-sat-08-23-1
FAIL
900
DW-sat-08-22-1
FAIL
900
CM-unsat-18-01-05-3
FAIL
900
CM-unsat-17-01-06-2
FAIL
900
CM-unsat-17-01-05-3
FAIL
900
CM-unsat-08-01-05-3
FAIL
900
CM-unsat-07-01-06-2
FAIL
900
CM-unsat-07-01-05-3
FAIL
900
CM-sat-17-01-07-3
FAIL
900
CM-sat-17-01-06-4
FAIL
900
CM-sat-17-01-06-3
FAIL
900
DWs-sat-10-24-1
FAIL
900
DWs-sat-10-25-1
FAIL
900
SR-unsat-04-01-07-2
FAIL
900
SR-sat-04-01-08-2
FAIL
900
SR-sat-03-01-08-2
FAIL
900
SR-sat-03-01-07-3
FAIL
900
JP-unsat-03-07-4
FAIL
900
JP-unsat-02-06-3
FAIL
900
JP-sat-03-09-5
FAIL
900
JP-sat-03-09-4
FAIL
900
JP-sat-03-08-5
FAIL
900
DW-unsat-20-44-1
FAIL
900
DW-unsat-19-43-1
FAIL
900
DW-unsat-19-42-1
FAIL
900
DW-unsat-09-22-1
FAIL
900
DWs-unsat-12-25-1
FAIL
900
DWs-unsat-11-23-1
FAIL
900
CM-sat-07-01-07-3
FAIL
900
CM-sat-07-01-06-4
FAIL
900
CM-sat-07-01-06-3
FAIL
900
klieber2017q-080-20-eq
FAIL
900
klieber2017q-078-19-eq
FAIL
900
klieber2017q-076-19-eq
FAIL
900
klieber2017q-074-18-eq
FAIL
900
klieber2017q-104-26-eq
FAIL
900
mult_bool_matrix_17_17_17.unsat
FAIL
900
mult_bool_matrix_17_17_17.sat
FAIL
900
mult_bool_matrix_10_9_11.unsat
FAIL
900
mult_bool_matrix_10_9_11.sat
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
load_full_4_comp3_REAL.unsat
FAIL
900
load_full_4_comp3_REAL.sat
FAIL
900
load_3c_comp_comp7_REAL.unsat
FAIL
900
load_3c_comp_comp7_REAL.sat
FAIL
900
klieber2017q-082-20-eq
FAIL
900
klieber2017q-082-20-t1
FAIL
900
klieber2017q-116-29-t1
FAIL
900
klieber2017q-116-29-eq
FAIL
900
klieber2017q-112-28-t1
FAIL
900
klieber2017q-112-28-eq
FAIL
900
klieber2017q-108-27-eq
FAIL
900
klieber2017q-104-26-t1
FAIL
900
klieber2017q-100-25-t1
FAIL
900
klieber2017q-100-25-eq
FAIL
900
klieber2017q-096-24-t1
FAIL
900
klieber2017q-096-24-eq
FAIL
900
klieber2017q-092-23-eq
FAIL
900
klieber2017q-088-22-t1
FAIL
900
klieber2017q-088-22-eq
FAIL
900
klieber2017q-086-21-eq
FAIL
900
klieber2017q-084-21-eq
FAIL
900
oski3ub5i_c0to255.sat
FAIL
900
f600-50
FAIL
900
s3330_d12_u
FAIL
900
s1269_d15_u
FAIL
900
cnt16r
FAIL
900
cnt14
FAIL
900
k_ph_p-19
FAIL
900
k_branch_p-11
FAIL
900
k_branch_n-10
FAIL
900
C499.blif_0.10_0.20_0_0_out_exact
FAIL
900
adder-12-unsat
FAIL
900
ev-pr-8x8-15-7-0-1-2-lg
FAIL
900
test3_quant_squaring2
FAIL
900
test3_quant_squaring4
FAIL
900
C880.blif_0.10_1.00_0_0_inp_exact
FAIL
900
Adder2-16-s
FAIL
900
ken.flash^08.C-d4
FAIL
900
ken.oop^2.C-d4
FAIL
900
sortnetsort10.v.stepl.005
FAIL
900
c5_BMC_p2_k64
FAIL
900
c5_BMC_p2_k128
FAIL
900
c2_BMC_p1_k2048
FAIL
900
ring_r6_ser--opt-17_
FAIL
900
emptyroom_e4_ser--opt-44_
FAIL
900
cube_c7_ser--opt-24_
FAIL
900
c4_Debug_s5_f2_e2_v1
FAIL
900
c4_Debug_s3_f2_e2_v2
FAIL
900
c3_Debug_s3_f2_e2_v2
FAIL
900
c2_Debug_s3_f1_e1_v2
FAIL
900
c1_Debug_s5_f1_e1_v2
FAIL
900
sortnetsort9.v.stepl.007
FAIL
900
sortnetsort9.v.stepl.005
FAIL
900
sortnetsort9.AE.stepl.012
FAIL
900
s3330_d9_s
FAIL
900
test1_quant_squaring3
FAIL
900
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
900
ev-pr-8x8-13-7-0-1-2-lg
FAIL
900
qshifter_7
FAIL
900
ev-pr-6x6-17-5-0-1-2-s
FAIL
900
ev-pr-6x6-13-5-0-1-2-s
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
qshifter_8
FAIL
900
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
900
ev-pr-6x6-19-5-0-1-2-lg
FAIL
900
test2_quant_squaring2
FAIL
900
k_ph_p-12
FAIL
900
C499.blif_0.10_0.20_0_1_out_exact
FAIL
900
connect_9x8_6_R
FAIL
900
C499.blif_0.10_1.00_0_0_out_exact
FAIL
900
ev-pr-4x4-13-3-0-0-1-s
FAIL
900
ev-pr-4x4-17-3-0-0-1-s
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
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900
stmt19_64_99
FAIL
900
possibility5_0_9
FAIL
900
assertion2_0_8
FAIL
900
assertion2_0_6
FAIL
900
assertion2_0_5
FAIL
900
assertion2_0_3
FAIL
900
assertion11_0_7
FAIL
900
assertion10_0_9
FAIL
900
query44_query26_1344n
FAIL
900
query42_query06_1344n
FAIL
900
pipesnotankage18_8
FAIL
900
pipesnotankage14_10
FAIL
900
p20-5.pddl_planlen=32
FAIL
900
p20-20.pddl_planlen=23
FAIL
900
p20-1.pddl_planlen=24
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
900
assertion3_0_6
FAIL
900
assertion4_0_10
FAIL
900
assertion5_0_9
FAIL
900
possibility5_0_4
FAIL
900
possibility4_0_7
FAIL
900
possibility4_0_5
FAIL
900
possibility3_0_6
FAIL
900
possibility3_0_3
FAIL
900
possibility11_0_7
FAIL
900
possibility10_0_7
FAIL
900
possibility10_0_2
FAIL
900
possibility1_0_8
FAIL
900
possibility1_0_3
FAIL
900
incrementer-enc08-uniform-depth-33
FAIL
900
assertion9_0_7
FAIL
900
assertion9_0_3
FAIL
900
assertion7_0_4
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
900
b21_C_3_206
FAIL
900
rankfunc17_unsigned_16
FAIL
900
rankfunc13_unsigned_64
FAIL
900
s1269_d12_u
FAIL
900
s1269_d13_u
FAIL
900
k5_2_3
FAIL
900
k14_2_3
FAIL
900
k8_2_3
FAIL
900
k12_4_2
FAIL
900
stmt41_160_235
FAIL
900
stmt41_738_749
FAIL
900
stmt16_950_951
FAIL
900
stmt17_86_98
FAIL
900
stmt17_63_82
FAIL
900
stmt17_70_90
FAIL
900
rankfunc33_signed_32
FAIL
900
rankfunc5_unsigned_64
FAIL
900
rankfunc14_signed_64
FAIL
900
b20_C_3_2
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
900
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
900
incrementer-enc02-uniform-depth-58
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
Umbrella_tbm_05.tex.module.000039
FAIL
900
stmt28_68_81
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB