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___pf3
QBFEVAL'18 - Prenex non-CNF Track
Instance
Result
Time
query71_query15_1133
UNSAT
4.54
query30_eequery_1133
SAT
4.59
pg-hkb-2
UNSAT
4.61
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
4.61
query04_query03_1133
UNSAT
4.61
klieber2017q-078-19-t1
UNSAT
4.64
query64_query31_1133
UNSAT
4.66
klieber2017q-112-28-t1
UNSAT
4.66
SR-unsat-02-01-06-1
UNSAT
4.69
ntrivil_query54_1133
SAT
4.7
stay22n.unsat
UNSAT
4.71
query50_query49_1133
UNSAT
4.73
bs128n.unsat
UNSAT
4.73
6s318r_c0to15.unsat
UNSAT
4.74
pg-hkb-3
UNSAT
4.79
query21_reachqu_1133
SAT
4.8
CM-sat-02-01-07-3
SAT
4.85
k_ph_n-21
SAT
4.93
driver_d9n.unsat
UNSAT
5.11
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
5.17
query44_query57_1133
UNSAT
5.19
ev-pr-4x4-11-3-0-0-1-lg
SAT
5.22
CM-sat-03-01-07-3
SAT
5.3
ev-pr-4x4-13-3-0-0-1-lg
SAT
5.4
query51_query48_1133
UNSAT
5.47
JP-sat-02-07-3
SAT
5.59
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
5.6
klieber2017q-104-26-t1
FAIL
5.66
k0225682.c.oe
FAIL
5.67
cycle_sched_6_2_1.sat
FAIL
5.69
klieber2017q-074-18-t1
FAIL
5.69
jctc1-pass
FAIL
5.69
sortnetsort10.v.stepl.005
FAIL
5.69
k0026150.h.oe
FAIL
5.69
k0206272.s.oe
FAIL
5.7
rankfunc33_signed_32
FAIL
5.7
k0300663.v.oe
FAIL
5.71
genbuf9b4n.unsat
FAIL
5.71
nreachq_query02_1344
FAIL
5.71
klieber2017q-082-20-eq
FAIL
5.71
k0206272.h.oe
FAIL
5.71
gb_s2_r2_comp3_REAL.sat
FAIL
5.72
jctc4-fail
FAIL
5.72
mult_bool_matrix_4_5_5.sat
FAIL
5.72
sdlx-fixpoint-3
FAIL
5.72
klieber2017q-108-27-t1
FAIL
5.73
query08_query64_1344
FAIL
5.73
klieber2017q-116-29-eq
FAIL
5.73
audio_ddksynth_csynth2.cpp
FAIL
5.74
k0201058.c.oe
FAIL
5.74
chess_solving_mate_in_2_2011_ISC-7B_01
FAIL
5.74
klieber2017q-080-20-eq
FAIL
5.74
k0226271.c.oe
FAIL
5.74
load_full_3_comp3_REAL.unsat
FAIL
5.74
gb_s2_r2_comp3_REAL.unsat
FAIL
5.75
k0300663.s.oe
FAIL
5.75
klieber2017q-108-27-eq
FAIL
5.75
ltl2dpa_C26_comp3_REAL.sat
FAIL
5.76
incrementer-enc07-uniform-depth-25
FAIL
5.76
klieber2017q-092-23-eq
FAIL
5.76
query03_query57_1344
FAIL
5.76
k0300663.h.oe
FAIL
5.76
klieber2017q-104-26-eq
FAIL
5.76
query64_query58_1344
FAIL
5.76
bs128n.sat
FAIL
5.76
klieber2017q-076-19-eq
FAIL
5.77
klieber2017q-084-21-t1
FAIL
5.77
klieber2017q-086-21-eq
FAIL
5.77
query44_query58_1344
FAIL
5.77
klieber2017q-086-21-t1
FAIL
5.77
driver_a9y.unsat
FAIL
5.77
rankfunc17_unsigned_16
FAIL
5.77
k_ph_p-12
FAIL
5.77
mult_bool_matrix_4_5_5.unsat
FAIL
5.77
mult_bool_matrix_2_3_30.sat
FAIL
5.77
incrementer-enc08-uniform-depth-33
FAIL
5.77
sortnetsort9.v.stepl.005
FAIL
5.78
k0026150.v.oe
FAIL
5.78
amba2f9n.unsat
FAIL
5.78
chess_solving_mate_in_6_1998_OST-CH-1_15
FAIL
5.78
ltl2dpa_C26_comp2_REAL.unsat
FAIL
5.78
test2_quant_squaring2
FAIL
5.78
jctc8-pass
FAIL
5.78
stay24n.sat
FAIL
5.78
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
5.78
sortnetsort9.v.stepl.007
FAIL
5.78
mult_bool_matrix_2_3_30.unsat
FAIL
5.79
klieber2017q-100-25-t1
FAIL
5.79
k0225418.s.oe
FAIL
5.79
genbuf5b4n.unsat
FAIL
5.79
k0026150.s.oe
FAIL
5.79
rankfunc13_unsigned_64
FAIL
5.8
k0225418.c.oe
FAIL
5.8
klieber2017q-080-20-t1
FAIL
5.8
jctc13-fail
FAIL
5.8
small-swap2-fixpoint-4
FAIL
5.8
klieber2017q-092-23-t1
FAIL
5.8
k0225418.h.oe
FAIL
5.8
query64_query55_1344
FAIL
5.8
load_3c_comp_comp7_REAL.unsat
FAIL
5.8
ev-pr-6x6-9-5-0-1-2-lg
FAIL
5.8
k0225744.s.oe
FAIL
5.8
ken.flash^08.C-d4
FAIL
5.8
k0206272.v.oe
FAIL
5.81
jctc9-pass
FAIL
5.81
incrementer-enc02-uniform-depth-58
FAIL
5.81
query48_query42_1344
FAIL
5.81
query49_query58_1344
FAIL
5.81
input_pnpi8042_moudep.c
FAIL
5.81
amba2f9n.sat
FAIL
5.81
test3_quant_squaring2
FAIL
5.81
k0225744.h.oe
FAIL
5.81
load_full_3_comp3_REAL.sat
FAIL
5.82
klieber2017q-078-19-eq
FAIL
5.82
query42_query64_1344
FAIL
5.82
query33_query71_1344
FAIL
5.82
klieber2017q-116-29-t1
FAIL
5.83
jctc16-vals-0,2-pass
FAIL
5.83
klieber2017q-100-25-eq
FAIL
5.83
klieber2017q-096-24-t1
FAIL
5.83
query49_query64_1133
FAIL
5.84
genbuf5b4n.sat
FAIL
5.84
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
5.84
ken.oop^2.C-d4
FAIL
5.84
chess_solving_mate_in_2_1996_FIN-CH-17_03
FAIL
5.85
qshifter_7
FAIL
5.85
jctc10-fail
FAIL
5.86
genbuf10b4y.unsat
FAIL
5.86
chess_solving_mate_in_6_2011_SRB-CH_15
FAIL
5.87
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
FAIL
5.88
chess_solving_mate_in_2_1983_FIN-CH-4_01
FAIL
5.88
jctc2-pass
FAIL
5.9
cnt16r
FAIL
5.9
beemldelec4b1_c0to15.unsat
FAIL
5.9
nreachq_reachqu_2233
FAIL
5.91
chess_solving_mate_in_5_2012_NED-CH-18A_11
FAIL
5.91
k0302060.c.oe
FAIL
5.91
oski3ub1i_c0to63.unsat
FAIL
5.91
jctc6-pass
FAIL
5.91
filesys_smbmrx_cvsndrcv.c
FAIL
5.92
6s318r_c0to31.sat
FAIL
5.93
k0225418.v.oe
FAIL
5.95
klieber2017q-074-18-eq
FAIL
5.96
mv16y.sat
FAIL
5.97
klieber2017q-112-28-eq
FAIL
5.97
jctc7-pass
FAIL
5.98
ltl2dpa_C26_comp3_REAL.unsat
FAIL
5.98
chess_solving_mate_in_5_1996_UKR-CH-10_15
FAIL
5.98
klieber2017q-096-24-eq
FAIL
5.98
k0225744.v.oe
FAIL
5.99
chess_solving_mate_in_6_2016_RUS-CH_15
FAIL
6
query42_query57_1344
FAIL
6.01
jctc15-unrolled-fail
FAIL
6.02
chess_solving_mate_in_2_2012_GER-CH-36-19_03
FAIL
6.03
jctc5-fail
FAIL
6.03
network_irda_miniport_nscirda_comm.c
FAIL
6.03
chess_solving_mate_in_5_1984_FIN-CH-5_09
FAIL
6.03
cycle_sched_6_2_1.unsat
FAIL
6.04
ev-pr-6x6-11-5-0-1-2-lg
FAIL
6.07
jctc14-unrolled-fail
FAIL
6.08
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
UNSAT
6.12
jctc3-vals-0,2-pass
FAIL
6.19
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10
FAIL
6.19
p20-5.pddl_planlen=32
FAIL
6.26
JP-sat-02-08-3
SAT
6.41
jctc11-pass
FAIL
6.5
CM-sat-03-01-06-4
SAT
6.59
jctc18-vals-0,2-pass
FAIL
6.61
pg-hkb-4
UNSAT
6.67
SR-sat-02-01-06-2
SAT
6.76
SR-sat-02-01-07-2
SAT
6.84
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
7.04
nreachq_reachqu_2133
FAIL
7.11
jctc17-vals-0,2-pass
FAIL
7.12
query09_trivial_1344
SAT
7.3
DW-sat-06-20-1
SAT
7.32
CM-sat-04-01-06-3
SAT
7.47
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
7.82
JP-unsat-02-06-3
UNSAT
8.06
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
8.19
k_branch_p-10
UNSAT
8.63
JP-sat-02-07-4
SAT
8.67
SR-unsat-02-01-05-2
UNSAT
8.84
DW-sat-08-23-1
SAT
9.33
DW-sat-08-22-1
SAT
9.34
p20-20.pddl_planlen=23
FAIL
9.68
CM-sat-04-01-06-4
SAT
10
random-qcir-1000-50-441
UNSAT
12.27
DWs-sat-10-23-1
SAT
12.5
CM-sat-04-01-07-3
SAT
13.52
DWs-sat-10-25-1
SAT
13.71
DWs-unsat-07-16-1
UNSAT
13.74
pg-hkb-5
UNSAT
14.18
random-qcir-1000-50-930
UNSAT
18.12
random-qcir-1000-50-754
UNSAT
18.34
random-qcir-1000-50-134
UNSAT
18.65
DWs-sat-12-28-1
SAT
19.58
DWs-unsat-08-17-1
UNSAT
19.62
random-qcir-1000-50-970
UNSAT
21.09
random-qcir-1000-50-857
UNSAT
22.12
DW-sat-08-24-1
SAT
22.95
DWs-unsat-08-18-1
UNSAT
23.86
random-qcir-1000-50-898
UNSAT
24.41
random-qcir-1000-50-68
UNSAT
25.41
random-qcir-1000-50-428
UNSAT
27.61
random-qcir-1000-50-393
UNSAT
27.89
random-qcir-1000-50-267
UNSAT
28.57
random-qcir-1000-50-983
UNSAT
28.87
random-qcir-1000-50-473
UNSAT
30.07
random-qcir-1000-50-275
UNSAT
30.37
random-qcir-1000-50-98
UNSAT
31.64
random-qcir-1000-50-361
UNSAT
32.11
random-qcir-1000-50-743
UNSAT
32.21
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
SAT
32.7
random-qcir-1000-50-846
UNSAT
32.89
random-qcir-1000-50-295
UNSAT
33.46
k_branch_p-11
UNSAT
34.2
random-qcir-1000-50-658
UNSAT
37.03
DWs-sat-15-35-1
SAT
38.81
random-qcir-1000-50-940
UNSAT
39.87
random-qcir-1000-50-456
UNSAT
39.9
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
UNSAT
41.3
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
42.92
random-qcir-1000-50-793
UNSAT
44.51
random-qcir-1000-50-545
UNSAT
46.3
DWs-unsat-09-19-1
UNSAT
46.34
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
SAT
46.99
SR-sat-02-01-06-3
SAT
47.68
random-qcir-1000-50-255
UNSAT
51.86
pg-hkb-6
UNSAT
58.87
pipesnotankage18_8
FAIL
59.58
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
SAT
61.87
CM-sat-07-01-07-3
SAT
67.13
cnt14
SAT
69.45
DW-sat-09-26-1
SAT
81.55
CM-sat-07-01-06-4
SAT
86.66
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
SAT
99.32
DW-unsat-09-22-1
UNSAT
116.65
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
SAT
118.78
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
SAT
134.82
SR-sat-03-01-07-2
SAT
138.63
SR-sat-03-01-08-2
SAT
144.21
k_branch_n-10
SAT
151.4
DWs-sat-10-24-1
SAT
155.31
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
158.65
JP-unsat-03-08-3
UNSAT
162.18
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
SAT
168
DWs-unsat-11-23-1
UNSAT
192.37
JP-unsat-03-07-4
UNSAT
234.59
CM-sat-07-01-06-3
SAT
242.11
sortnetsort9.AE.stepl.012
UNSAT
250.94
CM-unsat-07-01-06-2
UNSAT
256.09
k0225418.connected.oe
SAT
265.82
DWs-unsat-11-24-1
UNSAT
275.68
DW-unsat-10-25-1
UNSAT
282.91
pg-hkb-7
UNSAT
315.06
k_branch_p-16
UNSAT
346.79
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
UNSAT
356.74
DWs-unsat-12-25-1
UNSAT
387.09
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
SAT
458.89
DW-unsat-11-26-1
UNSAT
666.44
ev-pr-4x4-15-3-0-0-1-s
FAIL
708.04
DW-unsat-11-27-1
UNSAT
820.48
SR-unsat-03-01-06-2
UNSAT
868.51
pg-hkb-23
FAIL
900.01
small-swap1-fixpoint-3
FAIL
900.01
pg-hkb-24
FAIL
900.01
pg-hkb-8
FAIL
900.01
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03
FAIL
900.01
chess_composing_6_template_01
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900.01
pg-hkb-18
FAIL
900.01
chess_solving_mate_in_9_2003_RUS-CH_15
FAIL
900.02
chess_solving_mate_in_3_2009_FIN-CH-30_04
FAIL
900.02
chess_composing_8_template_42
FAIL
900.02
pipesnotankage14_10
FAIL
900.02
chess_solving_mate_in_7_2005_GER-CH-29-12_15
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900.03
pg-hkb-15
FAIL
900.03
chess_composing_8_template_43
FAIL
900.03
k_ph_p-19
FAIL
900.03
k0026150.connected.oe
FAIL
900.03
pg-hkb-9
FAIL
900.03
pg-hkb-21
FAIL
900.03
pg-hkb-17
FAIL
900.03
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900.03
k_branch_n-12
FAIL
900.03
JP-sat-03-09-4
FAIL
900.03
chess_solving_mate_in_4_1999_GER-CH-23-6_14
FAIL
900.04
k0225744.connected.oe
FAIL
900.04
chess_composing_6_template_04
FAIL
900.04
chess_solving_mate_in_7_2011_SVK-CH-19_15
FAIL
900.04
pg-hkb-12
FAIL
900.04
pg-hkb-13
FAIL
900.04
pg-hkb-22
FAIL
900.04
pg-hkb-26
FAIL
900.04
chess_solving_mate_in_4_1984_GBR-CH-5_04
FAIL
900.04
chess_solving_mate_in_3_2016_BEL-CH-23A_02
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.asp
FAIL
900.05
chess_composing_6_template_06
FAIL
900.05
chess_composing_8_template_38
FAIL
900.05
pg-hkb-11
FAIL
900.06
query08_query26_1344
FAIL
900.06
chess_composing_8_template_02
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900.06
chess_solving_mate_in_8_2011_BEL-CH-19A_03
FAIL
900.06
chess_solving_mate_in_7_2016_BEL-CH-23A_03
FAIL
900.06
DWs-unsat-13-28-1
FAIL
900.07
pg-hkb-14
FAIL
900.07
JP-unsat-03-08-5
FAIL
900.07
p20-1.pddl_planlen=24
FAIL
900.07
pg-hkb-19
FAIL
900.07
k0300663.connected.oe
FAIL
900.07
test1_quant_squaring3
FAIL
900.07
chess_solving_mate_in_4_2009_SEROCK-OPEN_09
FAIL
900.08
pg-hkb-10
FAIL
900.08
pg-hkb-16
FAIL
900.08
pg-hkb-25
FAIL
900.08
chess_composing_8_template_13
FAIL
900.08
JP-unsat-03-09-4
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900.09
chess_solving_mate_in_7_2009_POL-CH-33_15
FAIL
900.09
JP-sat-03-08-4
FAIL
900.09
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900.09
pg-hkb-20
FAIL
900.09
test2_quant_squaring3
FAIL
900.09
k0206272.connected.oe
FAIL
900.09
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900.09
beemldelec4b1_c0to15.sat
FAIL
900.1
chess_solving_mate_in_3_1999_WCSC-23_05
FAIL
900.1
oski3ub1i_c0to63.sat
FAIL
900.1
Contact
|
Organization
|
Links
|
Citing QBFLIB