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
GhostQ_PG___cegar_qcir_2018
QBFEVAL'18 - Prenex non-CNF Track
Instance
Result
Time
query71_query15_1133
UNSAT
0
query30_eequery_1133
SAT
0
pg-hkb-2
UNSAT
0
query04_query03_1133
UNSAT
0
query51_query48_1133
UNSAT
0.09
query50_query49_1133
UNSAT
0.09
pg-hkb-3
UNSAT
0.11
query64_query31_1133
UNSAT
0.14
driver_d9n.unsat
UNSAT
0.18
ntrivil_query54_1133
SAT
0.18
pg-hkb-4
UNSAT
0.2
SR-unsat-02-01-06-1
UNSAT
0.22
query21_reachqu_1133
SAT
0.26
k0206272.s.oe
SAT
0.37
query09_trivial_1344
SAT
0.64
bs128n.unsat
UNSAT
0.76
k0201058.c.oe
SAT
0.83
stay22n.unsat
UNSAT
0.83
k0206272.h.oe
SAT
0.88
ltl2dpa_C26_comp2_REAL.unsat
UNSAT
0.96
6s318r_c0to15.unsat
UNSAT
1.15
ltl2dpa_C26_comp3_REAL.unsat
UNSAT
1.28
CM-sat-02-01-07-3
SAT
1.32
query44_query57_1133
UNSAT
1.59
random-qcir-1000-50-930
UNSAT
1.61
pg-hkb-5
UNSAT
1.62
nreachq_query02_1344
UNSAT
1.75
random-qcir-1000-50-983
UNSAT
2.24
random-qcir-1000-50-793
UNSAT
2.29
random-qcir-1000-50-393
UNSAT
2.3
query08_query26_1344
SAT
2.48
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
2.51
random-qcir-1000-50-940
UNSAT
3.13
query03_query57_1344
SAT
3.13
driver_a9y.unsat
UNSAT
3.49
incrementer-enc08-uniform-depth-33
SAT
3.6
random-qcir-1000-50-267
UNSAT
4
k0206272.v.oe
SAT
4.02
random-qcir-1000-50-743
UNSAT
4.07
random-qcir-1000-50-441
UNSAT
4.08
random-qcir-1000-50-857
UNSAT
4.39
query49_query64_1133
UNSAT
4.74
random-qcir-1000-50-295
UNSAT
4.8
random-qcir-1000-50-98
UNSAT
4.98
random-qcir-1000-50-545
UNSAT
5.18
random-qcir-1000-50-134
UNSAT
5.41
k0226271.c.oe
SAT
5.48
pg-hkb-13
FAIL
5.52
random-qcir-1000-50-361
UNSAT
5.61
random-qcir-1000-50-275
UNSAT
5.65
random-qcir-1000-50-68
UNSAT
5.78
random-qcir-1000-50-970
UNSAT
5.99
k0026150.h.oe
SAT
6.06
jctc13-fail
UNSAT
6.36
jctc6-pass
SAT
6.37
random-qcir-1000-50-456
UNSAT
6.42
JP-sat-02-07-3
SAT
6.52
klieber2017q-104-26-t1
UNSAT
6.58
random-qcir-1000-50-846
UNSAT
6.61
random-qcir-1000-50-754
UNSAT
6.71
random-qcir-1000-50-658
UNSAT
6.98
k0225744.s.oe
SAT
7.28
pg-hkb-14
FAIL
7.3
klieber2017q-076-19-eq
SAT
7.37
klieber2017q-078-19-eq
SAT
7.43
random-qcir-1000-50-898
UNSAT
7.62
random-qcir-1000-50-428
UNSAT
7.87
pg-hkb-6
UNSAT
8.17
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
8.68
random-qcir-1000-50-255
UNSAT
8.75
klieber2017q-108-27-t1
UNSAT
8.9
incrementer-enc07-uniform-depth-25
UNSAT
9.41
pg-hkb-15
FAIL
9.53
beemldelec4b1_c0to15.unsat
UNSAT
9.61
JP-sat-02-07-4
SAT
9.68
CM-sat-03-01-07-3
SAT
10
random-qcir-1000-50-473
UNSAT
10.12
klieber2017q-074-18-t1
UNSAT
10.25
klieber2017q-074-18-eq
SAT
11.51
query08_query64_1344
SAT
12.3
pg-hkb-16
FAIL
12.34
SR-sat-02-01-06-2
SAT
12.59
klieber2017q-086-21-eq
SAT
12.7
SR-sat-02-01-07-2
SAT
14.03
JP-sat-02-08-3
SAT
14.59
JP-unsat-02-06-3
UNSAT
14.86
pg-hkb-17
FAIL
15.59
jctc16-vals-0,2-pass
SAT
16.15
DW-sat-06-20-1
SAT
16.76
klieber2017q-082-20-eq
SAT
18.59
klieber2017q-112-28-t1
UNSAT
18.82
pg-hkb-18
FAIL
19.59
klieber2017q-100-25-t1
UNSAT
20.79
jctc1-pass
SAT
20.79
klieber2017q-080-20-t1
UNSAT
22.78
k0225418.v.oe
SAT
23.44
DWs-unsat-07-16-1
UNSAT
24.33
pg-hkb-19
FAIL
24.35
CM-sat-03-01-06-4
SAT
24.61
klieber2017q-092-23-t1
UNSAT
24.77
klieber2017q-100-25-eq
SAT
25.81
CM-sat-04-01-06-3
SAT
26.8
jctc4-fail
UNSAT
27.29
k0225418.connected.oe
SAT
28.21
SR-unsat-02-01-05-2
UNSAT
29.13
pg-hkb-20
FAIL
30.02
load_full_3_comp3_REAL.unsat
UNSAT
30.98
genbuf5b4n.unsat
UNSAT
31.91
klieber2017q-096-24-t1
UNSAT
33.5
pg-hkb-21
FAIL
36.03
pg-hkb-7
UNSAT
36.1
DWs-unsat-08-17-1
UNSAT
38.26
klieber2017q-078-19-t1
UNSAT
42.86
load_3c_comp_comp7_REAL.unsat
UNSAT
43.8
pg-hkb-22
FAIL
44.12
amba2f9n.unsat
UNSAT
45.72
CM-sat-04-01-07-3
SAT
48.62
chess_solving_mate_in_2_1983_FIN-CH-4_01
SAT
53.68
jctc2-pass
SAT
53.91
klieber2017q-104-26-eq
SAT
55.88
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
56.04
klieber2017q-092-23-eq
SAT
56.99
pg-hkb-23
FAIL
57.31
DWs-unsat-08-18-1
UNSAT
60.78
pg-hkb-24
FAIL
63.04
klieber2017q-086-21-t1
UNSAT
63.97
klieber2017q-096-24-eq
SAT
65.52
DW-sat-08-24-1
SAT
70.52
pg-hkb-25
FAIL
72.74
klieber2017q-116-29-eq
SAT
79.01
pg-hkb-26
FAIL
86.47
DW-sat-08-22-1
SAT
88.15
DWs-unsat-09-19-1
UNSAT
93.11
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
SAT
94.69
query33_query71_1344
UNSAT
99.77
DWs-sat-10-25-1
SAT
100.75
chess_solving_mate_in_2_2011_ISC-7B_01
SAT
109.07
CM-sat-04-01-06-4
SAT
111.39
DW-sat-09-26-1
SAT
111.85
chess_solving_mate_in_2_1996_FIN-CH-17_03
SAT
113.91
jctc8-pass
SAT
129.83
DW-sat-08-23-1
SAT
145.45
CM-sat-07-01-06-3
SAT
160.7
pg-hkb-8
UNSAT
170.3
klieber2017q-084-21-t1
UNSAT
171.47
DW-unsat-09-22-1
UNSAT
175.49
query64_query58_1344
UNSAT
227.38
DWs-sat-10-24-1
SAT
242.81
incrementer-enc02-uniform-depth-58
UNSAT
243.71
klieber2017q-080-20-eq
SAT
245.51
oski3ub1i_c0to63.unsat
UNSAT
245.65
klieber2017q-112-28-eq
SAT
252.73
chess_solving_mate_in_2_2012_GER-CH-36-19_03
SAT
260.08
query48_query42_1344
SAT
297.11
genbuf9b4n.unsat
UNSAT
321.74
genbuf10b4y.unsat
UNSAT
336.89
jctc9-pass
SAT
380.15
ev-pr-4x4-11-3-0-0-1-lg
SAT
386.43
gb_s2_r2_comp3_REAL.unsat
UNSAT
512.38
DW-unsat-10-25-1
UNSAT
529.34
SR-sat-02-01-06-3
SAT
545.15
DWs-unsat-11-23-1
UNSAT
576.48
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
585.63
klieber2017q-116-29-t1
UNSAT
618.74
ev-pr-4x4-13-3-0-0-1-lg
SAT
628.61
CM-sat-07-01-06-4
SAT
630.49
query64_query55_1344
UNSAT
645.18
DWs-sat-10-23-1
SAT
664.36
pg-hkb-9
UNSAT
724.07
ev-pr-6x6-9-5-0-1-2-lg
UNSAT
791.92
DWs-unsat-11-24-1
UNSAT
895.07
chess_solving_mate_in_3_2009_FIN-CH-30_04
FAIL
900
query42_query57_1344
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
FAIL
900
test3_quant_squaring2
FAIL
900
jctc14-unrolled-fail
FAIL
900
k0302060.c.oe
FAIL
900
chess_solving_mate_in_4_2009_SEROCK-OPEN_09
FAIL
900
chess_solving_mate_in_9_2003_RUS-CH_15
FAIL
900
small-swap1-fixpoint-3
FAIL
900
chess_solving_mate_in_7_2016_BEL-CH-23A_03
FAIL
900
ken.flash^08.C-d4
FAIL
900.01
cnt14
FAIL
900.01
chess_solving_mate_in_3_1999_WCSC-23_05
FAIL
900.01
chess_composing_6_template_01
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900.01
chess_composing_6_template_04
FAIL
900.01
query49_query58_1344
FAIL
900.01
ev-pr-8x8-7-7-0-1-2-lg
FAIL
900.01
sortnetsort9.v.stepl.005
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.asp
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
FAIL
900.01
pg-hkb-10
FAIL
900.01
k0225418.c.oe
FAIL
900.01
rankfunc33_signed_32
FAIL
900.01
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900.01
pg-hkb-12
FAIL
900.01
input_pnpi8042_moudep.c
FAIL
900.01
k0206272.connected.oe
FAIL
900.01
pipesnotankage18_8
FAIL
900.01
cycle_sched_6_2_1.sat
FAIL
900.02
cycle_sched_6_2_1.unsat
FAIL
900.02
p20-20.pddl_planlen=23
FAIL
900.02
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900.02
rankfunc17_unsigned_16
FAIL
900.02
load_full_3_comp3_REAL.sat
FAIL
900.02
k0225418.h.oe
FAIL
900.02
k0026150.v.oe
FAIL
900.02
k0300663.h.oe
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900.02
k0300663.connected.oe
FAIL
900.02
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900.02
chess_composing_8_template_42
FAIL
900.02
CM-unsat-07-01-06-2
FAIL
900.02
chess_solving_mate_in_3_2016_BEL-CH-23A_02
FAIL
900.02
JP-unsat-03-07-4
FAIL
900.02
jctc7-pass
FAIL
900.02
jctc17-vals-0,2-pass
FAIL
900.02
DW-unsat-11-26-1
FAIL
900.02
chess_composing_8_template_02
FAIL
900.02
JP-sat-03-08-4
FAIL
900.02
jctc11-pass
FAIL
900.02
JP-unsat-03-08-5
FAIL
900.02
amba2f9n.sat
FAIL
900.02
chess_composing_8_template_43
FAIL
900.03
small-swap2-fixpoint-4
FAIL
900.03
mult_bool_matrix_2_3_30.sat
FAIL
900.03
SR-sat-03-01-08-2
FAIL
900.03
mult_bool_matrix_4_5_5.sat
FAIL
900.03
jctc5-fail
FAIL
900.03
chess_solving_mate_in_6_2011_SRB-CH_15
FAIL
900.03
rankfunc13_unsigned_64
FAIL
900.03
k0225744.connected.oe
FAIL
900.03
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
FAIL
900.03
network_irda_miniport_nscirda_comm.c
FAIL
900.03
DWs-unsat-12-25-1
FAIL
900.03
test1_quant_squaring3
FAIL
900.03
genbuf5b4n.sat
FAIL
900.03
DWs-unsat-13-28-1
FAIL
900.03
jctc15-unrolled-fail
FAIL
900.03
oski3ub1i_c0to63.sat
FAIL
900.03
k_branch_p-10
FAIL
900.03
pipesnotankage14_10
FAIL
900.03
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
900.04
chess_solving_mate_in_7_2011_SVK-CH-19_15
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
FAIL
900.04
p20-5.pddl_planlen=32
FAIL
900.04
sdlx-fixpoint-3
FAIL
900.04
pg-hkb-11
FAIL
900.04
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
900.04
filesys_smbmrx_cvsndrcv.c
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
FAIL
900.04
DWs-sat-15-35-1
FAIL
900.04
k0225682.c.oe
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
FAIL
900.04
mult_bool_matrix_2_3_30.unsat
FAIL
900.04
k_ph_n-21
FAIL
900.04
jctc18-vals-0,2-pass
FAIL
900.04
JP-unsat-03-09-4
FAIL
900.04
query42_query64_1344
FAIL
900.04
chess_solving_mate_in_4_1999_GER-CH-23-6_14
FAIL
900.04
test2_quant_squaring2
FAIL
900.04
chess_composing_6_template_06
FAIL
900.04
k0300663.v.oe
FAIL
900.05
chess_composing_8_template_38
FAIL
900.05
k_branch_p-11
FAIL
900.05
k_ph_p-19
FAIL
900.05
cnt16r
FAIL
900.05
chess_composing_8_template_13
FAIL
900.05
k0300663.s.oe
FAIL
900.05
chess_solving_mate_in_6_2016_RUS-CH_15
FAIL
900.05
chess_solving_mate_in_5_1984_FIN-CH-5_09
FAIL
900.05
k0225744.h.oe
FAIL
900.05
ev-pr-4x4-15-3-0-0-1-s
FAIL
900.05
JP-sat-03-09-4
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900.05
mv16y.sat
FAIL
900.05
DWs-sat-12-28-1
FAIL
900.05
stay24n.sat
FAIL
900.05
beemldelec4b1_c0to15.sat
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
FAIL
900.05
DW-unsat-11-27-1
FAIL
900.05
JP-unsat-03-08-3
FAIL
900.05
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
900.05
SR-sat-03-01-07-2
FAIL
900.05
jctc3-vals-0,2-pass
FAIL
900.05
6s318r_c0to31.sat
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900.05
sortnetsort9.AE.stepl.012
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900.06
CM-sat-07-01-07-3
FAIL
900.06
sortnetsort10.v.stepl.005
FAIL
900.06
nreachq_reachqu_2233
FAIL
900.06
audio_ddksynth_csynth2.cpp
FAIL
900.06
k0026150.s.oe
FAIL
900.06
chess_solving_mate_in_7_2009_POL-CH-33_15
FAIL
900.06
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10
FAIL
900.06
k_ph_p-12
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900.07
klieber2017q-108-27-eq
FAIL
900.07
test2_quant_squaring3
FAIL
900.07
SR-unsat-03-01-06-2
FAIL
900.07
bs128n.sat
FAIL
900.07
mult_bool_matrix_4_5_5.unsat
FAIL
900.07
k0225744.v.oe
FAIL
900.07
jctc10-fail
FAIL
900.07
nreachq_reachqu_2133
FAIL
900.07
chess_solving_mate_in_6_1998_OST-CH-1_15
FAIL
900.07
chess_solving_mate_in_5_2012_NED-CH-18A_11
FAIL
900.07
chess_solving_mate_in_7_2005_GER-CH-29-12_15
FAIL
900.07
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900.07
ken.oop^2.C-d4
FAIL
900.08
k_branch_n-12
FAIL
900.08
sortnetsort9.v.stepl.007
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
FAIL
900.08
k0026150.connected.oe
FAIL
900.08
k_branch_n-10
FAIL
900.08
chess_solving_mate_in_5_1996_UKR-CH-10_15
FAIL
900.08
k0225418.s.oe
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900.08
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
900.08
p20-1.pddl_planlen=24
FAIL
900.09
k_branch_p-16
FAIL
900.09
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
900.09
gb_s2_r2_comp3_REAL.sat
FAIL
900.09
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
900.09
ltl2dpa_C26_comp3_REAL.sat
FAIL
900.09
chess_solving_mate_in_4_1984_GBR-CH-5_04
FAIL
900.09
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03
FAIL
900.1
chess_solving_mate_in_8_2011_BEL-CH-19A_03
FAIL
900.1
qshifter_7
FAIL
900.11
query44_query58_1344
FAIL
900.11
Contact
|
Organization
|
Links
|
Citing QBFLIB