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___plain_qcir_2019
Prenex non-CNF Track
Instance
Result
Time
k0302060.connected.oe
FAIL
0
k0300663.s.oe
FAIL
0
k0300663.v.oe
FAIL
0
eequery_query71_1133
SAT
0
exquery_query64_1133
SAT
0
falsequ_query60_1133
SAT
0
falsequ_query71_1133
SAT
0
k0248814.v.oe
FAIL
0
nxquery_query50_1133
UNSAT
0
trueque_query71_1344
SAT
0
k0325715.connected.oe
FAIL
0
nxquery_query71_1133
UNSAT
0
falsequ_query64_1133
SAT
0
nxquery_query71_1344
SAT
0
query64_query11_1133
UNSAT
0
falsequ_query71_1344
SAT
0
axquery_query64_1133
SAT
0
axquery_query42_1133
SAT
0
k0302060.h.oe
FAIL
0
k0302060.s.oe
FAIL
0
k0325261.connected.oe
FAIL
0
k0325261.h.oe
FAIL
0
k0325261.s.oe
FAIL
0
k0325624.connected.oe
FAIL
0
k0325624.s.oe
FAIL
0
k0325624.v.oe
FAIL
0
k0325715.c.oe
FAIL
0
k0325715.s.oe
FAIL
0
k0326191.connected.oe
FAIL
0
k0326578.connected.oe
FAIL
0
k0327178.c.oe
FAIL
0
k0327620.h.oe
FAIL
0
k0327694.v.oe
FAIL
0
falsequ_query64_1344
SAT
0
exquery_query64_1344
SAT
0
nxquery_query42_1133
SAT
0
k0225418.connected.oe
FAIL
0
k0206272.h.oe
FAIL
0
k0226271.s.oe
FAIL
0
k0225418.v.oe
FAIL
0
k0225744.s.oe
FAIL
0
trueque_query71_1133
SAT
0
trueque_query64_1133
SAT
0
trueque_query60_1133
SAT
0
k0226271.connected.oe
FAIL
0
k0206272.v.oe
FAIL
0
k0206272.s.oe
FAIL
0
k0201058.c.oe
FAIL
0
k0026150.c.oe
FAIL
0
k0248814.h.oe
FAIL
0
axquery_query71_1344
SAT
0
k0026150.h.oe
FAIL
0
k0201058.connected.oe
FAIL
0
k0201058.h.oe
FAIL
0
k0201058.v.oe
FAIL
0
k0206272.c.oe
FAIL
0
trivial_query64_1133
SAT
0
axquery_query71_1133
UNSAT
0.09
exquery_query71_1133
SAT
0.09
exquery_query42_1133
UNSAT
0.1
nxquery_query64_1133
SAT
0.1
eequery_query42_1133
UNSAT
0.11
eequery_query64_1133
UNSAT
0.11
trueque_query64_1344
SAT
0.12
exquery_query71_1344
SAT
0.15
query64_query42_1133
UNSAT
0.15
axquery_query64_1344
SAT
0.16
trivial_query60_1133
SAT
0.17
nreachq_query11_1133
UNSAT
0.17
trivial_query71_1133
SAT
0.17
ntrivil_query71_1133
SAT
0.17
ntrivil_query42_1133
SAT
0.18
k0248814.c.oe
FAIL
0.19
k0300663.c.oe
FAIL
0.19
k0225682.v.oe
FAIL
0.19
ntrivil_query64_1133
SAT
0.19
SR-unsat-02-01-06-1
UNSAT
0.22
query71_query36_1133
UNSAT
0.27
query71_query31_1133
UNSAT
0.27
k0327178.connected.oe
FAIL
0.28
query71_query34_1133
UNSAT
0.28
trivial_query71_1344
SAT
0.39
ntrivil_query71_1344
SAT
0.4
trivial_query64_1344
SAT
0.45
ntrivil_query64_1344
SAT
0.55
nreachq_query54_1133
UNSAT
1.2
nreachq_query71_1133
UNSAT
1.29
jctc6-pass
SAT
2.13
reachqu_query60_1133
SAT
2.34
SR-unsat-03-01-07-1
UNSAT
2.74
DW-sat-04-16-1
SAT
3.28
reachqu_query64_1133
SAT
3.56
jctc13-fail
UNSAT
3.6
jctc1-pass
SAT
3.69
jctc9-pass
SAT
6.09
JP-unsat-02-07-2
UNSAT
6.94
klieber2017q-048-12-t1
UNSAT
6.97
jctc4-fail
UNSAT
9.79
chess_solving_mate_in_2_2009_BEL-CH-17B_01
SAT
12.3
jctc8-pass
SAT
13.06
chess_solving_mate_in_2_2002_WCCC-OPEN-45_01
SAT
13.49
chess_solving_mate_in_2_2011_GBR-CH-32_03
SAT
13.88
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
SAT
14.19
chess_solving_mate_in_2_2014_NED-CH-20B_09
SAT
14.38
jctc16-vals-0,2-pass
SAT
14.48
chess_solving_mate_in_2_1983_FIN-CH-4_01
SAT
15.5
chess_solving_mate_in_2_2008_BEL-CH-16B_08
SAT
16.01
jctc2-pass
SAT
16.62
chess_solving_mate_in_2_2009_POL-CH-33_01
SAT
16.72
chess_solving_mate_in_2_2002_MAC-CH-6_03
SAT
17.09
chess_solving_mate_in_2_2011_ISC-7B_01
SAT
18.68
chess_solving_mate_in_2_1996_FIN-CH-17_03
SAT
20.06
chess_solving_mate_in_2_1998_GBR-CH-19_01
SAT
20.45
chess_solving_mate_in_2_2011_WCCC-OPEN-54_01
SAT
20.6
chess_solving_mate_in_2_2011_ROM-CH-W_02
SAT
22.39
klieber2017q-048-12-eq
SAT
22.75
chess_solving_mate_in_2_1987_FIN-CH-8_01
SAT
22.76
chess_solving_mate_in_2_2015_GBR-CH-36_02
SAT
24.38
chess_solving_mate_in_2_2012_GER-CH-36-19_03
SAT
26.78
chess_solving_mate_in_2_1991_GER-CH-15_01
SAT
27.88
chess_solving_mate_in_2_1982_WCSC-6_02
SAT
30.87
chess_solving_mate_in_2_1997_WCCC-OPEN-40_03
SAT
31.42
klieber2017q-052-13-eq
SAT
37.21
DW-sat-08-23-1
SAT
39.06
chess_solving_mate_in_3_2010_UKR-CH_04
SAT
43.66
chess_solving_mate_in_3_2008_ISC-4B_07
SAT
76.08
klieber2017q-056-14-eq
SAT
81.1
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
87.88
SR-unsat-02-01-05-2
UNSAT
97.06
DW-sat-08-22-1
SAT
102.2
chess_solving_mate_in_3_2011_UKR-OPEN-25_04
SAT
112.11
JP-sat-02-08-3
SAT
112.81
DW-sat-09-26-1
SAT
120.06
chess_solving_mate_in_3_2014_FRA-CH_03
SAT
139.7
DWs-unsat-08-17-1
UNSAT
168.46
klieber2017q-066-16-t1
UNSAT
171.35
chess_solving_mate_in_3_2012_NED-CH-18B_04
SAT
202.4
chess_solving_mate_in_3_1978_WCSC-2_05
SAT
208.22
chess_solving_mate_in_3_1991_WCSC-15_05
SAT
218.87
DW-unsat-09-23-1
UNSAT
244.02
chess_solving_mate_in_3_2001_UKR-CH_06
SAT
252.79
chess_solving_mate_in_4_2001_UKR-CH_13
SAT
256.34
DWs-unsat-08-18-1
UNSAT
258.12
chess_solving_mate_in_3_2012_GRE-CH-11_02
SAT
258.6
chess_solving_mate_in_3_2003_UKR-CH_04
SAT
272.13
DW-unsat-09-22-1
UNSAT
276.37
DWs-sat-10-23-1
SAT
292.45
SR-unsat-04-01-08-1
UNSAT
307.85
klieber2017q-060-15-t1
UNSAT
373.92
JP-sat-02-07-4
SAT
433.75
jctc10-fail
UNSAT
435.59
DWs-unsat-09-19-1
UNSAT
444.29
klieber2017q-062-15-eq
SAT
446.12
DWs-sat-12-28-1
SAT
447.64
SR-sat-02-01-06-2
SAT
483.66
SR-sat-02-01-07-2
SAT
500.82
klieber2017q-060-15-eq
SAT
570.67
chess_solving_mate_in_3_2000_CZE-CH_04
SAT
609.88
eequery_query42_1344
UNSAT
623.34
DW-unsat-10-25-1
UNSAT
627.77
jctc14-unrolled-fail
UNSAT
797.45
amba2c7n.sat
SAT
849.21
DW-sat-21-48-1
FAIL
900
klieber2017q-070-17-t1
FAIL
900
klieber2017q-064-16-eq
FAIL
900
DWs-unsat-10-22-1
FAIL
900
DWs-unsat-22-45-1
FAIL
900
DWs-unsat-23-47-1
FAIL
900
DWs-unsat-24-49-1
FAIL
900
klieber2017q-064-16-t1
FAIL
900
DWs-sat-25-53-1
FAIL
900
DWs-sat-24-51-1
FAIL
900
DWs-sat-23-49-1
FAIL
900
DW-sat-22-50-1
FAIL
900
reachqu_query60_1344
FAIL
900
klieber2017q-068-17-t1
FAIL
900
klieber2017q-070-17-eq
FAIL
900
DWs-sat-19-41-1
FAIL
900
DWs-sat-20-43-1
FAIL
900
DWs-sat-21-45-1
FAIL
900
DWs-sat-22-47-1
FAIL
900
klieber2017q-072-18-eq
FAIL
900
klieber2017q-066-16-eq
FAIL
900
DWs-unsat-25-51-1
FAIL
900
DW-unsat-21-46-1
FAIL
900
JP-unsat-03-08-3
FAIL
900
JP-sat-03-10-5
FAIL
900
JP-sat-03-08-4
FAIL
900
DW-unsat-25-54-1
FAIL
900
DW-unsat-24-52-1
FAIL
900
DW-unsat-23-50-1
FAIL
900
DW-unsat-22-48-1
FAIL
900
JP-unsat-03-08-5
FAIL
900
JP-unsat-03-09-4
FAIL
900
SR-sat-02-01-06-3
FAIL
900
klieber2017q-068-17-eq
FAIL
900
SR-unsat-03-01-06-2
FAIL
900
klieber2017q-072-18-t1
FAIL
900
DW-unsat-11-26-1
FAIL
900
SR-sat-04-01-09-2
FAIL
900
klieber2017q-062-15-t1
FAIL
900
SR-sat-04-01-08-3
FAIL
900
SR-sat-03-01-07-2
FAIL
900
JP-sat-03-09-6
FAIL
900
add20y.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
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
load_full_4_comp3_REAL.unsat
FAIL
900
load_3c_comp_comp7_REAL.unsat
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
genbuf9b4n.unsat
FAIL
900
genbuf10b4n.unsat
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
mult_bool_matrix_17_17_17.sat
FAIL
900
stay24n.sat
FAIL
900
amba3b5y.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
beemskbn1f1_c0to7.sat
FAIL
900
driver_c9y.sat
FAIL
900
driver_c9n.sat
FAIL
900
driver_b8n.sat
FAIL
900
driver_a10y.sat
FAIL
900
cycle_sched_6_6_2.sat
FAIL
900
cycle_sched_4_4_2.sat
FAIL
900
cycle_sched_2_10_1.sat
FAIL
900
cycle_sched_12_2_1.sat
FAIL
900
amba4b9y.unsat
FAIL
900
amba2f9n.sat
FAIL
900
reachqu_query71_1344
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#288.w#4.s#8.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.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#368.w#6.s#7.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp
FAIL
900
reachqu_query64_1344
FAIL
900
nreachq_query71_1344
FAIL
900
eequery_query64_1344
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#392.w#6.s#4.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#384.w#6.s#3.asp
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#200.w#6.s#6.asp
FAIL
900
bs128n.sat
FAIL
900
DW-sat-20-46-1
FAIL
900
jctc18-vals-0,2-pass
FAIL
900
jctc17-vals-0,2-pass
FAIL
900
SR-sat-03-01-08-2
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-07-3
FAIL
900
jctc5-fail
FAIL
900
CM-sat-04-01-06-3
FAIL
900
CM-sat-04-01-06-4
FAIL
900
DW-sat-18-42-1
FAIL
900
DW-sat-17-40-1
FAIL
900
CM-unsat-21-01-05-3
FAIL
900
CM-unsat-20-01-05-3
FAIL
900
CM-unsat-19-01-05-3
FAIL
900
CM-unsat-16-01-05-3
FAIL
900
CM-unsat-15-01-05-3
FAIL
900
CM-unsat-14-01-05-3
FAIL
900
CM-unsat-13-01-05-3
FAIL
900
CM-sat-21-01-06-3
FAIL
900
CM-sat-20-01-06-3
FAIL
900
CM-sat-19-01-06-3
FAIL
900
CM-sat-18-01-07-3
FAIL
900
CM-sat-04-01-07-3
FAIL
900
JP-unsat-03-07-4
FAIL
900
JP-unsat-02-06-3
FAIL
900
JP-sat-03-09-5
FAIL
900
klieber2017q-088-22-t1
FAIL
900
klieber2017q-088-22-eq
FAIL
900
klieber2017q-086-21-t1
FAIL
900
klieber2017q-084-21-t1
FAIL
900
klieber2017q-084-21-eq
FAIL
900
klieber2017q-082-20-t1
FAIL
900
klieber2017q-080-20-t1
FAIL
900
klieber2017q-078-19-t1
FAIL
900
klieber2017q-078-19-eq
FAIL
900
klieber2017q-076-19-t1
FAIL
900
klieber2017q-076-19-eq
FAIL
900
klieber2017q-074-18-t1
FAIL
900
klieber2017q-074-18-eq
FAIL
900
mult9.sat
FAIL
900
klieber2017q-100-25-t1
FAIL
900
klieber2017q-104-26-t1
FAIL
900
klieber2017q-108-27-t1
FAIL
900
JP-sat-03-09-4
FAIL
900
JP-sat-03-08-5
FAIL
900
DW-unsat-20-44-1
FAIL
900
DWs-unsat-11-24-1
FAIL
900
DWs-unsat-11-23-1
FAIL
900
DWs-sat-10-25-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
CM-sat-07-01-07-3
FAIL
900
CM-sat-07-01-06-4
FAIL
900
CM-sat-07-01-06-3
FAIL
900
klieber2017q-112-28-t1
FAIL
900
bs128y.sat
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB