eval10

Overview

number of participating solvers: 16
number of participating formulas: 568

Overall Solving Statistics

SOLVER SAT UNSAT TOTAL

bdepqbf 226 239 465

hiqqer3 211 237 448

runAqme.sh 184 226 410

pre_dual_ooq.py 185 222 407

dual_ooq 178 222 400

run_rareqs 178 216 394

ghostq-bq-cegar.sh 182 209 391

squeezebf1.2-qube7.2.pl 163 221 384

ghostq-cegar.sh 179 204 383

depqbf 165 217 382

qube7.2 131 226 357

squeezebf1.2-qube3.0 143 206 349

ghostq.sh 167 166 333

ooq 97 164 261

qcnf2z3 107 122 229

StruQS 102 123 225

Number of Solved Formulas

Number of Solved Formulas
SOLVER	SAT	UNSAT	TOTAL
bdepqbf	226	239	465
hiqqer3	211	237	448
runAqme.sh	184	226	410
pre_dual_ooq.py	185	222	407
dual_ooq	178	222	400
run_rareqs	178	216	394
ghostq-bq-cegar.sh	182	209	391
squeezebf1.2-qube7.2.pl	163	221	384
ghostq-cegar.sh	179	204	383
depqbf	165	217	382
qube7.2	131	226	357
squeezebf1.2-qube3.0	143	206	349
ghostq.sh	167	166	333
ooq	97	164	261
qcnf2z3	107	122	229
StruQS	102	123	225

solver AVERAGE SUM

bdepqbf 117.17 66555.85

hiqqer3 138.63 78743.96

runAqme.sh 161.76 91881.87

run_rareqs 163.10 92643.06

pre_dual_ooq.py 166.62 94640.42

dual_ooq 169.80 96448.56

ghostq-bq-cegar.sh 174.19 98943.02

depqbf 180.80 102694.90

ghostq-cegar.sh 183.66 104320.29

squeezebf1.2-qube7.2.pl 191.80 108945.09

squeezebf1.2-qube3.0 211.99 120414.79

qube7.2 214.65 121922.66

ghostq.sh 222.01 126105.53

ooq 283.59 161081.46

qcnf2z3 304.24 172813.42

StruQS 329.01 186881.87

Time Statistics (overall runtime, average runtime)

Time Statistics (overall runtime, average runtime)
solver	AVERAGE	SUM
bdepqbf	117.17	66555.85
hiqqer3	138.63	78743.96
runAqme.sh	161.76	91881.87
run_rareqs	163.10	92643.06
pre_dual_ooq.py	166.62	94640.42
dual_ooq	169.80	96448.56
ghostq-bq-cegar.sh	174.19	98943.02
depqbf	180.80	102694.90
ghostq-cegar.sh	183.66	104320.29
squeezebf1.2-qube7.2.pl	191.80	108945.09
squeezebf1.2-qube3.0	211.99	120414.79
qube7.2	214.65	121922.66
ghostq.sh	222.01	126105.53
ooq	283.59	161081.46
qcnf2z3	304.24	172813.42
StruQS	329.01	186881.87

formula

adder-12-unsat-shuffled.qdimacs

adder-8-unsat-shuffled.qdimacs

connect_7x6_4_R-shuffled.qdimacs

adder-14-sat-shuffled.qdimacs

blocks_enc_2_b4_ser--opt-26_-shuffled.qdimacs

C6288.blif_0.10_0.20_0_0_out_exact-shuffled.qdimacs

C5315.blif_0.10_0.20_0_0_inp_exact-shuffled.qdimacs

k_ph_p-12-shuffled.qdimacs

C5315.blif_0.10_0.20_0_0_out_exact-shuffled.qdimacs

adder-12-sat-shuffled.qdimacs

Adder2-10-s-shuffled.qdimacs

ev-pr-8x8-19-7-0-1-2-lg-shuffled.qdimacs

f600-00-shuffled.qdimacs

C5315.blif_0.10_0.20_0_1_inp_exact-shuffled.qdimacs

connect_9x8_3_R-shuffled.qdimacs

C6288.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimacs

cube_c7_ser---23_-shuffled.qdimacs

C5315.blif_0.10_0.20_0_1_out_exact-shuffled.qdimacs

ev-pr-6x6-15-5-0-1-2-lg-shuffled.qdimacs

Number of Unsolved Formulas (solved by no solver)

Number of Unsolved Formulas (solved by no solver)
formula
adder-12-unsat-shuffled.qdimacs
adder-8-unsat-shuffled.qdimacs
connect_7x6_4_R-shuffled.qdimacs
adder-14-sat-shuffled.qdimacs
blocks_enc_2_b4_ser--opt-26_-shuffled.qdimacs
C6288.blif_0.10_0.20_0_0_out_exact-shuffled.qdimacs
C5315.blif_0.10_0.20_0_0_inp_exact-shuffled.qdimacs
k_ph_p-12-shuffled.qdimacs
C5315.blif_0.10_0.20_0_0_out_exact-shuffled.qdimacs
adder-12-sat-shuffled.qdimacs
Adder2-10-s-shuffled.qdimacs
ev-pr-8x8-19-7-0-1-2-lg-shuffled.qdimacs
f600-00-shuffled.qdimacs
C5315.blif_0.10_0.20_0_1_inp_exact-shuffled.qdimacs
connect_9x8_3_R-shuffled.qdimacs
C6288.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimacs
cube_c7_ser---23_-shuffled.qdimacs
C5315.blif_0.10_0.20_0_1_out_exact-shuffled.qdimacs
ev-pr-6x6-15-5-0-1-2-lg-shuffled.qdimacs

FORMULA SOLVER

adder-10-sat-shuffled.qdimacs runAqme.sh

adder-10-unsat-shuffled.qdimacs squeezebf1.2-qube7.2.pl

adder-14-unsat-shuffled.qdimacs squeezebf1.2-qube7.2.pl

adder-16-unsat-shuffled.qdimacs squeezebf1.2-qube7.2.pl

adder-8-sat-shuffled.qdimacs runAqme.sh

biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-008-shuffled.qdimacs run_rareqs

biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-010-shuffled.qdimacs run_rareqs

biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-009-shuffled.qdimacs run_rareqs

c3_Debug_s3_f2_e2_v2-shuffled.qdimacs squeezebf1.2-qube7.2.pl

c4_Debug_s3_f1_e1_v3-shuffled.qdimacs squeezebf1.2-qube7.2.pl

c4_Debug_s3_f1_e2_v3-shuffled.qdimacs squeezebf1.2-qube7.2.pl

c4_Debug_s3_f2_e1_v3-shuffled.qdimacs squeezebf1.2-qube7.2.pl

connect_6x5_5_R-shuffled.qdimacs runAqme.sh

emptyroom_e4_ser--opt-44_-shuffled.qdimacs run_rareqs

ev-pr-8x8-13-7-0-1-2-lg-shuffled.qdimacs depqbf

k5_3_2-shuffled.qdimacs run_rareqs

k_branch_n-20-shuffled.qdimacs hiqqer3

ring_r6_ser--opt-17_-shuffled.qdimacs squeezebf1.2-qube7.2.pl

s3330_d10_u-shuffled.qdimacs squeezebf1.2-qube7.2.pl

Formulas only solved by one solver

Formulas only solved by one solver
FORMULA	SOLVER
adder-10-sat-shuffled.qdimacs	runAqme.sh
adder-10-unsat-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
adder-14-unsat-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
adder-16-unsat-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
adder-8-sat-shuffled.qdimacs	runAqme.sh
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-008-shuffled.qdimacs	run_rareqs
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-010-shuffled.qdimacs	run_rareqs
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-009-shuffled.qdimacs	run_rareqs
c3_Debug_s3_f2_e2_v2-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
c4_Debug_s3_f1_e1_v3-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
c4_Debug_s3_f1_e2_v3-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
c4_Debug_s3_f2_e1_v3-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
connect_6x5_5_R-shuffled.qdimacs	runAqme.sh
emptyroom_e4_ser--opt-44_-shuffled.qdimacs	run_rareqs
ev-pr-8x8-13-7-0-1-2-lg-shuffled.qdimacs	depqbf
k5_3_2-shuffled.qdimacs	run_rareqs
k_branch_n-20-shuffled.qdimacs	hiqqer3
ring_r6_ser--opt-17_-shuffled.qdimacs	squeezebf1.2-qube7.2.pl
s3330_d10_u-shuffled.qdimacs	squeezebf1.2-qube7.2.pl

bdepqbf 6366.91
depqbf 5380.308
runAqme.sh 4830.362
hiqqer3 4552.047
squeezebf1.2-qube7.2.pl 3183.3665
qube7.2 2951.7854
squeezebf1.2-qube3.0 2948.7737
StruQS 2454.427
ghostq-bq-cegar.sh 2252.1965
ghostq-cegar.sh 2137.5852
ghostq.sh 1909.5709
pre_dual_ooq.py 1134.5736
dual_ooq 1124.6182
ooq 755.1766
run_rareqs 187.10559
qcnf2z3 119.72602
SOTA Ranking

SOTA Ranking
bdepqbf	6366.91
depqbf	5380.308
runAqme.sh	4830.362
hiqqer3	4552.047
squeezebf1.2-qube7.2.pl	3183.3665
qube7.2	2951.7854
squeezebf1.2-qube3.0	2948.7737
StruQS	2454.427
ghostq-bq-cegar.sh	2252.1965
ghostq-cegar.sh	2137.5852
ghostq.sh	1909.5709
pre_dual_ooq.py	1134.5736
dual_ooq	1124.6182
ooq	755.1766
run_rareqs	187.10559
qcnf2z3	119.72602

Formulas with Discrepancies

FORMULA SAT UNSAT

c1_BMC_p2_k1024-shuffled.qdimacs 1 7

c1_BMC_p2_k128-shuffled.qdimacs 1 10

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimacs 2 13

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs 1 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs 1 1

ring_r6_ser---16_-shuffled.qdimacs 1 3

ring_r7_ser---19_-shuffled.qdimacs 1 1

Formulas with Discrepancies

Formulas with Discrepancies
FORMULA	SAT	UNSAT
c1_BMC_p2_k1024-shuffled.qdimacs	1	7
c1_BMC_p2_k128-shuffled.qdimacs	1	10
C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimacs	2	13
ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs	1	1
ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs	1	1
ring_r6_ser---16_-shuffled.qdimacs	1	3
ring_r7_ser---19_-shuffled.qdimacs	1	1

formula solver result

c1_BMC_p2_k1024-shuffled.qdimacs bdepqbf 20

c1_BMC_p2_k1024-shuffled.qdimacs depqbf 1

c1_BMC_p2_k1024-shuffled.qdimacs runAqme.sh 1

c1_BMC_p2_k1024-shuffled.qdimacs StruQS 1

c1_BMC_p2_k1024-shuffled.qdimacs hiqqer3 20

c1_BMC_p2_k1024-shuffled.qdimacs squeezebf1.2-qube3.0 1

c1_BMC_p2_k1024-shuffled.qdimacs squeezebf1.2-qube7.2.pl 10

c1_BMC_p2_k1024-shuffled.qdimacs qube7.2 20

c1_BMC_p2_k1024-shuffled.qdimacs ghostq-cegar.sh 1

c1_BMC_p2_k1024-shuffled.qdimacs ghostq-bq-cegar.sh 1

c1_BMC_p2_k1024-shuffled.qdimacs ghostq.sh 1

c1_BMC_p2_k1024-shuffled.qdimacs pre_dual_ooq.py 1

c1_BMC_p2_k1024-shuffled.qdimacs ooq 20

c1_BMC_p2_k1024-shuffled.qdimacs dual_ooq 20

c1_BMC_p2_k1024-shuffled.qdimacs run_rareqs 20

c1_BMC_p2_k1024-shuffled.qdimacs qcnf2z3 20

formula solver result

c1_BMC_p2_k128-shuffled.qdimacs bdepqbf 20

c1_BMC_p2_k128-shuffled.qdimacs depqbf 1

c1_BMC_p2_k128-shuffled.qdimacs StruQS 1

c1_BMC_p2_k128-shuffled.qdimacs runAqme.sh 20

c1_BMC_p2_k128-shuffled.qdimacs hiqqer3 20

c1_BMC_p2_k128-shuffled.qdimacs qube7.2 20

c1_BMC_p2_k128-shuffled.qdimacs squeezebf1.2-qube7.2.pl 10

c1_BMC_p2_k128-shuffled.qdimacs squeezebf1.2-qube3.0 1

c1_BMC_p2_k128-shuffled.qdimacs ghostq-bq-cegar.sh 20

c1_BMC_p2_k128-shuffled.qdimacs ghostq-cegar.sh 1

c1_BMC_p2_k128-shuffled.qdimacs ghostq.sh 1

c1_BMC_p2_k128-shuffled.qdimacs pre_dual_ooq.py 20

c1_BMC_p2_k128-shuffled.qdimacs ooq 20

c1_BMC_p2_k128-shuffled.qdimacs dual_ooq 20

c1_BMC_p2_k128-shuffled.qdimacs run_rareqs 20

c1_BMC_p2_k128-shuffled.qdimacs qcnf2z3 20

formula solver result

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac depqbf 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac bdepqbf 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac runAqme.sh 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac StruQS 1

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac hiqqer3 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac squeezebf1.2-qube7.2.pl 10

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac squeezebf1.2-qube3.0 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac qube7.2 10

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac ghostq-cegar.sh 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac ghostq-bq-cegar.sh 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac ghostq.sh 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac dual_ooq 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac pre_dual_ooq.py 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac ooq 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac run_rareqs 20

C5315.blif_0.10_1.00_0_0_inp_exact-shuffled.qdimac qcnf2z3 20

formula solver result

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs bdepqbf 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs depqbf 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs StruQS 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs runAqme.sh 20

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs hiqqer3 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs squeezebf1.2-qube3.0 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs qube7.2 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs squeezebf1.2-qube7.2.pl 10

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs ghostq.sh 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs ghostq-bq-cegar.sh 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs ghostq-cegar.sh 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs dual_ooq 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs ooq 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs pre_dual_ooq.py 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs run_rareqs 1

ev-pr-6x6-5-5-0-1-2-s-shuffled.qdimacs qcnf2z3 44

formula solver result

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs bdepqbf 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs depqbf 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs StruQS 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs runAqme.sh 20

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs hiqqer3 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs qube7.2 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs squeezebf1.2-qube3.0 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs squeezebf1.2-qube7.2.pl 10

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs ghostq-cegar.sh 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs ghostq.sh 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs ghostq-bq-cegar.sh 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs ooq 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs pre_dual_ooq.py 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs dual_ooq 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs run_rareqs 1

ev-pr-6x6-7-5-0-1-2-s-shuffled.qdimacs qcnf2z3 1

formula solver result

ring_r6_ser---16_-shuffled.qdimacs depqbf 1

ring_r6_ser---16_-shuffled.qdimacs bdepqbf 1

ring_r6_ser---16_-shuffled.qdimacs runAqme.sh 1

ring_r6_ser---16_-shuffled.qdimacs StruQS 1

ring_r6_ser---16_-shuffled.qdimacs hiqqer3 1

ring_r6_ser---16_-shuffled.qdimacs qube7.2 1

ring_r6_ser---16_-shuffled.qdimacs squeezebf1.2-qube7.2.pl 10

ring_r6_ser---16_-shuffled.qdimacs squeezebf1.2-qube3.0 1

ring_r6_ser---16_-shuffled.qdimacs ghostq-bq-cegar.sh 20

ring_r6_ser---16_-shuffled.qdimacs ghostq-cegar.sh 20

ring_r6_ser---16_-shuffled.qdimacs ghostq.sh 1

ring_r6_ser---16_-shuffled.qdimacs ooq 1

ring_r6_ser---16_-shuffled.qdimacs dual_ooq 1

ring_r6_ser---16_-shuffled.qdimacs pre_dual_ooq.py 1

ring_r6_ser---16_-shuffled.qdimacs run_rareqs 20

ring_r6_ser---16_-shuffled.qdimacs qcnf2z3 1

formula solver result

ring_r7_ser---19_-shuffled.qdimacs depqbf 1

ring_r7_ser---19_-shuffled.qdimacs bdepqbf 1

ring_r7_ser---19_-shuffled.qdimacs StruQS 1

ring_r7_ser---19_-shuffled.qdimacs runAqme.sh 1

ring_r7_ser---19_-shuffled.qdimacs hiqqer3 1

ring_r7_ser---19_-shuffled.qdimacs squeezebf1.2-qube3.0 1

ring_r7_ser---19_-shuffled.qdimacs squeezebf1.2-qube7.2.pl 10

ring_r7_ser---19_-shuffled.qdimacs qube7.2 1

ring_r7_ser---19_-shuffled.qdimacs ghostq-bq-cegar.sh 1

ring_r7_ser---19_-shuffled.qdimacs ghostq-cegar.sh 1

ring_r7_ser---19_-shuffled.qdimacs ghostq.sh 1

ring_r7_ser---19_-shuffled.qdimacs dual_ooq 1

ring_r7_ser---19_-shuffled.qdimacs pre_dual_ooq.py 1

ring_r7_ser---19_-shuffled.qdimacs ooq 1

ring_r7_ser---19_-shuffled.qdimacs qcnf2z3 1

ring_r7_ser---19_-shuffled.qdimacs run_rareqs 20

formula	solver	result
c1_BMC_p2_k1024-shuffled.qdimacs	bdepqbf	20
c1_BMC_p2_k1024-shuffled.qdimacs	depqbf	1
c1_BMC_p2_k1024-shuffled.qdimacs	runAqme.sh	1
c1_BMC_p2_k1024-shuffled.qdimacs	StruQS	1
c1_BMC_p2_k1024-shuffled.qdimacs	hiqqer3	20
c1_BMC_p2_k1024-shuffled.qdimacs	squeezebf1.2-qube3.0	1
c1_BMC_p2_k1024-shuffled.qdimacs	squeezebf1.2-qube7.2.pl	10
c1_BMC_p2_k1024-shuffled.qdimacs	qube7.2	20
c1_BMC_p2_k1024-shuffled.qdimacs	ghostq-cegar.sh	1
c1_BMC_p2_k1024-shuffled.qdimacs	ghostq-bq-cegar.sh	1
c1_BMC_p2_k1024-shuffled.qdimacs	ghostq.sh	1
c1_BMC_p2_k1024-shuffled.qdimacs	pre_dual_ooq.py	1
c1_BMC_p2_k1024-shuffled.qdimacs	ooq	20
c1_BMC_p2_k1024-shuffled.qdimacs	dual_ooq	20
c1_BMC_p2_k1024-shuffled.qdimacs	run_rareqs	20
c1_BMC_p2_k1024-shuffled.qdimacs	qcnf2z3	20