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
quabs___caqe-bloqqer
QBFEVAL'18 - Prenex non-CNF Track
Instance
Result
Time
random-qcir-1000-50-295
UNSAT
0
pg-hkb-6
UNSAT
0
random-qcir-1000-50-545
UNSAT
0
pg-hkb-4
UNSAT
0
pg-hkb-3
UNSAT
0
pg-hkb-2
UNSAT
0
ntrivil_query54_1133
SAT
0
random-qcir-1000-50-658
UNSAT
0
random-qcir-1000-50-68
UNSAT
0
random-qcir-1000-50-743
UNSAT
0
random-qcir-1000-50-754
UNSAT
0
query71_query15_1133
UNSAT
0
small-swap2-fixpoint-4
SAT
0
small-swap1-fixpoint-3
SAT
0
random-qcir-1000-50-473
UNSAT
0
random-qcir-1000-50-456
UNSAT
0
random-qcir-1000-50-275
UNSAT
0
random-qcir-1000-50-267
UNSAT
0
random-qcir-1000-50-255
UNSAT
0
random-qcir-1000-50-134
UNSAT
0
ltl2dpa_C26_comp2_REAL.unsat
UNSAT
0
random-qcir-1000-50-361
UNSAT
0
bs128n.sat
SAT
0
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
0
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
0
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
0
random-qcir-1000-50-393
UNSAT
0
random-qcir-1000-50-428
UNSAT
0
random-qcir-1000-50-441
UNSAT
0
query64_query31_1133
UNSAT
0
rankfunc33_signed_32
SAT
0
rankfunc17_unsigned_16
SAT
0
mv16y.sat
SAT
0
random-qcir-1000-50-930
UNSAT
0
random-qcir-1000-50-940
UNSAT
0
bs128n.unsat
UNSAT
0
mult_bool_matrix_4_5_5.sat
SAT
0
mult_bool_matrix_2_3_30.sat
SAT
0
random-qcir-1000-50-970
UNSAT
0
random-qcir-1000-50-983
UNSAT
0
driver_d9n.unsat
UNSAT
0
driver_a9y.unsat
UNSAT
0
random-qcir-1000-50-857
UNSAT
0
stay22n.unsat
UNSAT
0
k_branch_n-10
SAT
0
k_branch_p-10
UNSAT
0
rankfunc13_unsigned_64
SAT
0
query51_query48_1133
UNSAT
0
query50_query49_1133
UNSAT
0
random-qcir-1000-50-98
UNSAT
0
query30_eequery_1133
SAT
0
random-qcir-1000-50-793
UNSAT
0
random-qcir-1000-50-846
UNSAT
0
pg-hkb-5
UNSAT
0
random-qcir-1000-50-898
UNSAT
0
query04_query03_1133
UNSAT
0
k_branch_p-11
UNSAT
0.01
6s318r_c0to15.unsat
UNSAT
0.01
6s318r_c0to31.sat
SAT
0.01
stay24n.sat
SAT
0.01
k_branch_p-16
UNSAT
0.03
pg-hkb-7
UNSAT
0.04
ev-pr-4x4-13-3-0-0-1-lg
SAT
0.06
incrementer-enc08-uniform-depth-33
SAT
0.63
ltl2dpa_C26_comp3_REAL.unsat
UNSAT
0.65
klieber2017q-108-27-t1
UNSAT
0.67
incrementer-enc07-uniform-depth-25
UNSAT
0.68
query21_reachqu_1133
SAT
0.77
k0206272.s.oe
SAT
0.9
ltl2dpa_C26_comp3_REAL.sat
SAT
0.99
query44_query57_1133
UNSAT
1.03
query33_query71_1344
UNSAT
1.04
query49_query64_1133
UNSAT
1.37
jctc13-fail
UNSAT
1.41
incrementer-enc02-uniform-depth-58
UNSAT
1.49
k0201058.c.oe
SAT
1.49
k_branch_n-12
SAT
1.49
qshifter_7
SAT
1.5
klieber2017q-100-25-t1
UNSAT
1.57
sdlx-fixpoint-3
UNSAT
1.58
klieber2017q-080-20-t1
UNSAT
1.61
filesys_smbmrx_cvsndrcv.c
UNSAT
1.66
nreachq_query02_1344
UNSAT
1.82
load_3c_comp_comp7_REAL.unsat
UNSAT
2.33
amba2f9n.unsat
UNSAT
2.88
query64_query55_1344
UNSAT
2.91
load_full_3_comp3_REAL.unsat
UNSAT
2.96
klieber2017q-078-19-t1
UNSAT
3.09
klieber2017q-084-21-t1
UNSAT
3.59
klieber2017q-086-21-t1
UNSAT
3.65
k0206272.v.oe
SAT
3.81
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
SAT
3.88
cnt14
SAT
3.89
oski3ub1i_c0to63.unsat
UNSAT
3.95
klieber2017q-074-18-t1
UNSAT
4.07
pg-hkb-8
UNSAT
4.14
genbuf5b4n.unsat
UNSAT
4.21
dungeon_i15-m7-u4-v0.pddl_planlen=81
UNSAT
4.35
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
4.91
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
5.27
jctc4-fail
UNSAT
5.78
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
SAT
5.99
klieber2017q-096-24-t1
UNSAT
7.42
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
SAT
8.09
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.asp
SAT
9.24
pg-hkb-9
UNSAT
9.56
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
SAT
10.13
klieber2017q-104-26-t1
UNSAT
10.65
k0206272.h.oe
SAT
10.69
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.asp
SAT
10.8
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
SAT
11.65
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
SAT
13.05
beemldelec4b1_c0to15.unsat
UNSAT
15.33
jctc9-pass
SAT
15.68
klieber2017q-092-23-t1
UNSAT
16
query64_query58_1344
UNSAT
16.1
gb_s2_r2_comp3_REAL.unsat
UNSAT
18.97
k0226271.c.oe
SAT
22.88
k_ph_n-21
SAT
23.36
k0026150.h.oe
SAT
25.05
sortnetsort9.v.stepl.005
UNSAT
25.45
k0225744.s.oe
SAT
25.98
klieber2017q-116-29-t1
UNSAT
28.15
pg-hkb-10
UNSAT
29.07
sortnetsort9.v.stepl.007
SAT
32.69
genbuf9b4n.unsat
UNSAT
45.86
k0225418.v.oe
SAT
53.86
amba2f9n.sat
SAT
61.03
sortnetsort9.AE.stepl.012
UNSAT
66.45
sortnetsort10.v.stepl.005
UNSAT
91.84
genbuf10b4y.unsat
UNSAT
96.85
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.asp
SAT
102.46
ev-pr-6x6-9-5-0-1-2-lg
UNSAT
153.06
query03_query57_1344
SAT
257.79
query09_trivial_1344
SAT
261.92
ev-pr-4x4-11-3-0-0-1-lg
SAT
265.86
query49_query58_1344
UNSAT
284.27
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.asp
UNSAT
327.66
test3_quant_squaring2
UNSAT
344.99
pg-hkb-11
UNSAT
472.96
klieber2017q-112-28-t1
UNSAT
508.05
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
UNSAT
693.57
cycle_sched_6_2_1.sat
SAT
722.57
dungeon_i25-m12-u3-v0.pddl_planlen=190
UNSAT
773.7
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.asp
SAT
799.96
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
UNSAT
831.28
ev-pr-6x6-11-5-0-1-2-lg
UNSAT
864.69
SR-unsat-03-01-06-2
FAIL
900
chess_solving_mate_in_5_1996_UKR-CH-10_15
FAIL
900
JP-unsat-03-08-5
FAIL
900
k0225744.v.oe
FAIL
900
DWs-sat-12-28-1
FAIL
900
CM-sat-04-01-06-4
FAIL
900
CM-sat-02-01-07-3
FAIL
900
DW-unsat-11-27-1
FAIL
900
CM-sat-03-01-06-4
FAIL
900
klieber2017q-108-27-eq
FAIL
900
oski3ub1i_c0to63.sat
FAIL
900
nreachq_reachqu_2133
FAIL
900.01
nreachq_reachqu_2233
FAIL
900.01
jctc3-vals-0,2-pass
FAIL
900.01
pg-hkb-15
FAIL
900.01
pg-hkb-17
FAIL
900.01
CM-sat-03-01-07-3
FAIL
900.01
pg-hkb-22
FAIL
900.01
DW-sat-06-20-1
FAIL
900.01
DW-sat-09-26-1
FAIL
900.01
pg-hkb-23
FAIL
900.01
DW-unsat-11-26-1
FAIL
900.01
mult_bool_matrix_2_3_30.unsat
FAIL
900.01
JP-unsat-03-08-3
FAIL
900.01
k0026150.s.oe
FAIL
900.01
k0206272.connected.oe
FAIL
900.01
k0225682.c.oe
FAIL
900.01
genbuf5b4n.sat
FAIL
900.01
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900.01
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
FAIL
900.01
klieber2017q-076-19-eq
FAIL
900.01
chess_composing_6_template_01
FAIL
900.01
pipesnotankage14_10
FAIL
900.01
chess_solving_mate_in_7_2016_BEL-CH-23A_03
FAIL
900.01
SR-sat-03-01-08-2
FAIL
900.01
JP-unsat-03-07-4
FAIL
900.01
network_irda_miniport_nscirda_comm.c
FAIL
900.01
DWs-unsat-12-25-1
FAIL
900.01
DWs-unsat-11-23-1
FAIL
900.01
test2_quant_squaring2
FAIL
900.01
chess_solving_mate_in_6_1998_OST-CH-1_15
FAIL
900.01
CM-sat-07-01-06-4
FAIL
900.01
DW-sat-08-22-1
FAIL
900.01
chess_solving_mate_in_7_2009_POL-CH-33_15
FAIL
900.01
cycle_sched_6_2_1.unsat
FAIL
900.02
SR-unsat-02-01-05-2
FAIL
900.02
klieber2017q-096-24-eq
FAIL
900.02
SR-sat-03-01-07-2
FAIL
900.02
k0225744.h.oe
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.asp
FAIL
900.02
JP-unsat-03-09-4
FAIL
900.02
chess_solving_mate_in_5_2012_NED-CH-18A_11
FAIL
900.02
chess_solving_mate_in_4_1999_GER-CH-23-6_14
FAIL
900.02
chess_solving_mate_in_4_1984_GBR-CH-5_04
FAIL
900.02
klieber2017q-116-29-eq
FAIL
900.02
CM-sat-07-01-07-3
FAIL
900.02
klieber2017q-078-19-eq
FAIL
900.02
chess_composing_8_template_43
FAIL
900.02
DWs-sat-10-24-1
FAIL
900.02
DW-sat-08-24-1
FAIL
900.02
JP-unsat-02-06-3
FAIL
900.02
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03
FAIL
900.02
query42_query64_1344
FAIL
900.02
JP-sat-03-08-4
FAIL
900.02
CM-sat-04-01-07-3
FAIL
900.02
pipesnotankage18_8
FAIL
900.02
audio_ddksynth_csynth2.cpp
FAIL
900.02
jctc8-pass
FAIL
900.02
DWs-unsat-08-18-1
FAIL
900.02
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.asp
FAIL
900.02
ken.flash^08.C-d4
FAIL
900.02
chess_solving_mate_in_7_2005_GER-CH-29-12_15
FAIL
900.02
DWs-unsat-13-28-1
FAIL
900.02
jctc2-pass
FAIL
900.02
JP-sat-02-07-3
FAIL
900.02
SR-sat-02-01-06-2
FAIL
900.03
pg-hkb-18
FAIL
900.03
chess_composing_8_template_38
FAIL
900.03
klieber2017q-082-20-eq
FAIL
900.03
jctc16-vals-0,2-pass
FAIL
900.03
pg-hkb-21
FAIL
900.03
ken.oop^2.C-d4
FAIL
900.03
jctc5-fail
FAIL
900.03
klieber2017q-112-28-eq
FAIL
900.03
CM-unsat-07-01-06-2
FAIL
900.03
DWs-sat-10-23-1
FAIL
900.03
jctc11-pass
FAIL
900.03
chess_solving_mate_in_2_1983_FIN-CH-4_01
FAIL
900.03
chess_solving_mate_in_6_2016_RUS-CH_15
FAIL
900.03
DWs-unsat-07-16-1
FAIL
900.03
query42_query57_1344
FAIL
900.03
k0300663.v.oe
FAIL
900.03
chess_solving_mate_in_2_2012_GER-CH-36-19_03
FAIL
900.03
DW-sat-08-23-1
FAIL
900.03
beemldelec4b1_c0to15.sat
FAIL
900.03
p20-20.pddl_planlen=23
FAIL
900.03
chess_solving_mate_in_6_2011_SRB-CH_15
FAIL
900.03
chess_solving_mate_in_2_2011_ISC-7B_01
FAIL
900.03
k0300663.s.oe
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.asp
FAIL
900.04
chess_solving_mate_in_5_1984_FIN-CH-5_09
FAIL
900.04
CM-sat-07-01-06-3
FAIL
900.04
SR-sat-02-01-07-2
FAIL
900.04
k_ph_p-12
FAIL
900.04
cnt16r
FAIL
900.04
klieber2017q-104-26-eq
FAIL
900.04
query48_query42_1344
FAIL
900.04
chess_composing_8_template_13
FAIL
900.04
klieber2017q-080-20-eq
FAIL
900.04
mult_bool_matrix_4_5_5.unsat
FAIL
900.04
chess_composing_6_template_04
FAIL
900.04
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01
FAIL
900.04
chess_solving_mate_in_9_2003_RUS-CH_15
FAIL
900.04
klieber2017q-092-23-eq
FAIL
900.04
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.asp
FAIL
900.04
pg-hkb-24
FAIL
900.05
query44_query58_1344
FAIL
900.05
ev-pr-4x4-15-3-0-0-1-s
FAIL
900.05
pg-hkb-26
FAIL
900.05
k0300663.h.oe
FAIL
900.05
chess_solving_mate_in_2_1996_FIN-CH-17_03
FAIL
900.05
DWs-unsat-11-24-1
FAIL
900.05
JP-sat-02-07-4
FAIL
900.05
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.asp
FAIL
900.05
chess_composing_6_template_06
FAIL
900.05
chess_composing_8_template_42
FAIL
900.05
chess_solving_mate_in_3_1999_WCSC-23_05
FAIL
900.05
jctc1-pass
FAIL
900.05
k0225418.connected.oe
FAIL
900.06
chess_solving_mate_in_3_2009_FIN-CH-30_04
FAIL
900.06
chess_solving_mate_in_4_2009_SEROCK-OPEN_09
FAIL
900.06
SR-sat-02-01-06-3
FAIL
900.06
jctc6-pass
FAIL
900.06
k0300663.connected.oe
FAIL
900.06
DWs-unsat-09-19-1
FAIL
900.06
DWs-unsat-08-17-1
FAIL
900.06
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.asp
FAIL
900.06
k0225418.h.oe
FAIL
900.06
p20-1.pddl_planlen=24
FAIL
900.06
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
900.06
k0026150.connected.oe
FAIL
900.06
pg-hkb-16
FAIL
900.06
DWs-sat-10-25-1
FAIL
900.06
klieber2017q-086-21-eq
FAIL
900.06
klieber2017q-100-25-eq
FAIL
900.07
JP-sat-02-08-3
FAIL
900.07
k0302060.c.oe
FAIL
900.07
CM-sat-04-01-06-3
FAIL
900.07
load_full_3_comp3_REAL.sat
FAIL
900.07
jctc7-pass
FAIL
900.07
input_pnpi8042_moudep.c
FAIL
900.07
DW-unsat-09-22-1
FAIL
900.07
k0225418.s.oe
FAIL
900.07
k_ph_p-19
FAIL
900.07
k0225418.c.oe
FAIL
900.07
k0026150.v.oe
FAIL
900.07
chess_solving_mate_in_3_2016_BEL-CH-23A_02
FAIL
900.08
chess_solving_mate_in_7_2011_SVK-CH-19_15
FAIL
900.08
pg-hkb-14
FAIL
900.08
chess_solving_mate_in_8_2011_BEL-CH-19A_03
FAIL
900.08
JP-sat-03-09-4
FAIL
900.08
pg-hkb-19
FAIL
900.08
DW-unsat-10-25-1
FAIL
900.08
query08_query64_1344
FAIL
900.08
DWs-sat-15-35-1
FAIL
900.08
pg-hkb-13
FAIL
900.08
pg-hkb-25
FAIL
900.08
jctc15-unrolled-fail
FAIL
900.09
test2_quant_squaring3
FAIL
900.09
jctc17-vals-0,2-pass
FAIL
900.09
k0225744.connected.oe
FAIL
900.09
jctc18-vals-0,2-pass
FAIL
900.09
p20-5.pddl_planlen=32
FAIL
900.09
SR-unsat-02-01-06-1
FAIL
900.09
query08_query26_1344
FAIL
900.09
pg-hkb-12
FAIL
900.09
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10
FAIL
900.09
chess_composing_8_template_02
FAIL
900.1
test1_quant_squaring3
FAIL
900.1
klieber2017q-074-18-eq
FAIL
900.1
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.asp
FAIL
900.1
jctc14-unrolled-fail
FAIL
900.1
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900.1
gb_s2_r2_comp3_REAL.sat
FAIL
900.1
jctc10-fail
FAIL
900.11
pg-hkb-20
FAIL
900.17
Contact
|
Organization
|
Links
|
Citing QBFLIB