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
cqesto
QBFEVAL'17 - Prenex non-CNF Track
Instance
Result
Time
mutex-4-s
SAT
0
halfadder_match2.sat
SAT
0
halfadder_match2.unsat
UNSAT
0
mvs16y.unsat
UNSAT
0.01
stmt16_950_951
SAT
0.01
stmt41_738_749
SAT
0.03
mutex-32-s
SAT
0.04
stay24n.unsat
UNSAT
0.05
C499.blif_0.10_1.00_0_0_out_exact
UNSAT
0.05
Core1108_tbm_02.tex.moduleQ3.2S.000015
UNSAT
0.05
mutex-64-s
SAT
0.08
incrementer-enc07-uniform-depth-25
UNSAT
0.11
CHAIN20v.21
SAT
0.14
CHAIN22v.23
SAT
0.18
CHAIN23v.24
SAT
0.2
incrementer-enc08-uniform-depth-33
SAT
0.27
SR-unsat-03-01-07-1
UNSAT
0.38
klieber2017q-080-20-eq
SAT
0.44
klieber2017q-078-19-t1
UNSAT
0.47
klieber2017q-086-21-eq
SAT
0.48
incrementer-enc02-uniform-depth-58
UNSAT
0.5
klieber2017q-080-20-t1
UNSAT
0.52
klieber2017q-112-28-t1
UNSAT
0.56
klieber2017q-078-19-eq
SAT
0.58
filesys_smbmrx_cvsndrcv.c
UNSAT
0.66
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
0.68
klieber2017q-096-24-eq
SAT
0.68
klieber2017q-082-20-eq
SAT
0.72
klieber2017q-076-19-eq
SAT
0.79
klieber2017q-086-21-t1
UNSAT
0.81
szymanski-5-s
UNSAT
0.82
oski3ub5i_c0to255.unsat
UNSAT
0.84
driver_d9y.unsat
UNSAT
0.85
klieber2017q-092-23-eq
SAT
0.9
JP-unsat-02-07-2
UNSAT
0.91
klieber2017q-100-25-t1
UNSAT
1.01
klieber2017q-088-22-eq
SAT
1.01
klieber2017q-074-18-eq
SAT
1.03
klieber2017q-074-18-t1
UNSAT
1.12
klieber2017q-084-21-eq
SAT
1.3
beemldelec4b1_c0to127.unsat
UNSAT
1.3
ltl2dba_C2-6_comp3_REAL.unsat
UNSAT
1.37
assertion12_0_1
UNSAT
1.45
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
1.66
klieber2017q-104-26-t1
UNSAT
1.93
uclid-pipe3a
SAT
2.04
klieber2017q-108-27-eq
SAT
2.35
JP-unsat-02-06-3
UNSAT
2.57
C499.blif_0.10_0.20_0_0_out_exact
UNSAT
2.77
klieber2017q-084-21-t1
UNSAT
2.77
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
2.79
C499.blif_0.10_0.20_0_1_out_exact
UNSAT
3.2
ev-pr-4x4-13-3-0-0-1-lg
SAT
3.36
klieber2017q-092-23-t1
UNSAT
3.45
szymanski-6-s
UNSAT
3.65
consistency_0_1
SAT
3.66
klieber2017q-088-22-t1
UNSAT
3.83
klieber2017q-108-27-t1
UNSAT
4.61
DW-sat-08-24-1
SAT
4.8
klieber2017q-104-26-eq
SAT
5.16
DW-sat-08-23-1
SAT
5.21
sortnetsort9.AE.stepl.012
UNSAT
6.2
arbiter-08-comp-error02-qbf-hardness-depth-9
SAT
6.33
klieber2017q-100-25-eq
SAT
7.66
DW-sat-08-22-1
SAT
9.65
SR-unsat-04-01-08-1
UNSAT
11.44
klieber2017q-116-29-eq
SAT
11.57
possibility10_0_1
UNSAT
12.05
vonNeumann-ripple-carry-12-c
UNSAT
13.63
klieber2017q-112-28-eq
SAT
14.63
klieber2017q-076-19-t1
UNSAT
15.11
possibility5_0_1
UNSAT
15.43
consistency_0_2
SAT
16.38
ev-pr-8x8-7-7-0-1-2-lg
UNSAT
19.05
klieber2017q-096-24-t1
UNSAT
21.99
DW-unsat-08-21-1
UNSAT
23.25
stmt17_63_82
SAT
26.96
stmt28_68_81
SAT
30.92
szymanski-8-s
UNSAT
33.46
stmt17_70_90
SAT
35.33
fpu-10Xe-correct01-nonuniform-depth-24
UNSAT
36.93
stmt19_64_99
SAT
37.33
DWs-sat-10-25-1
SAT
39.44
consistency_0_3
SAT
44.84
k_ph_n-21
SAT
47.32
stmt17_86_98
SAT
50.08
fpu-10Xh-correct04-nonuniform-depth-27
UNSAT
52.56
assertion4_0_10
FAIL
52.83
consistency_0_10
FAIL
53.01
assertion2_0_8
FAIL
53.85
possibility10_0_7
FAIL
54.14
consistency_0_9
FAIL
54.54
possibility8_0_7
FAIL
54.95
possibility8_0_1
SAT
55.46
possibility1_0_8
FAIL
55.55
assertion5_0_9
FAIL
55.63
possibility11_0_7
FAIL
55.67
possibility4_0_7
FAIL
56.19
possibility5_0_9
FAIL
56.33
possibility6_0_7
FAIL
56.56
consistency_0_7
FAIL
56.94
possibility6_0_10
FAIL
57
assertion1_0_10
FAIL
57.12
assertion9_0_7
FAIL
57.67
assertion10_0_9
FAIL
57.92
consistency_0_8
FAIL
61.58
assertion1_0_9
FAIL
63.38
assertion11_0_7
FAIL
63.84
DW-unsat-09-23-1
UNSAT
67.99
DW-unsat-09-22-1
UNSAT
70.37
possibility7_0_6
FAIL
74.43
assertion10_0_6
FAIL
78.52
possibility3_0_6
FAIL
78.78
assertion3_0_6
FAIL
79.03
klieber2017q-116-29-t1
UNSAT
82.46
consistency_0_4
SAT
89.02
assertion2_0_6
FAIL
91.16
DWs-sat-10-23-1
SAT
130.87
DWs-sat-10-24-1
SAT
162.64
consistency_0_5
SAT
163.47
consistency_0_6
FAIL
177.99
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
178.12
JP-unsat-03-07-4
UNSAT
185.16
DWs-unsat-11-23-1
UNSAT
204.94
C880.blif_0.10_1.00_0_0_inp_exact
UNSAT
215.36
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
SAT
241.18
CM-unsat-07-01-06-2
UNSAT
280.14
DWs-unsat-11-24-1
UNSAT
348.36
CM-sat-07-01-06-3
SAT
396.83
ev-pr-6x6-9-5-0-1-2-lg
UNSAT
418.45
ev-pr-4x4-11-3-0-0-1-lg
SAT
458.69
klieber2017q-082-20-t1
UNSAT
474.18
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.asp
SAT
536.77
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.asp
SAT
544.3
k_branch_p-10
UNSAT
552.38
DWs-unsat-12-25-1
UNSAT
588.86
SR-sat-03-01-08-2
SAT
622.39
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.asp
SAT
783.6
JP-sat-03-09-5
FAIL
900
DW-sat-19-46-1
FAIL
900
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.asp
FAIL
900
DW-sat-19-45-1
FAIL
900
DW-sat-19-44-1
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#344.w#4.s#5.asp
FAIL
900
CM-unsat-18-01-05-3
FAIL
900
CM-unsat-17-01-06-2
FAIL
900
CM-unsat-17-01-05-3
FAIL
900
CM-unsat-08-01-05-3
FAIL
900
SR-unsat-04-01-07-2
FAIL
900
SR-sat-04-01-08-2
FAIL
900
JP-sat-03-09-4
FAIL
900
JP-sat-03-08-5
FAIL
900
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.asp
FAIL
900
DW-unsat-20-44-1
FAIL
900
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.asp
FAIL
900
DW-unsat-19-43-1
FAIL
900
DW-unsat-19-42-1
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#336.w#4.s#5.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.asp
FAIL
900
SR-sat-03-01-07-3
FAIL
900
ci.e#1.a#3.E#40.A#60.c#408.w#4.s#3.asp
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
ltl2dpa_C26_comp2_REAL.unsat
FAIL
900
mult_bool_matrix_10_9_11.unsat
FAIL
900
driver_a9n.sat
FAIL
900
driver_a9n.unsat
FAIL
900
driver_d9y.sat
FAIL
900
mult_bool_matrix_10_9_11.sat
FAIL
900
genbuf10b4n.sat
FAIL
900
genbuf10b4n.unsat
FAIL
900
genbuf9b4n.sat
FAIL
900
genbuf9b4n.unsat
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
oski3ub5i_c0to255.sat
FAIL
900
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
load_full_4_comp3_REAL.unsat
FAIL
900
load_full_4_comp3_REAL.sat
FAIL
900
load_3c_comp_comp7_REAL.sat
FAIL
900
cycle_sched_6_7_1.unsat
FAIL
900
mult_bool_matrix_17_17_17.sat
FAIL
900
CM-unsat-07-01-05-3
FAIL
900
CM-sat-17-01-07-3
FAIL
900
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
FAIL
900
CM-sat-17-01-06-4
FAIL
900
amba2f9n.sat
FAIL
900
amba2f9n.unsat
FAIL
900
amba4b9y.sat
FAIL
900
amba4b9y.unsat
FAIL
900
CM-sat-17-01-06-3
FAIL
900
CM-sat-07-01-07-3
FAIL
900
CM-sat-07-01-06-4
FAIL
900
cycle_sched_4_7_1.unsat
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
stay24n.sat
FAIL
900
mvs16y.sat
FAIL
900
mult_bool_matrix_17_17_17.unsat
FAIL
900
load_3c_comp_comp7_REAL.unsat
FAIL
900
ring_r6_ser--opt-17_
FAIL
900
cnt14
FAIL
900
k_ph_p-19
FAIL
900
k_branch_p-11
FAIL
900
k_branch_n-10
FAIL
900
adder-12-unsat
FAIL
900
ev-pr-8x8-15-7-0-1-2-lg
FAIL
900
szymanski-16-s
FAIL
900
test3_quant_squaring2
FAIL
900
test3_quant_squaring4
FAIL
900
szymanski-14-s
FAIL
900
Adder2-16-s
FAIL
900
s3330_d9_s
FAIL
900
test1_quant_squaring3
FAIL
900
cnt16r
FAIL
900
s1269_d15_u
FAIL
900
emptyroom_e4_ser--opt-44_
FAIL
900
cube_c7_ser--opt-24_
FAIL
900
c4_Debug_s5_f2_e2_v1
FAIL
900
c4_Debug_s3_f2_e2_v2
FAIL
900
c3_Debug_s3_f2_e2_v2
FAIL
900
c2_Debug_s3_f1_e1_v2
FAIL
900
c1_Debug_s5_f1_e1_v2
FAIL
900
sortnetsort9.v.stepl.007
FAIL
900
sortnetsort9.v.stepl.005
FAIL
900
sortnetsort10.v.stepl.005
FAIL
900
ken.oop^2.C-d4
FAIL
900
ken.flash^08.C-d4
FAIL
900
s3330_d12_u
FAIL
900
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
900
k_ph_p-12
FAIL
900
qshifter_7
FAIL
900
ev-pr-6x6-17-5-0-1-2-s
FAIL
900
ev-pr-6x6-13-5-0-1-2-s
FAIL
900
k_branch_n-12
FAIL
900
k_branch_p-16
FAIL
900
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
900
ev-pr-6x6-11-5-0-1-2-s
FAIL
900
ev-pr-4x4-15-3-0-0-1-s
FAIL
900
adder-10-sat
FAIL
900
connect_8x7_6_R
FAIL
900
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900
adder-14-sat
FAIL
900
qshifter_8
FAIL
900
ev-pr-8x8-13-7-0-1-2-lg
FAIL
900
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
900
ev-pr-4x4-13-3-0-0-1-s
FAIL
900
ev-pr-4x4-17-3-0-0-1-s
FAIL
900
uclid-pipe2
FAIL
900
C6288.blif_0.10_0.20_0_1_out_exact
FAIL
900
ev-pr-8x8-19-7-0-1-2-lg
FAIL
900
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
900
test2_quant_squaring3
FAIL
900
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
900
ev-pr-4x4-7-3-0-0-1-s
FAIL
900
ev-pr-6x6-9-5-0-1-2-s
FAIL
900
test2_quant_squaring2
FAIL
900
ev-pr-6x6-19-5-0-1-2-lg
FAIL
900
BLOCKS4iii.6
FAIL
900
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.asp
FAIL
900
assertion12_0_2
FAIL
900
assertion1_0_4
FAIL
900
s15850_PR_8_50
FAIL
900
query44_query26_1344n
FAIL
900
query42_query06_1344n
FAIL
900
pipesnotankage18_8
FAIL
900
pipesnotankage14_10
FAIL
900
p20-5.pddl_planlen=32
FAIL
900
p20-20.pddl_planlen=23
FAIL
900
p20-1.pddl_planlen=24
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
900
assertion2_0_3
FAIL
900
assertion2_0_5
FAIL
900
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.asp
FAIL
900
possibility7_0_3
FAIL
900
possibility6_0_3
FAIL
900
possibility5_0_4
FAIL
900
possibility4_0_5
FAIL
900
possibility3_0_3
FAIL
900
possibility10_0_2
FAIL
900
possibility1_0_3
FAIL
900
connect_9x8_6_R
FAIL
900
assertion9_0_3
FAIL
900
assertion7_0_4
FAIL
900
assertion7_0_3
FAIL
900
assertion6_0_3
FAIL
900
b22_PR_8_20
FAIL
900
b21_C_3_206
FAIL
900
rankfunc33_signed_32
FAIL
900
rankfunc17_unsigned_16
FAIL
900
rankfunc13_unsigned_64
FAIL
900
s1269_d12_u
FAIL
900
s1269_d13_u
FAIL
900
k5_2_3
FAIL
900
k14_2_3
FAIL
900
k8_2_3
FAIL
900
k12_4_2
FAIL
900
stmt41_160_235
FAIL
900
f600-50
FAIL
900
c5_BMC_p2_k64
FAIL
900
c5_BMC_p2_k128
FAIL
900
rankfunc5_unsigned_64
FAIL
900
rankfunc14_signed_64
FAIL
900
b20_PR_7_20
FAIL
900
b20_C_3_2
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
900
audio_ddksynth_csynth2.cpp
FAIL
900
network_irda_miniport_nscirda_comm.c
FAIL
900
input_pnpi8042_moudep.c
FAIL
900
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
900
small-swap2-fixpoint-4
FAIL
900
small-synabs-fixpoint-9
FAIL
900
small-swap1-fixpoint-3
FAIL
900
sdlx-fixpoint-3
FAIL
900
cache-coherence-2-fixpoint-6
FAIL
900
Umbrella_tbm_05.tex.module.000039
FAIL
900
c2_BMC_p1_k2048
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB