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
QBFEVAL'17 - Prenex non-CNF Track
Instance
Result
Time
halfadder_match2.unsat
UNSAT
0.07
halfadder_match2.sat
SAT
0.07
mvs16y.unsat
UNSAT
0.1
driver_d9y.unsat
UNSAT
0.21
stmt16_950_951
SAT
0.28
ltl2dba_C2-6_comp3_REAL.unsat
UNSAT
0.35
stmt41_738_749
SAT
0.45
C499.blif_0.10_1.00_0_0_out_exact
UNSAT
0.55
stay24n.unsat
UNSAT
0.7
assertion12_0_1
UNSAT
0.95
ltl2dpa_C26_comp2_REAL.unsat
UNSAT
0.97
BLOCKS4iii.6
UNSAT
1.65
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.asp
SAT
2.55
incrementer-enc08-uniform-depth-33
SAT
3.47
SR-unsat-03-01-07-1
UNSAT
3.67
JP-unsat-02-07-2
UNSAT
3.8
klieber2017q-104-26-t1
UNSAT
6.36
klieber2017q-078-19-eq
SAT
7.28
klieber2017q-076-19-eq
SAT
7.34
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.asp
SAT
7.64
beemldelec4b1_c0to127.unsat
UNSAT
8.49
klieber2017q-108-27-t1
UNSAT
8.82
incrementer-enc07-uniform-depth-25
UNSAT
9.04
klieber2017q-076-19-t1
UNSAT
9.24
klieber2017q-082-20-t1
UNSAT
9.94
klieber2017q-074-18-t1
UNSAT
10.19
klieber2017q-074-18-eq
SAT
11.4
klieber2017q-086-21-eq
SAT
12.39
JP-unsat-02-06-3
UNSAT
14.18
oski3ub5i_c0to255.unsat
UNSAT
15.24
klieber2017q-112-28-t1
UNSAT
16.22
klieber2017q-082-20-eq
SAT
18.33
klieber2017q-100-25-t1
UNSAT
20.43
klieber2017q-080-20-t1
UNSAT
21.88
klieber2017q-084-21-eq
SAT
22.31
klieber2017q-092-23-t1
UNSAT
24.54
klieber2017q-100-25-eq
SAT
25.21
driver_a9n.unsat
UNSAT
27.6
amba2f9n.unsat
UNSAT
30.2
possibility5_0_1
UNSAT
31.47
klieber2017q-096-24-t1
UNSAT
31.87
klieber2017q-088-22-t1
UNSAT
35.32
possibility10_0_1
UNSAT
38.61
SR-unsat-04-01-08-1
UNSAT
39.18
klieber2017q-078-19-t1
UNSAT
41.16
load_3c_comp_comp7_REAL.unsat
UNSAT
41.68
klieber2017q-104-26-eq
SAT
53.98
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.asp
SAT
54.15
klieber2017q-092-23-eq
SAT
60.78
b22_PR_8_20
SAT
61.19
klieber2017q-086-21-t1
UNSAT
62.41
b20_PR_7_20
SAT
64.31
klieber2017q-096-24-eq
SAT
65.55
DW-sat-08-24-1
SAT
66.55
klieber2017q-088-22-eq
SAT
73.48
klieber2017q-116-29-eq
SAT
76.49
DW-sat-08-22-1
SAT
82.9
DW-sat-08-23-1
SAT
92.2
DWs-sat-10-25-1
SAT
94.13
DW-unsat-08-21-1
UNSAT
98.19
CM-sat-07-01-06-3
SAT
153.1
DW-unsat-09-22-1
UNSAT
166.36
klieber2017q-084-21-t1
UNSAT
170.72
stmt28_68_81
SAT
208.27
klieber2017q-080-20-eq
SAT
217.2
DW-unsat-09-23-1
UNSAT
225.19
DWs-sat-10-24-1
SAT
227
klieber2017q-112-28-eq
SAT
227.53
incrementer-enc02-uniform-depth-58
UNSAT
230.78
cube_c7_ser--opt-24_
SAT
287.95
genbuf9b4n.unsat
UNSAT
311.58
fpu-10Xe-correct01-nonuniform-depth-24
UNSAT
331.47
fpu-10Xh-correct04-nonuniform-depth-27
UNSAT
341.01
ev-pr-4x4-11-3-0-0-1-lg
SAT
341.53
vonNeumann-ripple-carry-12-c
UNSAT
381.58
stmt17_86_98
SAT
389.08
DWs-sat-10-23-1
SAT
393.18
genbuf10b4n.unsat
UNSAT
457.98
stmt17_70_90
SAT
470.59
DWs-unsat-11-23-1
UNSAT
551.29
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.asp
SAT
561.11
stmt17_63_82
SAT
581.7
CM-sat-07-01-06-4
SAT
600.67
ev-pr-4x4-13-3-0-0-1-lg
SAT
613.04
klieber2017q-116-29-t1
UNSAT
623.74
stmt19_64_99
SAT
713.28
ev-pr-6x6-9-5-0-1-2-lg
UNSAT
721.55
CM-sat-07-01-07-3
SAT
743.49
DWs-unsat-11-24-1
UNSAT
865.7
c3_Debug_s3_f2_e2_v2
FAIL
889.42
SR-sat-03-01-07-3
FAIL
891.15
pipesnotankage18_8
FAIL
892.38
CM-sat-17-01-06-4
FAIL
892.77
p20-20.pddl_planlen=23
FAIL
895.02
SR-sat-04-01-08-2
FAIL
896.24
CM-sat-17-01-07-3
FAIL
896.68
pipesnotankage14_10
FAIL
896.71
SR-unsat-04-01-07-2
FAIL
896.79
c2_BMC_p1_k2048
FAIL
896.96
CM-sat-17-01-06-3
FAIL
896.97
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#2.s#3.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#376.w#2.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#392.w#6.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#408.w#4.s#3.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#424.w#2.s#1.asp
FAIL
900
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.asp
FAIL
900
JP-sat-03-09-4
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
possibility3_0_3
FAIL
900
possibility3_0_6
FAIL
900
possibility4_0_5
FAIL
900
possibility4_0_7
FAIL
900
possibility5_0_4
FAIL
900
possibility5_0_9
FAIL
900
possibility6_0_10
FAIL
900
possibility6_0_3
FAIL
900
possibility6_0_7
FAIL
900
possibility7_0_3
FAIL
900
possibility7_0_6
FAIL
900
possibility8_0_1
FAIL
900
possibility8_0_7
FAIL
900
SR-sat-03-01-08-2
FAIL
900
JP-unsat-03-07-4
FAIL
900
JP-sat-03-09-5
FAIL
900
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.asp
FAIL
900
possibility11_0_7
FAIL
900
amba2f9n.sat
FAIL
900
JP-sat-03-08-5
FAIL
900
CM-unsat-17-01-05-3
FAIL
900
oski3ub5i_c0to255.sat
FAIL
900
CM-unsat-08-01-05-3
FAIL
900
CM-unsat-07-01-06-2
FAIL
900
CM-unsat-07-01-05-3
FAIL
900
load_3c_comp_comp7_REAL.sat
FAIL
900
load_full_4_comp3_REAL.sat
FAIL
900
load_full_4_comp3_REAL.unsat
FAIL
900
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
mult_bool_matrix_17_17_17.unsat
FAIL
900
mult_bool_matrix_10_9_11.sat
FAIL
900
mult_bool_matrix_10_9_11.unsat
FAIL
900
mult_bool_matrix_17_17_17.sat
FAIL
900
connect_9x8_6_R
FAIL
900
klieber2017q-108-27-eq
FAIL
900
stay24n.sat
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
CM-unsat-17-01-06-2
FAIL
900
genbuf9b4n.sat
FAIL
900
amba4b9y.sat
FAIL
900
amba4b9y.unsat
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
DW-unsat-20-44-1
FAIL
900
cycle_sched_4_7_1.unsat
FAIL
900
DW-unsat-19-43-1
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
cycle_sched_6_7_1.unsat
FAIL
900
driver_a9n.sat
FAIL
900
DW-unsat-19-42-1
FAIL
900
DWs-unsat-12-25-1
FAIL
900
DW-sat-19-46-1
FAIL
900
DW-sat-19-45-1
FAIL
900
driver_d9y.sat
FAIL
900
DW-sat-19-44-1
FAIL
900
genbuf10b4n.sat
FAIL
900
CM-unsat-18-01-05-3
FAIL
900
mvs16y.sat
FAIL
900
possibility10_0_7
FAIL
900
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900
C499.blif_0.10_0.20_0_0_out_exact
FAIL
900
adder-12-unsat
FAIL
900
szymanski-6-s
FAIL
900
ev-pr-8x8-15-7-0-1-2-lg
FAIL
900
szymanski-16-s
FAIL
900
szymanski-8-s
FAIL
900
test3_quant_squaring2
FAIL
900
test3_quant_squaring4
FAIL
900
k_ph_n-21
FAIL
900
CHAIN22v.23
FAIL
900
C880.blif_0.10_1.00_0_0_inp_exact
FAIL
900
szymanski-14-s
FAIL
900
Adder2-16-s
FAIL
900
s3330_d9_s
FAIL
900
test1_quant_squaring3
FAIL
900
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
900
k_branch_n-10
FAIL
900
k_branch_p-10
FAIL
900
c4_Debug_s5_f2_e2_v1
FAIL
900
c4_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
sortnetsort9.AE.stepl.012
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
s1269_d15_u
FAIL
900
cnt16r
FAIL
900
cnt14
FAIL
900
k_ph_p-19
FAIL
900
k_branch_p-11
FAIL
900
k_ph_p-12
FAIL
900
CHAIN23v.24
FAIL
900
ev-pr-6x6-19-5-0-1-2-lg
FAIL
900
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
900
ev-pr-8x8-13-7-0-1-2-lg
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
mutex-64-s
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
test2_quant_squaring2
FAIL
900
ev-pr-6x6-9-5-0-1-2-s
FAIL
900
C499.blif_0.10_0.20_0_1_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
ev-pr-8x8-7-7-0-1-2-lg
FAIL
900
uclid-pipe3a
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
CHAIN20v.21
FAIL
900
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
900
mutex-32-s
FAIL
900
mutex-4-s
FAIL
900
szymanski-5-s
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
qshifter_8
FAIL
900
emptyroom_e4_ser--opt-44_
FAIL
900
possibility10_0_2
FAIL
900
assertion4_0_10
FAIL
900
assertion3_0_6
FAIL
900
assertion2_0_8
FAIL
900
assertion2_0_6
FAIL
900
assertion2_0_5
FAIL
900
assertion2_0_3
FAIL
900
assertion12_0_2
FAIL
900
assertion11_0_7
FAIL
900
assertion10_0_9
FAIL
900
assertion10_0_6
FAIL
900
assertion1_0_9
FAIL
900
assertion1_0_4
FAIL
900
assertion1_0_10
FAIL
900
s15850_PR_8_50
FAIL
900
query44_query26_1344n
FAIL
900
query42_query06_1344n
FAIL
900
assertion5_0_9
FAIL
900
assertion6_0_3
FAIL
900
possibility1_0_8
FAIL
900
possibility1_0_3
FAIL
900
consistency_0_9
FAIL
900
consistency_0_8
FAIL
900
consistency_0_7
FAIL
900
consistency_0_6
FAIL
900
consistency_0_5
FAIL
900
consistency_0_4
FAIL
900
consistency_0_3
FAIL
900
consistency_0_2
FAIL
900
consistency_0_10
FAIL
900
consistency_0_1
FAIL
900
assertion9_0_7
FAIL
900
assertion9_0_3
FAIL
900
assertion7_0_4
FAIL
900
assertion7_0_3
FAIL
900
p20-5.pddl_planlen=32
FAIL
900
p20-1.pddl_planlen=24
FAIL
900
Umbrella_tbm_05.tex.module.000039
FAIL
900
rankfunc14_signed_64
FAIL
900
rankfunc5_unsigned_64
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
Core1108_tbm_02.tex.moduleQ3.2S.000015
FAIL
900
cache-coherence-2-fixpoint-6
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
b21_C_3_206
FAIL
900
b20_C_3_2
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
900
arbiter-08-comp-error02-qbf-hardness-depth-9
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
filesys_smbmrx_cvsndrcv.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
ring_r6_ser--opt-17_
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB