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
PortfolioGhostQQfunQuAbSQute___pfs
QBFEVAL'18 - Prenex non-CNF Track
Instance
Result
Time
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
4.58
CM-sat-02-01-07-3
SAT
4.59
query21_reachqu_1133
SAT
4.61
klieber2017q-112-28-t1
UNSAT
4.62
pg-hkb-2
UNSAT
4.63
query71_query15_1133
UNSAT
4.63
query04_query03_1133
UNSAT
4.64
query64_query31_1133
UNSAT
4.66
query30_eequery_1133
SAT
4.66
bs128n.unsat
UNSAT
4.66
6s318r_c0to15.unsat
UNSAT
4.67
stay22n.unsat
UNSAT
4.72
pg-hkb-3
UNSAT
4.76
query50_query49_1133
UNSAT
4.78
ntrivil_query54_1133
SAT
4.78
SR-unsat-02-01-06-1
UNSAT
4.79
klieber2017q-078-19-t1
UNSAT
4.91
k_ph_n-21
SAT
4.95
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
5.01
driver_d9n.unsat
UNSAT
5.11
query44_query57_1133
UNSAT
5.19
ev-pr-4x4-11-3-0-0-1-lg
SAT
5.3
query51_query48_1133
UNSAT
5.36
ev-pr-4x4-13-3-0-0-1-lg
SAT
5.51
CM-sat-03-01-07-3
SAT
5.52
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
5.52
random-qcir-1000-50-295
FAIL
5.59
random-qcir-1000-50-98
FAIL
5.65
random-qcir-1000-50-361
FAIL
5.65
k0300663.h.oe
FAIL
5.66
k0225744.connected.oe
FAIL
5.68
klieber2017q-084-21-t1
FAIL
5.68
nreachq_query02_1344
FAIL
5.68
k0201058.c.oe
FAIL
5.68
jctc1-pass
FAIL
5.69
random-qcir-1000-50-898
FAIL
5.69
JP-sat-02-07-3
SAT
5.69
jctc13-fail
FAIL
5.7
klieber2017q-108-27-t1
FAIL
5.7
p20-1.pddl_planlen=24
FAIL
5.7
mult_bool_matrix_2_3_30.unsat
FAIL
5.7
klieber2017q-100-25-eq
FAIL
5.7
k0026150.h.oe
FAIL
5.7
amba2f9n.unsat
FAIL
5.7
small-swap2-fixpoint-4
FAIL
5.71
random-qcir-1000-50-940
FAIL
5.71
test2_quant_squaring2
FAIL
5.71
jctc8-pass
FAIL
5.71
rankfunc17_unsigned_16
FAIL
5.72
k0225418.v.oe
FAIL
5.72
bs128n.sat
FAIL
5.72
k0300663.v.oe
FAIL
5.72
klieber2017q-086-21-eq
FAIL
5.73
klieber2017q-096-24-t1
FAIL
5.73
klieber2017q-076-19-eq
FAIL
5.73
mult_bool_matrix_4_5_5.unsat
FAIL
5.73
klieber2017q-108-27-eq
FAIL
5.73
rankfunc13_unsigned_64
FAIL
5.73
random-qcir-1000-50-857
FAIL
5.73
sortnetsort10.v.stepl.005
FAIL
5.73
k0225682.c.oe
FAIL
5.73
random-qcir-1000-50-846
FAIL
5.74
test2_quant_squaring3
FAIL
5.74
test3_quant_squaring2
FAIL
5.74
random-qcir-1000-50-393
FAIL
5.74
klieber2017q-100-25-t1
FAIL
5.75
query33_query71_1344
FAIL
5.75
genbuf5b4n.unsat
FAIL
5.75
random-qcir-1000-50-754
FAIL
5.75
klieber2017q-074-18-eq
FAIL
5.75
random-qcir-1000-50-793
FAIL
5.75
k0225744.s.oe
FAIL
5.75
random-qcir-1000-50-255
FAIL
5.75
random-qcir-1000-50-970
FAIL
5.75
klieber2017q-082-20-eq
FAIL
5.76
chess_solving_mate_in_5_2012_NED-CH-18A_11
FAIL
5.76
stay24n.sat
FAIL
5.76
klieber2017q-078-19-eq
FAIL
5.76
mult_bool_matrix_2_3_30.sat
FAIL
5.76
driver_a9y.unsat
FAIL
5.76
random-qcir-1000-50-456
FAIL
5.76
klieber2017q-116-29-t1
FAIL
5.76
k0026150.connected.oe
FAIL
5.76
cycle_sched_6_2_1.sat
FAIL
5.76
k0300663.s.oe
FAIL
5.76
query09_trivial_1344
FAIL
5.76
k0226271.c.oe
FAIL
5.76
ken.oop^2.C-d4
FAIL
5.77
k0026150.v.oe
FAIL
5.77
random-qcir-1000-50-658
FAIL
5.77
random-qcir-1000-50-68
FAIL
5.77
query03_query57_1344
FAIL
5.77
klieber2017q-104-26-t1
FAIL
5.77
jctc4-fail
FAIL
5.77
k0225418.s.oe
FAIL
5.77
klieber2017q-096-24-eq
FAIL
5.78
k_ph_p-12
FAIL
5.78
random-qcir-1000-50-983
FAIL
5.78
random-qcir-1000-50-545
FAIL
5.78
genbuf5b4n.sat
FAIL
5.78
query08_query26_1344
FAIL
5.78
audio_ddksynth_csynth2.cpp
FAIL
5.78
ltl2dpa_C26_comp3_REAL.unsat
FAIL
5.78
random-qcir-1000-50-267
FAIL
5.78
k0206272.h.oe
FAIL
5.78
k0026150.s.oe
FAIL
5.78
random-qcir-1000-50-275
FAIL
5.78
load_3c_comp_comp7_REAL.unsat
FAIL
5.78
incrementer-enc08-uniform-depth-33
FAIL
5.79
klieber2017q-116-29-eq
FAIL
5.79
k0206272.v.oe
FAIL
5.79
mult_bool_matrix_4_5_5.sat
FAIL
5.79
random-qcir-1000-50-930
FAIL
5.79
genbuf9b4n.unsat
FAIL
5.79
random-qcir-1000-50-473
FAIL
5.79
klieber2017q-080-20-t1
FAIL
5.79
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
5.8
jctc6-pass
FAIL
5.8
k0206272.connected.oe
FAIL
5.8
chess_solving_mate_in_2_2011_ISC-7B_01
FAIL
5.8
klieber2017q-104-26-eq
FAIL
5.8
random-qcir-1000-50-428
FAIL
5.8
ltl2dpa_C26_comp2_REAL.unsat
FAIL
5.8
load_full_3_comp3_REAL.sat
FAIL
5.8
k0225418.h.oe
FAIL
5.81
k0225418.connected.oe
FAIL
5.81
k0206272.s.oe
FAIL
5.81
JP-sat-02-08-3
FAIL
5.81
random-qcir-1000-50-743
FAIL
5.81
JP-sat-02-07-4
FAIL
5.81
klieber2017q-074-18-t1
FAIL
5.81
random-qcir-1000-50-134
FAIL
5.81
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
5.81
query48_query42_1344
FAIL
5.81
query42_query64_1344
FAIL
5.82
gb_s2_r2_comp3_REAL.sat
FAIL
5.82
k0225744.v.oe
FAIL
5.82
cycle_sched_6_2_1.unsat
FAIL
5.82
ltl2dpa_C26_comp3_REAL.sat
FAIL
5.82
rankfunc33_signed_32
FAIL
5.82
query49_query58_1344
FAIL
5.82
klieber2017q-080-20-eq
FAIL
5.82
klieber2017q-092-23-eq
FAIL
5.82
sortnetsort9.v.stepl.007
FAIL
5.82
amba2f9n.sat
FAIL
5.83
incrementer-enc02-uniform-depth-58
FAIL
5.83
k0300663.connected.oe
FAIL
5.83
SR-unsat-02-01-05-2
FAIL
5.83
ev-pr-6x6-9-5-0-1-2-lg
FAIL
5.83
chess_solving_mate_in_3_1999_WCSC-23_05
FAIL
5.83
incrementer-enc07-uniform-depth-25
FAIL
5.84
query08_query64_1344
FAIL
5.84
chess_solving_mate_in_4_1984_GBR-CH-5_04
FAIL
5.84
jctc16-vals-0,2-pass
FAIL
5.84
chess_solving_mate_in_3_2009_FIN-CH-30_04
FAIL
5.84
klieber2017q-092-23-t1
FAIL
5.84
chess_solving_mate_in_2_1983_FIN-CH-4_01
FAIL
5.84
gb_s2_r2_comp3_REAL.unsat
FAIL
5.85
chess_solving_mate_in_6_2016_RUS-CH_15
FAIL
5.85
load_full_3_comp3_REAL.unsat
FAIL
5.85
sortnetsort9.AE.stepl.012
FAIL
5.85
beemldelec4b1_c0to15.unsat
FAIL
5.86
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10
FAIL
5.86
jctc10-fail
FAIL
5.86
query44_query58_1344
FAIL
5.86
filesys_smbmrx_cvsndrcv.c
FAIL
5.86
6s318r_c0to31.sat
FAIL
5.86
chess_solving_mate_in_4_1999_GER-CH-23-6_14
FAIL
5.86
query49_query64_1133
FAIL
5.87
chess_solving_mate_in_4_2009_SEROCK-OPEN_09
FAIL
5.87
chess_solving_mate_in_3_2016_BEL-CH-23A_02
FAIL
5.87
chess_composing_6_template_06
FAIL
5.87
chess_solving_mate_in_6_1998_OST-CH-1_15
FAIL
5.87
chess_composing_6_template_04
FAIL
5.87
nreachq_reachqu_2233
FAIL
5.88
genbuf10b4y.unsat
FAIL
5.88
chess_solving_mate_in_5_1996_UKR-CH-10_15
FAIL
5.89
chess_solving_mate_in_7_2009_POL-CH-33_15
FAIL
5.89
pg-hkb-4
UNSAT
5.89
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03
FAIL
5.89
chess_solving_mate_in_7_2016_BEL-CH-23A_03
FAIL
5.9
SR-sat-02-01-06-2
FAIL
5.9
random-qcir-1000-50-441
FAIL
5.91
chess_solving_mate_in_5_1984_FIN-CH-5_09
FAIL
5.91
input_pnpi8042_moudep.c
FAIL
5.93
k0302060.c.oe
FAIL
5.93
klieber2017q-086-21-t1
FAIL
5.93
query64_query58_1344
FAIL
5.95
network_irda_miniport_nscirda_comm.c
FAIL
5.95
k0225744.h.oe
FAIL
5.95
chess_composing_6_template_01
FAIL
5.96
query42_query57_1344
FAIL
5.96
sdlx-fixpoint-3
FAIL
5.96
chess_solving_mate_in_2_1996_FIN-CH-17_03
FAIL
5.96
chess_solving_mate_in_7_2005_GER-CH-29-12_15
FAIL
5.96
jctc9-pass
FAIL
5.97
k0225418.c.oe
FAIL
5.98
p20-5.pddl_planlen=32
FAIL
5.98
sortnetsort9.v.stepl.005
FAIL
5.99
query64_query55_1344
FAIL
5.99
ev-pr-6x6-11-5-0-1-2-lg
FAIL
5.99
chess_solving_mate_in_6_2011_SRB-CH_15
FAIL
5.99
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
FAIL
6
chess_solving_mate_in_7_2011_SVK-CH-19_15
FAIL
6
ken.flash^08.C-d4
FAIL
6
klieber2017q-112-28-eq
FAIL
6
chess_solving_mate_in_8_2011_BEL-CH-19A_03
FAIL
6.02
chess_solving_mate_in_9_2003_RUS-CH_15
FAIL
6.04
chess_solving_mate_in_2_2012_GER-CH-36-19_03
FAIL
6.05
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
UNSAT
6.15
CM-sat-03-01-06-4
SAT
6.58
SR-sat-02-01-07-2
SAT
6.9
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
6.98
nreachq_reachqu_2133
FAIL
7.04
DW-sat-06-20-1
SAT
7.34
CM-sat-04-01-06-3
SAT
7.48
JP-unsat-02-06-3
UNSAT
8.12
k_branch_p-10
UNSAT
8.45
DW-sat-08-22-1
SAT
9.21
DW-sat-08-23-1
SAT
9.34
oski3ub1i_c0to63.unsat
UNSAT
9.47
CM-sat-04-01-06-4
SAT
9.69
p20-20.pddl_planlen=23
FAIL
9.7
DWs-sat-10-23-1
SAT
11.88
CM-sat-04-01-07-3
SAT
12.71
jctc2-pass
SAT
12.84
DWs-unsat-07-16-1
UNSAT
13.68
DWs-sat-10-25-1
SAT
13.72
DWs-sat-12-28-1
SAT
19.33
DWs-unsat-08-17-1
UNSAT
21.19
DWs-unsat-08-18-1
UNSAT
22.15
DW-sat-08-24-1
SAT
24.32
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
SAT
32.68
k_branch_p-11
UNSAT
34.85
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
40.97
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
UNSAT
41.59
SR-sat-02-01-06-3
SAT
41.73
DWs-sat-15-35-1
SAT
44.64
DWs-unsat-09-19-1
UNSAT
46.38
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
SAT
46.85
pipesnotankage18_8
FAIL
58.3
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
SAT
62.52
CM-sat-07-01-07-3
SAT
67.08
cnt14
SAT
71.95
jctc18-vals-0,2-pass
SAT
72.57
DW-sat-09-26-1
SAT
81.36
CM-sat-07-01-06-4
SAT
86.46
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
SAT
100.05
pg-hkb-5
UNSAT
103.32
DW-unsat-09-22-1
UNSAT
117.34
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
SAT
118.15
jctc17-vals-0,2-pass
SAT
118.78
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
SAT
135.16
SR-sat-03-01-07-2
SAT
138.4
SR-sat-03-01-08-2
SAT
144.45
k_branch_n-10
SAT
151.92
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
155.36
DWs-sat-10-24-1
SAT
157.23
JP-unsat-03-08-3
UNSAT
162.15
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
SAT
166.8
DWs-unsat-11-23-1
UNSAT
175.06
pg-hkb-6
FAIL
208.15
JP-unsat-03-07-4
UNSAT
210.25
CM-sat-07-01-06-3
SAT
213
CM-unsat-07-01-06-2
UNSAT
255.01
DW-unsat-10-25-1
UNSAT
257.86
pg-hkb-7
UNSAT
297.73
DWs-unsat-11-24-1
UNSAT
313.03
k_branch_p-16
UNSAT
347.37
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
UNSAT
358.01
DWs-unsat-12-25-1
UNSAT
394.36
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
SAT
539.37
DW-unsat-11-26-1
UNSAT
680.02
ev-pr-4x4-15-3-0-0-1-s
FAIL
696.74
DW-unsat-11-27-1
UNSAT
796.9
SR-unsat-03-01-06-2
UNSAT
873.93
jctc5-fail
FAIL
900.01
JP-sat-03-08-4
FAIL
900.01
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
900.01
pg-hkb-19
FAIL
900.01
DWs-unsat-13-28-1
FAIL
900.01
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900.01
cnt16r
FAIL
900.01
chess_composing_8_template_38
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900.01
pg-hkb-10
FAIL
900.02
JP-sat-03-09-4
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900.02
pg-hkb-14
FAIL
900.02
pg-hkb-18
FAIL
900.02
pg-hkb-24
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900.02
test1_quant_squaring3
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900.02
chess_composing_8_template_02
FAIL
900.02
pg-hkb-12
FAIL
900.02
pg-hkb-23
FAIL
900.03
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.asp
FAIL
900.03
mv16y.sat
FAIL
900.03
jctc14-unrolled-fail
FAIL
900.03
pg-hkb-20
FAIL
900.03
pg-hkb-17
FAIL
900.03
jctc7-pass
FAIL
900.04
pg-hkb-15
FAIL
900.04
jctc15-unrolled-fail
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900.04
pg-hkb-13
FAIL
900.05
qshifter_7
FAIL
900.05
oski3ub1i_c0to63.sat
FAIL
900.05
chess_composing_8_template_13
FAIL
900.05
chess_composing_8_template_43
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900.06
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900.06
pg-hkb-26
FAIL
900.06
pg-hkb-9
FAIL
900.06
pg-hkb-16
FAIL
900.06
pipesnotankage14_10
FAIL
900.06
small-swap1-fixpoint-3
FAIL
900.06
jctc3-vals-0,2-pass
FAIL
900.07
pg-hkb-8
FAIL
900.07
pg-hkb-25
FAIL
900.07
k_branch_n-12
FAIL
900.07
jctc11-pass
FAIL
900.08
k_ph_p-19
FAIL
900.08
JP-unsat-03-08-5
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900.08
JP-unsat-03-09-4
FAIL
900.09
pg-hkb-21
FAIL
900.09
pg-hkb-22
FAIL
900.09
pg-hkb-11
FAIL
900.09
beemldelec4b1_c0to15.sat
FAIL
900.09
chess_composing_8_template_42
FAIL
900.09
Contact
|
Organization
|
Links
|
Citing QBFLIB