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_hybrid
QBFEVAL'17 - Prenex non-CNF Track
Instance
Result
Time
halfadder_match2.unsat
UNSAT
0
mvs16y.unsat
UNSAT
0.01
halfadder_match2.sat
SAT
0.01
mutex-4-s
SAT
0.01
szymanski-5-s
UNSAT
0.04
mutex-32-s
SAT
0.07
mvs16y.sat
SAT
0.09
CHAIN20v.21
SAT
0.09
szymanski-6-s
UNSAT
0.11
stay24n.unsat
UNSAT
0.12
CHAIN22v.23
SAT
0.12
assertion12_0_1
UNSAT
0.14
CHAIN23v.24
SAT
0.14
mutex-64-s
SAT
0.15
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
0.17
stay24n.sat
SAT
0.36
k_ph_n-21
SAT
0.4
BLOCKS4iii.6
UNSAT
0.45
Core1108_tbm_02.tex.moduleQ3.2S.000015
UNSAT
0.47
szymanski-8-s
UNSAT
0.53
consistency_0_1
SAT
0.56
driver_d9y.unsat
UNSAT
0.74
possibility8_0_1
SAT
0.98
possibility10_0_1
UNSAT
1.12
beemldelec4b1_c0to127.unsat
UNSAT
1.37
oski3ub5i_c0to255.unsat
UNSAT
1.68
SR-unsat-03-01-07-1
UNSAT
1.99
driver_d9y.sat
SAT
2.09
consistency_0_2
SAT
2.54
possibility5_0_1
UNSAT
3.5
assertion12_0_2
SAT
3.51
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
UNSAT
3.65
klieber2017q-104-26-t1
UNSAT
3.71
b20_PR_7_20
SAT
4.16
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
5.22
possibility6_0_3
UNSAT
6.34
consistency_0_3
SAT
6.42
fpu-10Xe-correct01-nonuniform-depth-24
UNSAT
6.69
fpu-10Xh-correct04-nonuniform-depth-27
UNSAT
7.83
assertion6_0_3
UNSAT
8.36
incrementer-enc07-uniform-depth-25
UNSAT
10.6
filesys_smbmrx_cvsndrcv.c
UNSAT
12
szymanski-14-s
UNSAT
13.62
DW-unsat-08-21-1
UNSAT
14.38
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
UNSAT
16.17
consistency_0_4
SAT
16.41
assertion1_0_4
SAT
16.59
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
UNSAT
20.27
vonNeumann-ripple-carry-12-c
UNSAT
22.83
klieber2017q-108-27-t1
UNSAT
23.42
klieber2017q-092-23-t1
UNSAT
27.91
klieber2017q-078-19-t1
UNSAT
30.9
b22_PR_8_20
SAT
31.78
possibility7_0_3
SAT
38.52
klieber2017q-084-21-t1
UNSAT
39.6
klieber2017q-076-19-t1
UNSAT
39.7
szymanski-16-s
UNSAT
50.61
consistency_0_5
SAT
51.08
DW-unsat-09-23-1
UNSAT
56.92
JP-unsat-02-07-2
UNSAT
61.4
uclid-pipe3a
SAT
67.08
consistency_0_6
SAT
69.33
assertion10_0_6
SAT
73.52
possibility6_0_7
UNSAT
79.72
ltl2dba_C2-6_comp3_REAL.unsat
UNSAT
80.13
uclid-pipe2
SAT
92.56
ev-pr-4x4-13-3-0-0-1-lg
SAT
92.65
consistency_0_7
SAT
105.12
consistency_0_8
SAT
139.6
assertion9_0_3
SAT
154.87
ev-pr-4x4-11-3-0-0-1-lg
SAT
192.51
C6288.blif_0.10_0.20_0_1_out_exact
SAT
196.18
klieber2017q-088-22-t1
UNSAT
196.54
assertion1_0_9
SAT
264.22
consistency_0_9
SAT
303.89
consistency_0_10
SAT
359.71
possibility6_0_10
UNSAT
363.1
amba2f9n.unsat
UNSAT
443.42
DW-unsat-09-22-1
UNSAT
456.7
SR-unsat-04-01-08-1
UNSAT
460.68
assertion7_0_3
UNSAT
472.58
klieber2017q-080-20-t1
UNSAT
485.04
assertion10_0_9
SAT
522.57
dungeon_i15-m7-u4-v0.pddl_planlen=81
UNSAT
529.27
k_branch_p-11
UNSAT
541.68
s15850_PR_8_50
SAT
545.77
klieber2017q-112-28-t1
UNSAT
565.88
CM-sat-07-01-07-3
SAT
569.33
stmt41_160_235
UNSAT
597.79
cnt14
SAT
614.9
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
653.45
rankfunc17_unsigned_16
FAIL
754.22
test3_quant_squaring2
UNSAT
793.36
k_branch_p-10
UNSAT
796.45
possibility1_0_3
SAT
813.34
SR-sat-03-01-08-2
FAIL
852.84
klieber2017q-116-29-t1
FAIL
854.9
f600-50
FAIL
855.62
klieber2017q-086-21-t1
FAIL
856.31
DW-sat-08-22-1
SAT
862.42
c1_Debug_s5_f1_e1_v2
FAIL
875.55
DW-sat-08-23-1
FAIL
875.61
possibility4_0_7
FAIL
875.72
ev-pr-6x6-9-5-0-1-2-s
FAIL
875.81
ev-pr-6x6-17-5-0-1-2-s
FAIL
875.81
ev-pr-4x4-13-3-0-0-1-s
FAIL
875.92
CM-unsat-07-01-05-3
FAIL
875.93
SR-sat-04-01-08-2
FAIL
875.95
DW-unsat-19-43-1
FAIL
875.95
c4_Debug_s3_f2_e2_v2
FAIL
876.07
connect_9x8_6_R
FAIL
876.16
assertion2_0_8
FAIL
876.23
k12_4_2
FAIL
876.31
CM-unsat-08-01-05-3
FAIL
876.31
CM-sat-17-01-07-3
FAIL
876.32
ev-pr-6x6-9-5-0-1-2-lg
FAIL
876.32
b20_C_3_2
FAIL
876.33
query42_query06_1344n
FAIL
876.33
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
876.34
DWs-unsat-12-25-1
FAIL
876.34
c3_Debug_s3_f2_e2_v2
FAIL
876.36
CM-unsat-18-01-05-3
FAIL
876.41
ev-pr-6x6-11-5-0-1-2-s
FAIL
876.41
ev-pr-8x8-7-7-0-1-2-lg
FAIL
876.41
ev-pr-8x8-13-7-0-1-2-lg
FAIL
876.41
ev-pr-6x6-19-5-0-1-2-lg
FAIL
876.42
pipesnotankage14_10
FAIL
876.42
JP-sat-03-09-5
FAIL
876.49
ev-pr-6x6-17-5-0-1-2-lg
FAIL
876.51
cnt16r
FAIL
876.52
DWs-unsat-11-24-1
FAIL
876.52
cycle_sched_4_7_1.unsat
FAIL
876.53
connect_8x7_6_R
FAIL
876.53
ev-pr-6x6-11-5-0-1-2-lg
FAIL
876.59
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
876.61
JP-unsat-03-07-4
FAIL
876.61
pipesnotankage18_8
FAIL
876.63
assertion1_0_10
FAIL
876.63
CM-sat-17-01-06-4
FAIL
876.64
p20-20.pddl_planlen=23
FAIL
876.67
ltl2dba_C2-6_comp3_REAL.sat
FAIL
876.71
load_full_4_comp3_REAL.unsat
FAIL
876.73
mult_bool_matrix_17_17_17.unsat
FAIL
876.73
ev-pr-4x4-17-3-0-0-1-s
FAIL
876.74
s1269_d15_u
FAIL
876.81
ev-pr-4x4-7-3-0-0-1-s
FAIL
876.82
s3330_d12_u
FAIL
876.82
CM-unsat-17-01-06-2
FAIL
876.82
s3330_d9_s
FAIL
876.82
load_3c_comp_comp7_REAL.sat
FAIL
876.82
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
876.84
p20-5.pddl_planlen=32
FAIL
876.89
SR-sat-03-01-07-3
FAIL
876.89
SR-unsat-04-01-07-2
FAIL
876.91
ltl2dpa_C26_comp2_REAL.sat
FAIL
876.92
possibility5_0_9
FAIL
876.93
DW-sat-08-24-1
FAIL
876.93
p20-1.pddl_planlen=24
FAIL
876.94
c4_Debug_s5_f2_e2_v1
FAIL
876.95
c2_BMC_p1_k2048
FAIL
876.97
cycle_sched_4_7_1.sat
FAIL
877
possibility3_0_6
FAIL
877.01
sortnetsort9.AE.stepl.012
FAIL
877.01
CM-sat-07-01-06-3
FAIL
877.01
amba2f9n.sat
FAIL
877.01
oski3ub5i_c0to255.sat
FAIL
877.02
possibility10_0_7
FAIL
877.02
c2_Debug_s3_f1_e1_v2
FAIL
877.05
ev-pr-6x6-13-5-0-1-2-s
FAIL
877.08
load_full_4_comp3_REAL.sat
FAIL
877.09
CM-unsat-17-01-05-3
FAIL
877.1
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
FAIL
877.11
k_branch_n-10
FAIL
877.11
adder-14-sat
FAIL
877.11
c5_BMC_p2_k128
FAIL
877.11
cycle_sched_6_7_1.sat
FAIL
877.11
possibility3_0_3
FAIL
877.12
b21_C_3_206
FAIL
877.12
qshifter_8
FAIL
877.12
load_3c_comp_comp7_REAL.unsat
FAIL
877.15
stmt19_64_99
FAIL
877.2
beemldelec4b1_c0to127.sat
FAIL
877.21
amba4b9y.sat
FAIL
877.21
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
FAIL
877.21
assertion11_0_7
FAIL
877.21
stmt16_950_951
FAIL
877.21
s1269_d13_u
FAIL
877.21
possibility1_0_8
FAIL
877.21
CM-sat-07-01-06-4
FAIL
877.21
DW-unsat-20-44-1
FAIL
877.22
stmt17_63_82
FAIL
877.22
amba4b9y.unsat
FAIL
877.22
DWs-unsat-11-23-1
FAIL
877.22
ev-pr-8x8-15-7-0-1-2-lg
FAIL
877.23
DW-sat-19-45-1
FAIL
877.25
assertion4_0_10
FAIL
877.26
possibility11_0_7
FAIL
877.3
s1269_d12_u
FAIL
877.31
JP-sat-03-09-4
FAIL
877.31
possibility5_0_4
FAIL
877.31
stmt28_68_81
FAIL
877.31
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
877.31
Adder2-16-s
FAIL
877.32
stmt17_86_98
FAIL
877.32
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
FAIL
877.32
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
FAIL
877.38
possibility10_0_2
FAIL
877.41
CM-sat-17-01-06-3
FAIL
877.41
k14_2_3
FAIL
877.42
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
877.42
k_branch_p-16
FAIL
877.5
DWs-sat-10-24-1
FAIL
877.51
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
877.51
query44_query26_1344n
FAIL
877.52
k_ph_p-19
FAIL
877.52
DWs-sat-10-23-1
FAIL
877.6
genbuf10b4n.sat
FAIL
877.61
input_pnpi8042_moudep.c
FAIL
877.62
incrementer-enc02-uniform-depth-58
FAIL
877.62
DW-unsat-19-42-1
FAIL
877.62
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
877.62
DW-sat-19-46-1
FAIL
877.68
network_irda_miniport_nscirda_comm.c
FAIL
877.7
qshifter_7
FAIL
877.71
mult_bool_matrix_17_17_17.sat
FAIL
877.72
sortnetsort9.v.stepl.005
FAIL
877.72
k_branch_n-12
FAIL
877.72
assertion9_0_7
FAIL
877.72
possibility8_0_7
FAIL
877.72
stmt41_738_749
FAIL
877.81
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp
FAIL
877.81
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
877.81
adder-10-sat
FAIL
877.81
ken.flash^08.C-d4
FAIL
877.81
stmt17_70_90
FAIL
877.81
mult_bool_matrix_10_9_11.sat
FAIL
877.82
possibility7_0_6
FAIL
877.82
assertion2_0_6
FAIL
877.82
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.asp
FAIL
877.87
test2_quant_squaring2
FAIL
877.91
CM-unsat-07-01-06-2
FAIL
877.91
adder-12-unsat
FAIL
877.91
genbuf9b4n.sat
FAIL
877.92
small-swap2-fixpoint-4
FAIL
877.99
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
878
JP-unsat-02-06-3
FAIL
878.01
possibility4_0_5
FAIL
878.01
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
878.01
test3_quant_squaring4
FAIL
878.01
ring_r6_ser--opt-17_
FAIL
878.08
c5_BMC_p2_k64
FAIL
878.11
audio_ddksynth_csynth2.cpp
FAIL
878.11
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.asp
FAIL
878.12
driver_a9n.unsat
FAIL
878.21
small-synabs-fixpoint-9
FAIL
878.22
rankfunc5_unsigned_64
FAIL
878.22
test1_quant_squaring3
FAIL
878.22
rankfunc33_signed_32
FAIL
878.3
cycle_sched_6_7_1.unsat
FAIL
878.31
small-swap1-fixpoint-3
FAIL
878.31
k8_2_3
FAIL
878.32
ltl2dpa_C26_comp2_REAL.unsat
FAIL
878.41
rankfunc14_signed_64
FAIL
878.41
Umbrella_tbm_05.tex.module.000039
FAIL
878.42
incrementer-enc08-uniform-depth-33
FAIL
878.42
sdlx-fixpoint-3
FAIL
878.42
driver_a9n.sat
FAIL
878.5
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.asp
FAIL
878.5
cache-coherence-2-fixpoint-6
FAIL
878.6
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
878.61
assertion2_0_3
FAIL
878.62
JP-sat-03-08-5
FAIL
878.69
ken.oop^2.C-d4
FAIL
878.7
k_ph_p-12
FAIL
878.71
ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.asp
FAIL
878.71
ev-pr-8x8-19-7-0-1-2-lg
FAIL
878.71
rankfunc13_unsigned_64
FAIL
878.71
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
878.72
ev-pr-4x4-15-3-0-0-1-s
FAIL
878.72
test2_quant_squaring3
FAIL
878.81
sortnetsort9.v.stepl.007
FAIL
878.91
genbuf9b4n.unsat
FAIL
878.92
genbuf10b4n.unsat
FAIL
878.92
assertion5_0_9
FAIL
878.92
k5_2_3
FAIL
878.92
DWs-sat-10-25-1
FAIL
879
mult_bool_matrix_10_9_11.unsat
FAIL
879.02
ci.e#1.a#3.E#40.A#60.c#408.w#4.s#3.asp
FAIL
879.06
C880.blif_0.10_1.00_0_0_inp_exact
FAIL
879.1
klieber2017q-100-25-eq
FAIL
879.11
C499.blif_0.10_0.20_0_0_out_exact
FAIL
879.21
klieber2017q-092-23-eq
FAIL
879.21
klieber2017q-084-21-eq
FAIL
879.22
klieber2017q-078-19-eq
FAIL
879.31
cube_c7_ser--opt-24_
FAIL
879.32
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
879.32
DW-sat-19-44-1
FAIL
879.48
klieber2017q-096-24-t1
FAIL
879.51
klieber2017q-088-22-eq
FAIL
879.51
assertion2_0_5
FAIL
879.52
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
879.61
C499.blif_0.10_0.20_0_1_out_exact
FAIL
879.62
emptyroom_e4_ser--opt-44_
FAIL
879.62
klieber2017q-096-24-eq
FAIL
879.67
klieber2017q-076-19-eq
FAIL
879.7
klieber2017q-108-27-eq
FAIL
879.71
klieber2017q-074-18-eq
FAIL
879.72
klieber2017q-082-20-eq
FAIL
879.8
klieber2017q-082-20-t1
FAIL
879.8
klieber2017q-086-21-eq
FAIL
879.81
sortnetsort10.v.stepl.005
FAIL
879.81
klieber2017q-104-26-eq
FAIL
879.84
klieber2017q-112-28-eq
FAIL
879.92
klieber2017q-080-20-eq
FAIL
879.98
C499.blif_0.10_1.00_0_0_out_exact
FAIL
879.99
assertion3_0_6
FAIL
880.01
klieber2017q-116-29-eq
FAIL
880.04
klieber2017q-074-18-t1
FAIL
880.2
klieber2017q-100-25-t1
FAIL
881.62
assertion7_0_4
FAIL
883.84
Contact
|
Organization
|
Links
|
Citing QBFLIB