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___cegar_qcir_2019
Prenex non-CNF Track
Instance
Result
Time
ntrivil_query64_1133
SAT
0
falsequ_query71_1344
SAT
0
falsequ_query64_1344
SAT
0
k0327178.c.oe
FAIL
0
k0326578.connected.oe
FAIL
0
k0326191.connected.oe
FAIL
0
k0325715.s.oe
FAIL
0
k0325715.c.oe
FAIL
0
k0325624.v.oe
FAIL
0
k0325624.s.oe
FAIL
0
k0325624.connected.oe
FAIL
0
k0327178.connected.oe
FAIL
0
k0327620.h.oe
FAIL
0
k0327694.v.oe
FAIL
0
falsequ_query71_1133
SAT
0
nxquery_query42_1133
SAT
0
nxquery_query50_1133
UNSAT
0
nxquery_query64_1133
SAT
0
nxquery_query71_1133
UNSAT
0
trueque_query64_1344
SAT
0
k0302060.connected.oe
FAIL
0
axquery_query71_1133
UNSAT
0
axquery_query64_1133
SAT
0
falsequ_query64_1133
SAT
0
k0325261.s.oe
FAIL
0
k0325261.h.oe
FAIL
0
trueque_query60_1133
SAT
0
k0225682.v.oe
FAIL
0
k0225418.v.oe
FAIL
0
k0225418.connected.oe
FAIL
0
k0206272.v.oe
FAIL
0
k0206272.s.oe
FAIL
0
k0206272.h.oe
FAIL
0
k0206272.c.oe
FAIL
0
k0201058.v.oe
FAIL
0
k0201058.h.oe
FAIL
0
k0201058.c.oe
FAIL
0
k0026150.h.oe
FAIL
0
k0225744.s.oe
FAIL
0
k0226271.connected.oe
FAIL
0
trueque_query64_1133
SAT
0
trueque_query71_1133
SAT
0
k0325261.connected.oe
FAIL
0
k0302060.h.oe
FAIL
0
trueque_query71_1344
SAT
0
k0300663.v.oe
FAIL
0
k0248814.c.oe
FAIL
0
k0300663.s.oe
FAIL
0
k0226271.s.oe
FAIL
0
k0300663.c.oe
FAIL
0
k0248814.v.oe
FAIL
0
falsequ_query60_1133
SAT
0.08
exquery_query42_1133
UNSAT
0.09
query64_query11_1133
UNSAT
0.09
axquery_query42_1133
SAT
0.1
exquery_query71_1133
SAT
0.1
exquery_query64_1133
SAT
0.1
eequery_query42_1133
UNSAT
0.11
eequery_query71_1133
SAT
0.11
eequery_query64_1133
UNSAT
0.11
klieber2017q-048-12-eq
SAT
0.13
klieber2017q-048-12-t1
UNSAT
0.13
axquery_query71_1344
SAT
0.14
query64_query42_1133
UNSAT
0.14
exquery_query71_1344
SAT
0.15
nxquery_query71_1344
SAT
0.15
trivial_query71_1133
SAT
0.17
exquery_query64_1344
SAT
0.17
nreachq_query11_1133
UNSAT
0.17
axquery_query64_1344
SAT
0.17
ntrivil_query71_1133
SAT
0.17
trivial_query60_1133
SAT
0.17
trivial_query64_1133
SAT
0.18
ntrivil_query42_1133
SAT
0.18
k0302060.s.oe
FAIL
0.18
k0248814.h.oe
FAIL
0.19
k0026150.c.oe
FAIL
0.19
SR-unsat-02-01-06-1
UNSAT
0.22
k0325715.connected.oe
FAIL
0.27
query71_query36_1133
UNSAT
0.27
query71_query31_1133
UNSAT
0.27
query71_query34_1133
UNSAT
0.28
k0201058.connected.oe
FAIL
0.33
ntrivil_query71_1344
SAT
0.38
trivial_query71_1344
SAT
0.54
ntrivil_query64_1344
SAT
0.66
trivial_query64_1344
SAT
0.67
nreachq_query54_1133
UNSAT
1.14
nreachq_query71_1133
UNSAT
1.17
klieber2017q-066-16-t1
UNSAT
1.22
klieber2017q-070-17-t1
UNSAT
1.31
eequery_query64_1344
UNSAT
1.37
klieber2017q-060-15-t1
UNSAT
1.5
klieber2017q-056-14-eq
SAT
1.73
klieber2017q-068-17-t1
UNSAT
2.28
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
2.57
klieber2017q-052-13-eq
SAT
2.69
reachqu_query64_1133
SAT
2.78
DW-sat-04-16-1
SAT
3.6
SR-unsat-03-01-07-1
UNSAT
3.69
JP-unsat-02-07-2
UNSAT
3.86
reachqu_query60_1133
SAT
4.48
klieber2017q-066-16-eq
SAT
4.7
klieber2017q-060-15-eq
SAT
5.79
klieber2017q-068-17-eq
SAT
5.9
jctc13-fail
UNSAT
6.19
klieber2017q-072-18-eq
SAT
6.27
jctc6-pass
SAT
6.29
klieber2017q-104-26-t1
UNSAT
6.37
klieber2017q-062-15-t1
UNSAT
6.58
klieber2017q-070-17-eq
SAT
6.72
klieber2017q-078-19-eq
SAT
7.22
klieber2017q-076-19-eq
SAT
7.28
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
7.58
klieber2017q-108-27-t1
UNSAT
8.79
klieber2017q-076-19-t1
UNSAT
9.11
klieber2017q-064-16-t1
UNSAT
9.29
JP-sat-02-07-4
SAT
9.3
klieber2017q-082-20-t1
UNSAT
9.87
klieber2017q-074-18-t1
UNSAT
10.12
klieber2017q-064-16-eq
SAT
10.82
klieber2017q-074-18-eq
SAT
11.38
klieber2017q-062-15-eq
SAT
11.44
SR-sat-02-01-06-2
SAT
12.2
SR-sat-02-01-07-2
SAT
13.64
JP-sat-02-08-3
SAT
13.96
JP-unsat-02-06-3
UNSAT
14.34
klieber2017q-072-18-t1
UNSAT
15.63
jctc16-vals-0,2-pass
SAT
15.78
klieber2017q-112-28-t1
UNSAT
16.18
klieber2017q-100-25-t1
UNSAT
20.61
jctc1-pass
SAT
20.64
klieber2017q-084-21-eq
SAT
22.01
klieber2017q-080-20-t1
UNSAT
22.17
CM-sat-04-01-06-3
SAT
25.96
jctc4-fail
UNSAT
26.57
SR-unsat-02-01-05-2
UNSAT
28.09
klieber2017q-088-22-t1
UNSAT
34.91
DWs-unsat-08-17-1
UNSAT
37.04
SR-unsat-04-01-08-1
UNSAT
39.73
klieber2017q-078-19-t1
UNSAT
41.53
chess_solving_mate_in_2_2002_WCCC-OPEN-45_01
SAT
42.06
load_3c_comp_comp7_REAL.unsat
UNSAT
42.73
chess_solving_mate_in_2_2009_BEL-CH-17B_01
SAT
42.78
chess_solving_mate_in_2_2011_WCCC-OPEN-54_01
SAT
45.03
CM-sat-04-01-07-3
SAT
46.53
chess_solving_mate_in_2_2008_BEL-CH-16B_08
SAT
46.55
jctc2-pass
SAT
52.58
chess_solving_mate_in_2_1983_FIN-CH-4_01
SAT
53.91
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
54.57
DWs-unsat-08-18-1
UNSAT
58.32
chess_solving_mate_in_2_2002_MAC-CH-6_03
SAT
59.88
klieber2017q-086-21-t1
UNSAT
62.4
eequery_query42_1344
UNSAT
63.39
chess_solving_mate_in_2_2009_POL-CH-33_01
SAT
70.2
klieber2017q-088-22-eq
SAT
72.05
chess_solving_mate_in_2_2011_ISC-7B_01
SAT
73.1
chess_solving_mate_in_2_1998_GBR-CH-19_01
SAT
73.31
chess_solving_mate_in_2_1987_FIN-CH-8_01
SAT
74.68
DW-sat-08-22-1
SAT
83.49
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
SAT
84.01
DW-sat-09-26-1
SAT
86.54
chess_solving_mate_in_2_2014_NED-CH-20B_09
SAT
86.71
DWs-unsat-09-19-1
UNSAT
88.3
DW-sat-08-23-1
SAT
92.68
DWs-sat-10-25-1
SAT
95.27
chess_solving_mate_in_2_2011_ROM-CH-W_02
SAT
99.74
chess_solving_mate_in_2_1996_FIN-CH-17_03
SAT
108.35
chess_solving_mate_in_2_2015_GBR-CH-36_02
SAT
108.5
CM-sat-04-01-06-4
SAT
109.39
jctc8-pass
SAT
125.9
CM-sat-07-01-06-3
SAT
155.63
DW-unsat-09-22-1
UNSAT
168.54
klieber2017q-084-21-t1
UNSAT
170.06
chess_solving_mate_in_2_1982_WCSC-6_02
SAT
182.29
chess_solving_mate_in_2_2011_GBR-CH-32_03
SAT
194.18
chess_solving_mate_in_2_1997_WCCC-OPEN-40_03
SAT
199.41
DW-unsat-09-23-1
UNSAT
227.04
chess_solving_mate_in_2_2012_GER-CH-36-19_03
SAT
243.42
chess_solving_mate_in_2_1991_GER-CH-15_01
SAT
264.97
genbuf9b4n.unsat
UNSAT
313.3
jctc9-pass
SAT
366.42
DWs-unsat-10-22-1
UNSAT
370.93
DWs-sat-10-23-1
SAT
395.1
genbuf10b4n.unsat
UNSAT
430.91
DW-unsat-10-25-1
UNSAT
497.68
SR-sat-02-01-06-3
SAT
530.18
DWs-unsat-11-23-1
UNSAT
554.14
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
566.79
CM-sat-07-01-06-4
SAT
617.53
nreachq_query71_1344
SAT
640.96
CM-sat-07-01-07-3
SAT
742.01
reachqu_query60_1344
SAT
792.66
DWs-unsat-11-24-1
UNSAT
863.52
JP-sat-03-09-5
FAIL
900
cycle_sched_2_10_1.sat
FAIL
900
cycle_sched_4_4_2.sat
FAIL
900
cycle_sched_6_6_2.sat
FAIL
900
driver_a10y.sat
FAIL
900
driver_b8n.sat
FAIL
900
driver_c9n.sat
FAIL
900
cycle_sched_12_2_1.sat
FAIL
900
amba3b5y.sat
FAIL
900
amba2c7n.sat
FAIL
900
stay24n.sat
FAIL
900
chess_solving_mate_in_3_2012_NED-CH-18B_04
FAIL
900
mult_bool_matrix_17_17_17.sat
FAIL
900
mult_bool_matrix_10_9_11.unsat
FAIL
900
mult_bool_matrix_10_9_11.sat
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
driver_c9y.sat
FAIL
900
beemskbn1f1_c0to7.sat
FAIL
900
JP-sat-03-09-4
FAIL
900
JP-sat-03-08-5
FAIL
900
DW-unsat-20-44-1
FAIL
900
DW-sat-19-44-1
FAIL
900
CM-unsat-18-01-05-3
FAIL
900
CM-unsat-17-01-05-3
FAIL
900
CM-unsat-07-01-06-2
FAIL
900
mult9.sat
FAIL
900
bs128y.sat
FAIL
900
bs128n.sat
FAIL
900
add20y.sat
FAIL
900
mult_bool_matrix_dyn_9_5.sat
FAIL
900
mult_bool_matrix_18_18_18.sat
FAIL
900
mult_bool_matrix_12_13_11.sat
FAIL
900
ltl2dba_C2-8_comp4_REAL.sat
FAIL
900
load_2c_comp_comp7_REAL.sat
FAIL
900
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
load_full_4_comp3_REAL.unsat
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.asp
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
driver_d9y.sat
FAIL
900
driver_a9n.sat
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
cycle_sched_4_7_1.unsat
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
amba4b9y.unsat
FAIL
900
amba2f9n.sat
FAIL
900
reachqu_query71_1344
FAIL
900
reachqu_query64_1344
FAIL
900
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#4.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900
CM-unsat-13-01-05-3
FAIL
900
DWs-sat-23-49-1
FAIL
900
DWs-sat-24-51-1
FAIL
900
DWs-sat-25-53-1
FAIL
900
CM-sat-19-01-06-3
FAIL
900
CM-sat-18-01-07-3
FAIL
900
jctc5-fail
FAIL
900
jctc18-vals-0,2-pass
FAIL
900
DWs-unsat-22-45-1
FAIL
900
DWs-unsat-23-47-1
FAIL
900
DWs-unsat-24-49-1
FAIL
900
DWs-unsat-25-51-1
FAIL
900
jctc17-vals-0,2-pass
FAIL
900
DW-unsat-11-26-1
FAIL
900
DW-unsat-21-46-1
FAIL
900
DW-unsat-22-48-1
FAIL
900
DW-unsat-23-50-1
FAIL
900
DWs-sat-22-47-1
FAIL
900
DWs-sat-21-45-1
FAIL
900
CM-unsat-14-01-05-3
FAIL
900
CM-unsat-15-01-05-3
FAIL
900
CM-unsat-16-01-05-3
FAIL
900
CM-unsat-19-01-05-3
FAIL
900
CM-unsat-20-01-05-3
FAIL
900
CM-unsat-21-01-05-3
FAIL
900
CM-sat-21-01-06-3
FAIL
900
CM-sat-20-01-06-3
FAIL
900
DW-sat-17-40-1
FAIL
900
DW-sat-18-42-1
FAIL
900
DW-sat-20-46-1
FAIL
900
DW-sat-21-48-1
FAIL
900
DW-sat-22-50-1
FAIL
900
DWs-sat-12-28-1
FAIL
900
DWs-sat-19-41-1
FAIL
900
DWs-sat-20-43-1
FAIL
900
DW-unsat-24-52-1
FAIL
900
DW-unsat-25-54-1
FAIL
900
jctc14-unrolled-fail
FAIL
900
chess_solving_mate_in_3_2001_UKR-CH_06
FAIL
900
chess_solving_mate_in_3_2000_CZE-CH_04
FAIL
900
chess_solving_mate_in_3_1991_WCSC-15_05
FAIL
900
chess_solving_mate_in_3_1978_WCSC-2_05
FAIL
900
chess_composing_8_template_43
FAIL
900
chess_composing_8_template_42
FAIL
900
chess_composing_8_template_38
FAIL
900
chess_composing_8_template_13
FAIL
900
chess_composing_8_template_02
FAIL
900
chess_composing_6_template_06
FAIL
900
chess_composing_6_template_04
FAIL
900
chess_composing_6_template_01
FAIL
900
SR-unsat-04-01-07-2
FAIL
900
SR-sat-04-01-08-2
FAIL
900
SR-sat-03-01-08-2
FAIL
900
SR-sat-03-01-07-3
FAIL
900
chess_solving_mate_in_3_2003_UKR-CH_04
FAIL
900
chess_solving_mate_in_3_2008_ISC-4B_07
FAIL
900
jctc10-fail
FAIL
900
JP-sat-03-08-4
FAIL
900
JP-sat-03-09-6
FAIL
900
JP-sat-03-10-5
FAIL
900
JP-unsat-03-08-3
FAIL
900
JP-unsat-03-08-5
FAIL
900
JP-unsat-03-09-4
FAIL
900
chess_solving_mate_in_4_2001_UKR-CH_13
FAIL
900
chess_solving_mate_in_3_2014_FRA-CH_03
FAIL
900
SR-sat-03-01-07-2
FAIL
900
SR-sat-04-01-08-3
FAIL
900
SR-sat-04-01-09-2
FAIL
900
chess_solving_mate_in_3_2012_GRE-CH-11_02
FAIL
900
chess_solving_mate_in_3_2011_UKR-OPEN-25_04
FAIL
900
SR-unsat-03-01-06-2
FAIL
900
chess_solving_mate_in_3_2010_UKR-CH_04
FAIL
900
JP-unsat-03-07-4
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB