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'18 - Prenex non-CNF Track
Instance
Result
Time
SR-unsat-02-01-06-1
UNSAT
0
pg-hkb-3
UNSAT
0
query21_reachqu_1133
SAT
0
k_ph_n-21
SAT
0
klieber2017q-108-27-t1
UNSAT
0
query30_eequery_1133
SAT
0
bs128n.unsat
UNSAT
0
query50_query49_1133
UNSAT
0
ntrivil_query54_1133
SAT
0
query51_query48_1133
UNSAT
0
stay24n.sat
SAT
0
6s318r_c0to15.unsat
UNSAT
0
driver_d9n.unsat
UNSAT
0
stay22n.unsat
UNSAT
0
query71_query15_1133
UNSAT
0
pg-hkb-2
UNSAT
0
query64_query31_1133
UNSAT
0
query04_query03_1133
UNSAT
0
jctc6-pass
SAT
0.53
pg-hkb-4
UNSAT
0.58
CM-sat-02-01-07-3
SAT
0.61
query44_query57_1133
UNSAT
0.65
jctc8-pass
SAT
0.93
jctc13-fail
UNSAT
1.07
oski3ub1i_c0to63.unsat
UNSAT
1.51
beemldelec4b1_c0to15.unsat
UNSAT
1.53
jctc16-vals-0,2-pass
SAT
1.68
jctc1-pass
SAT
2.22
jctc4-fail
UNSAT
2.28
bs128n.sat
SAT
3.9
klieber2017q-092-23-t1
UNSAT
4.73
jctc2-pass
SAT
6.15
pg-hkb-5
UNSAT
6.39
incrementer-enc07-uniform-depth-25
UNSAT
6.72
query49_query64_1133
UNSAT
6.74
k0206272.s.oe
SAT
7.2
klieber2017q-078-19-t1
UNSAT
7.75
CM-sat-03-01-07-3
SAT
9.98
filesys_smbmrx_cvsndrcv.c
UNSAT
10.99
chess_solving_mate_in_2_2012_GER-CH-36-19_03
SAT
14
chess_solving_mate_in_2_1996_FIN-CH-17_03
SAT
16.28
klieber2017q-084-21-t1
UNSAT
16.51
query09_trivial_1344
SAT
24.17
DWs-unsat-07-16-1
UNSAT
31.07
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
34.36
k0201058.c.oe
SAT
59.79
SR-sat-02-01-07-2
SAT
63.29
ev-pr-4x4-13-3-0-0-1-lg
SAT
70.18
pg-hkb-6
UNSAT
71.45
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
SAT
75.93
JP-sat-02-08-3
SAT
93.5
SR-unsat-02-01-05-2
UNSAT
101.78
klieber2017q-086-21-t1
UNSAT
132.06
chess_solving_mate_in_2_2011_ISC-7B_01
SAT
136.04
DWs-unsat-08-18-1
UNSAT
149.58
chess_solving_mate_in_2_1983_FIN-CH-4_01
SAT
193.09
klieber2017q-074-18-t1
UNSAT
218.47
k0225744.s.oe
SAT
220.36
k0206272.h.oe
SAT
239.98
k0026150.h.oe
SAT
254.64
SR-sat-02-01-06-2
SAT
257.71
amba2f9n.unsat
UNSAT
322.45
ev-pr-4x4-11-3-0-0-1-lg
SAT
326.49
random-qcir-1000-50-793
UNSAT
390.08
k_branch_p-10
UNSAT
393.82
DW-sat-08-24-1
SAT
421.15
amba2f9n.sat
SAT
426.35
pg-hkb-7
UNSAT
429.99
k0206272.v.oe
SAT
433.27
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
462.06
k0226271.c.oe
SAT
484
random-qcir-1000-50-255
UNSAT
570.23
JP-sat-02-07-3
SAT
575.74
DWs-unsat-09-19-1
UNSAT
665.63
DW-unsat-10-25-1
UNSAT
750.47
mv16y.sat
SAT
751.48
DWs-unsat-08-17-1
UNSAT
755.93
klieber2017q-080-20-t1
UNSAT
827.78
k0026150.s.oe
UNSAT
833.17
k0300663.s.oe
UNSAT
852.31
DW-sat-08-22-1
FAIL
900
DWs-sat-10-23-1
FAIL
900
SR-sat-03-01-07-2
FAIL
900
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10
FAIL
900
JP-sat-02-07-4
FAIL
900
mult_bool_matrix_2_3_30.sat
FAIL
900
chess_composing_8_template_43
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900
k0225418.s.oe
FAIL
900
k0300663.connected.oe
FAIL
900
pg-hkb-23
FAIL
900
query42_query57_1344
FAIL
900
pipesnotankage18_8
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
900
6s318r_c0to31.sat
FAIL
900
k_branch_n-10
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
900.01
random-qcir-1000-50-98
FAIL
900.01
klieber2017q-112-28-t1
FAIL
900.01
chess_solving_mate_in_3_1999_WCSC-23_05
FAIL
900.01
k0225682.c.oe
FAIL
900.01
k0225744.h.oe
FAIL
900.01
chess_composing_6_template_04
FAIL
900.01
CM-sat-04-01-06-3
FAIL
900.01
JP-sat-03-09-4
FAIL
900.01
DW-unsat-09-22-1
FAIL
900.01
random-qcir-1000-50-134
FAIL
900.01
DWs-unsat-11-23-1
FAIL
900.01
sortnetsort9.v.stepl.007
FAIL
900.01
sdlx-fixpoint-3
FAIL
900.01
chess_solving_mate_in_4_1999_GER-CH-23-6_14
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
FAIL
900.01
query64_query55_1344
FAIL
900.01
random-qcir-1000-50-970
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.asp
FAIL
900.01
pg-hkb-11
FAIL
900.01
jctc18-vals-0,2-pass
FAIL
900.01
chess_solving_mate_in_6_1998_OST-CH-1_15
FAIL
900.01
jctc10-fail
FAIL
900.01
gb_s2_r2_comp3_REAL.sat
FAIL
900.01
k_branch_n-12
FAIL
900.01
random-qcir-1000-50-658
FAIL
900.01
qshifter_7
FAIL
900.01
chess_solving_mate_in_4_2009_SEROCK-OPEN_09
FAIL
900.01
chess_solving_mate_in_4_1984_GBR-CH-5_04
FAIL
900.01
random-qcir-1000-50-473
FAIL
900.02
cnt14
FAIL
900.02
jctc14-unrolled-fail
FAIL
900.02
random-qcir-1000-50-940
FAIL
900.02
chess_composing_8_template_13
FAIL
900.02
random-qcir-1000-50-930
FAIL
900.02
k_ph_p-12
FAIL
900.02
k_ph_p-19
FAIL
900.02
chess_composing_8_template_42
FAIL
900.02
cnt16r
FAIL
900.02
k_branch_p-11
FAIL
900.02
random-qcir-1000-50-441
FAIL
900.02
chess_solving_mate_in_3_2009_FIN-CH-30_04
FAIL
900.02
load_full_3_comp3_REAL.sat
FAIL
900.02
klieber2017q-104-26-t1
FAIL
900.02
klieber2017q-100-25-eq
FAIL
900.02
klieber2017q-096-24-t1
FAIL
900.02
mult_bool_matrix_2_3_30.unsat
FAIL
900.02
pg-hkb-25
FAIL
900.02
nreachq_reachqu_2233
FAIL
900.02
pg-hkb-22
FAIL
900.02
klieber2017q-076-19-eq
FAIL
900.02
pg-hkb-19
FAIL
900.02
pg-hkb-12
FAIL
900.02
load_3c_comp_comp7_REAL.unsat
FAIL
900.02
klieber2017q-112-28-eq
FAIL
900.02
CM-sat-04-01-06-4
FAIL
900.02
ken.flash^08.C-d4
FAIL
900.02
query64_query58_1344
FAIL
900.02
sortnetsort10.v.stepl.005
FAIL
900.02
DW-unsat-11-26-1
FAIL
900.02
rankfunc17_unsigned_16
FAIL
900.02
genbuf9b4n.unsat
FAIL
900.02
incrementer-enc02-uniform-depth-58
FAIL
900.02
chess_composing_6_template_01
FAIL
900.02
jctc11-pass
FAIL
900.03
k0225418.h.oe
FAIL
900.03
pg-hkb-21
FAIL
900.03
pg-hkb-17
FAIL
900.03
random-qcir-1000-50-857
FAIL
900.03
incrementer-enc08-uniform-depth-33
FAIL
900.03
JP-unsat-03-08-5
FAIL
900.03
k0225744.connected.oe
FAIL
900.03
random-qcir-1000-50-275
FAIL
900.03
jctc3-vals-0,2-pass
FAIL
900.03
chess_solving_mate_in_9_2003_RUS-CH_15
FAIL
900.03
chess_solving_mate_in_8_2011_BEL-CH-19A_03
FAIL
900.03
query42_query64_1344
FAIL
900.03
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900.03
pipesnotankage14_10
FAIL
900.03
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900.03
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
FAIL
900.03
CM-sat-07-01-06-4
FAIL
900.03
klieber2017q-078-19-eq
FAIL
900.03
klieber2017q-092-23-eq
FAIL
900.03
DWs-unsat-11-24-1
FAIL
900.03
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
900.03
CM-unsat-07-01-06-2
FAIL
900.03
input_pnpi8042_moudep.c
FAIL
900.03
test1_quant_squaring3
FAIL
900.03
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900.03
DW-sat-08-23-1
FAIL
900.03
mult_bool_matrix_4_5_5.unsat
FAIL
900.04
load_full_3_comp3_REAL.unsat
FAIL
900.04
random-qcir-1000-50-545
FAIL
900.04
genbuf5b4n.unsat
FAIL
900.04
CM-sat-07-01-06-3
FAIL
900.04
JP-unsat-03-08-3
FAIL
900.04
chess_solving_mate_in_7_2009_POL-CH-33_15
FAIL
900.04
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900.04
query08_query64_1344
FAIL
900.04
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
900.04
ken.oop^2.C-d4
FAIL
900.04
k0026150.connected.oe
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
FAIL
900.04
random-qcir-1000-50-393
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900.04
random-qcir-1000-50-428
FAIL
900.04
random-qcir-1000-50-295
FAIL
900.04
query08_query26_1344
FAIL
900.04
network_irda_miniport_nscirda_comm.c
FAIL
900.04
DWs-sat-15-35-1
FAIL
900.04
jctc17-vals-0,2-pass
FAIL
900.04
chess_composing_8_template_38
FAIL
900.04
jctc5-fail
FAIL
900.04
JP-unsat-03-07-4
FAIL
900.04
chess_solving_mate_in_5_1984_FIN-CH-5_09
FAIL
900.04
k0225418.c.oe
FAIL
900.05
pg-hkb-24
FAIL
900.05
klieber2017q-074-18-eq
FAIL
900.05
random-qcir-1000-50-267
FAIL
900.05
query03_query57_1344
FAIL
900.05
k0225418.connected.oe
FAIL
900.05
query48_query42_1344
FAIL
900.05
klieber2017q-082-20-eq
FAIL
900.05
nreachq_query02_1344
FAIL
900.05
p20-5.pddl_planlen=32
FAIL
900.05
DWs-sat-10-25-1
FAIL
900.05
chess_solving_mate_in_6_2016_RUS-CH_15
FAIL
900.05
pg-hkb-16
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900.05
k0300663.v.oe
FAIL
900.06
chess_composing_8_template_02
FAIL
900.06
query44_query58_1344
FAIL
900.06
pg-hkb-18
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
900.06
pg-hkb-14
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
FAIL
900.06
chess_solving_mate_in_3_2016_BEL-CH-23A_02
FAIL
900.06
CM-sat-04-01-07-3
FAIL
900.06
pg-hkb-8
FAIL
900.06
pg-hkb-10
FAIL
900.06
CM-sat-03-01-06-4
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
FAIL
900.06
jctc7-pass
FAIL
900.06
DWs-sat-12-28-1
FAIL
900.06
k0225418.v.oe
FAIL
900.06
ltl2dpa_C26_comp2_REAL.unsat
FAIL
900.06
random-qcir-1000-50-898
FAIL
900.06
klieber2017q-116-29-t1
FAIL
900.06
klieber2017q-108-27-eq
FAIL
900.06
ev-pr-4x4-15-3-0-0-1-s
FAIL
900.06
JP-sat-03-08-4
FAIL
900.06
ev-pr-6x6-9-5-0-1-2-lg
FAIL
900.06
random-qcir-1000-50-846
FAIL
900.06
JP-unsat-03-09-4
FAIL
900.06
random-qcir-1000-50-361
FAIL
900.06
JP-unsat-02-06-3
FAIL
900.06
chess_solving_mate_in_5_1996_UKR-CH-10_15
FAIL
900.06
beemldelec4b1_c0to15.sat
FAIL
900.06
rankfunc33_signed_32
FAIL
900.06
chess_solving_mate_in_5_2012_NED-CH-18A_11
FAIL
900.06
chess_solving_mate_in_6_2011_SRB-CH_15
FAIL
900.06
pg-hkb-26
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
FAIL
900.07
chess_solving_mate_in_7_2016_BEL-CH-23A_03
FAIL
900.07
small-swap1-fixpoint-3
FAIL
900.07
test2_quant_squaring3
FAIL
900.07
random-qcir-1000-50-754
FAIL
900.07
random-qcir-1000-50-68
FAIL
900.07
jctc15-unrolled-fail
FAIL
900.07
p20-1.pddl_planlen=24
FAIL
900.07
k0302060.c.oe
FAIL
900.07
k0225744.v.oe
FAIL
900.07
jctc9-pass
FAIL
900.07
nreachq_reachqu_2133
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900.07
SR-sat-02-01-06-3
FAIL
900.07
cycle_sched_6_2_1.unsat
FAIL
900.07
cycle_sched_6_2_1.sat
FAIL
900.07
query33_query71_1344
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900.07
pg-hkb-13
FAIL
900.07
pg-hkb-15
FAIL
900.07
query49_query58_1344
FAIL
900.07
random-qcir-1000-50-456
FAIL
900.07
genbuf5b4n.sat
FAIL
900.08
sortnetsort9.v.stepl.005
FAIL
900.08
genbuf10b4y.unsat
FAIL
900.08
klieber2017q-086-21-eq
FAIL
900.08
k0300663.h.oe
FAIL
900.08
klieber2017q-080-20-eq
FAIL
900.08
test3_quant_squaring2
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900.08
random-qcir-1000-50-983
FAIL
900.08
CM-sat-07-01-07-3
FAIL
900.08
chess_composing_6_template_06
FAIL
900.08
DWs-unsat-13-28-1
FAIL
900.08
DWs-sat-10-24-1
FAIL
900.08
klieber2017q-116-29-eq
FAIL
900.08
klieber2017q-104-26-eq
FAIL
900.08
SR-unsat-03-01-06-2
FAIL
900.08
chess_solving_mate_in_7_2011_SVK-CH-19_15
FAIL
900.08
gb_s2_r2_comp3_REAL.unsat
FAIL
900.08
p20-20.pddl_planlen=23
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
FAIL
900.08
DW-sat-06-20-1
FAIL
900.08
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03
FAIL
900.08
sortnetsort9.AE.stepl.012
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900.08
mult_bool_matrix_4_5_5.sat
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
FAIL
900.08
random-qcir-1000-50-743
FAIL
900.09
test2_quant_squaring2
FAIL
900.09
pg-hkb-9
FAIL
900.09
k_branch_p-16
FAIL
900.09
k0026150.v.oe
FAIL
900.09
k0206272.connected.oe
FAIL
900.09
small-swap2-fixpoint-4
FAIL
900.09
DW-unsat-11-27-1
FAIL
900.09
oski3ub1i_c0to63.sat
FAIL
900.09
ltl2dpa_C26_comp3_REAL.unsat
FAIL
900.09
rankfunc13_unsigned_64
FAIL
900.09
klieber2017q-096-24-eq
FAIL
900.09
audio_ddksynth_csynth2.cpp
FAIL
900.09
DWs-unsat-12-25-1
FAIL
900.09
DW-sat-09-26-1
FAIL
900.09
driver_a9y.unsat
FAIL
900.09
SR-sat-03-01-08-2
FAIL
900.09
chess_solving_mate_in_7_2005_GER-CH-29-12_15
FAIL
900.09
klieber2017q-100-25-t1
FAIL
900.1
ltl2dpa_C26_comp3_REAL.sat
FAIL
900.1
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900.1
pg-hkb-20
FAIL
900.1
Contact
|
Organization
|
Links
|
Citing QBFLIB