eval10_bloqqer_pp

Overview

number of participating solvers: 12
number of participating formulas: 420

Overall Solving Statistics

SOLVER SAT UNSAT TOTAL

depqbf-lazy-qup 164 163 327

depqbf 166 158 324

hiqqer3 131 156 287

rareqs-1.1 117 133 250

squeezebf1.2-qube3.0 94 133 227

dual_ooq 96 105 201

ooq 97 99 196

pre_dual_ooq.py 97 97 194

ghost-cegar.sh 103 76 179

ghost-bq-cegar.sh 103 76 179

ghost-plain.sh 90 89 179

nenofex 73 50 123

Number of Solved Formulas

Number of Solved Formulas
SOLVER	SAT	UNSAT	TOTAL
depqbf-lazy-qup	164	163	327
depqbf	166	158	324
hiqqer3	131	156	287
rareqs-1.1	117	133	250
squeezebf1.2-qube3.0	94	133	227
dual_ooq	96	105	201
ooq	97	99	196
pre_dual_ooq.py	97	97	194
ghost-cegar.sh	103	76	179
ghost-bq-cegar.sh	103	76	179
ghost-plain.sh	90	89	179
nenofex	73	50	123

solver AVERAGE SUM

depqbf-lazy-qup 237.75 99858.84

depqbf 247.95 104139.69

hiqqer3 348.90 146538.12

rareqs-1.1 379.95 159583.06

squeezebf1.2-qube3.0 476.92 200310.39

dual_ooq 487.72 204843.44

ooq 492.57 206882.00

pre_dual_ooq.py 518.04 217579.20

ghost-cegar.sh 550.40 231168.87

ghost-bq-cegar.sh 550.45 231191.74

ghost-plain.sh 556.67 233802.22

nenofex 647.09 271777.97

Time Statistics (overall runtime, average runtime)

Time Statistics (overall runtime, average runtime)
solver	AVERAGE	SUM
depqbf-lazy-qup	237.75	99858.84
depqbf	247.95	104139.69
hiqqer3	348.90	146538.12
rareqs-1.1	379.95	159583.06
squeezebf1.2-qube3.0	476.92	200310.39
dual_ooq	487.72	204843.44
ooq	492.57	206882.00
pre_dual_ooq.py	518.04	217579.20
ghost-cegar.sh	550.40	231168.87
ghost-bq-cegar.sh	550.45	231191.74
ghost-plain.sh	556.67	233802.22
nenofex	647.09	271777.97

formula

cmu.periodic.N-f4

nusmv.tcas-t^6.B-f3

C6288.blif_0.10_1.00_0_0_inp_exact

eijk.S208o.S-f4

ev-pr-6x6-7-5-0-1-2-s

C6288.blif_0.10_0.20_0_0_out_exact

adder-8-unsat

connect_7x6_4_R

eijk.S382.S-f4

ring_r6_ser--opt-17_

adder-8-sat

connect_9x8_3_R

nusmv.reactor^1.C-d4

s3330_d10_u

ev-pr-8x8-19-7-0-1-2-lg

blocks_enc_2_b4_ser--opt-26_

ken.flash^14.C-d4

f600-00

vis.arbiter.E-f4

nusmv.tcas^4.B-f3

ev-pr-6x6-5-5-0-1-2-s

C5315.blif_0.10_0.20_0_0_inp_exact

cmu.dme1.B-f4

C5315.blif_0.10_0.20_0_0_out_exact

adder-10-sat

adder-14-sat

C5315.blif_0.10_0.20_0_1_inp_exact

nusmv.tcas^2.B-f2

c3_Debug_s3_f2_e2_v2

eijk.S526.S-f4

adder-12-sat

cube_c7_ser---23_

Adder2-10-s

k_ph_p-11

vis.prodcell^24.E-f3

vis.prodcell^23.E-f4

c2_Debug_s5_f1_e1_v3

nusmv.reactor^2.C-d4

C5315.blif_0.10_0.20_0_1_out_exact

k_ph_p-12

k_branch_n-20

Number of Unsolved Formulas (solved by no solver)

Number of Unsolved Formulas (solved by no solver)
formula
cmu.periodic.N-f4
nusmv.tcas-t^6.B-f3
C6288.blif_0.10_1.00_0_0_inp_exact
eijk.S208o.S-f4
ev-pr-6x6-7-5-0-1-2-s
C6288.blif_0.10_0.20_0_0_out_exact
adder-8-unsat
connect_7x6_4_R
eijk.S382.S-f4
ring_r6_ser--opt-17_
adder-8-sat
connect_9x8_3_R
nusmv.reactor^1.C-d4
s3330_d10_u
ev-pr-8x8-19-7-0-1-2-lg
blocks_enc_2_b4_ser--opt-26_
ken.flash^14.C-d4
f600-00
vis.arbiter.E-f4
nusmv.tcas^4.B-f3
ev-pr-6x6-5-5-0-1-2-s
C5315.blif_0.10_0.20_0_0_inp_exact
cmu.dme1.B-f4
C5315.blif_0.10_0.20_0_0_out_exact
adder-10-sat
adder-14-sat
C5315.blif_0.10_0.20_0_1_inp_exact
nusmv.tcas^2.B-f2
c3_Debug_s3_f2_e2_v2
eijk.S526.S-f4
adder-12-sat
cube_c7_ser---23_
Adder2-10-s
k_ph_p-11
vis.prodcell^24.E-f3
vis.prodcell^23.E-f4
c2_Debug_s5_f1_e1_v3
nusmv.reactor^2.C-d4
C5315.blif_0.10_0.20_0_1_out_exact
k_ph_p-12
k_branch_n-20

FORMULA SOLVER

adder-10-unsat nenofex

adder-12-unsat nenofex

adder-14-unsat nenofex

adder-16-unsat nenofex

biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-008 rareqs-1.1

biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-007 rareqs-1.1

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 rareqs-1.1

biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-009 rareqs-1.1

biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-010 rareqs-1.1

biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-008 rareqs-1.1

c1_BMC_p1_k2048 rareqs-1.1

c4_Debug_s3_f1_e1_v3 nenofex

c4_Debug_s3_f1_e2_v3 nenofex

c4_Debug_s3_f2_e1_v3 nenofex

C6288.blif_0.10_1.00_0_1_inp_exact rareqs-1.1

C6288.blif_0.10_1.00_0_1_out_exact rareqs-1.1

connect_6x5_5_R squeezebf1.2-qube3.0

eijk.S1423.S-d4 hiqqer3

emptyroom_e3_ser---19_ rareqs-1.1

emptyroom_e4_ser--opt-44_ rareqs-1.1

nusmv.queue.B-d4 hiqqer3

ring_r7_ser---19_ rareqs-1.1

Formulas only solved by one solver

Formulas only solved by one solver
FORMULA	SOLVER
adder-10-unsat	nenofex
adder-12-unsat	nenofex
adder-14-unsat	nenofex
adder-16-unsat	nenofex
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-008	rareqs-1.1
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-007	rareqs-1.1
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	rareqs-1.1
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-009	rareqs-1.1
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-010	rareqs-1.1
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-008	rareqs-1.1
c1_BMC_p1_k2048	rareqs-1.1
c4_Debug_s3_f1_e1_v3	nenofex
c4_Debug_s3_f1_e2_v3	nenofex
c4_Debug_s3_f2_e1_v3	nenofex
C6288.blif_0.10_1.00_0_1_inp_exact	rareqs-1.1
C6288.blif_0.10_1.00_0_1_out_exact	rareqs-1.1
connect_6x5_5_R	squeezebf1.2-qube3.0
eijk.S1423.S-d4	hiqqer3
emptyroom_e3_ser---19_	rareqs-1.1
emptyroom_e4_ser--opt-44_	rareqs-1.1
nusmv.queue.B-d4	hiqqer3
ring_r7_ser---19_	rareqs-1.1

sqube bghostc dooqm rareqs ghostc hiqqer ghost depqbfm nenofexm sdooq ooqm ldepqbf

Abduction (29) 27 26 27 28 26 25 27 26 9 27 26 26

Adder (13) 1 1 1 2 1 2 1 1 6 1 1 2

blackbox-01X-QBF (48) 35 10 36 48 10 37 11 33 1 34 36 35

blackbox_design (2) 2 0 2 2 0 2 0 2 0 2 2 2

Blocks (3) 1 3 3 3 3 3 2 3 3 3 3 2

BMC (12) 2 9 10 12 9 10 7 10 11 9 10 9

C432 (4) 2 4 2 4 4 2 3 3 4 2 2 4

C499 (2) 1 2 2 2 2 2 2 2 2 2 2 2

C5315 (7) 2 3 2 3 3 2 2 2 3 2 2 2

C6288 (4) 0 0 0 2 0 0 0 0 0 0 0 0

C880 (1) 0 1 1 1 1 1 1 1 0 1 1 1

circuits (3) 1 2 2 3 2 2 1 2 3 2 2 2

comp (2) 2 2 2 2 2 2 2 2 2 2 2 2

conformant_planning (14) 2 7 4 11 7 4 5 4 7 4 4 4

Connect4 (4) 2 1 1 0 1 1 1 1 0 1 1 1

Counter (3) 1 1 2 3 1 2 2 2 3 2 2 2

Debug (5) 0 0 0 0 0 0 0 0 3 0 0 0

evader-pursuer-4x4-logarithmic (3) 2 3 2 3 3 3 3 2 1 2 2 2

evader-pursuer-4x4-standard (7) 7 7 2 7 7 6 7 6 0 2 1 6

evader-pursuer-6x6-logarithmic (4) 1 1 1 2 1 2 1 4 1 1 3 4

evader-pursuer-6x6-standard (2) 0 0 0 0 0 0 0 0 0 0 0 0

evader-pursuer-8x8-logarithmic (6) 3 1 2 4 1 3 3 5 1 2 5 5

FPGA_PLB_FIT_FAST (2) 2 2 2 2 2 2 2 2 2 2 2 2

FPGA_PLB_FIT_SLOW (1) 1 1 1 1 1 1 1 1 1 1 1 1

jmc_quant (2) 2 1 2 1 1 2 2 2 1 2 2 2

jmc_quant_squaring (1) 1 0 0 0 0 1 0 1 0 0 0 1

k_branch_n (1) 0 0 0 0 0 0 0 0 0 0 0 0

k_branch_p (3) 3 0 0 2 0 3 1 2 0 0 0 2

k_lin_n (1) 1 1 1 1 1 1 1 1 1 1 1 1

k_ph_n (6) 6 6 6 6 6 6 6 6 6 6 6 6

k_ph_p (4) 2 2 2 2 2 2 2 2 2 2 2 2

Logn (1) 1 1 1 1 1 1 1 1 1 1 1 1

mqm (136) 57 23 25 26 23 101 32 136 1 19 14 136

s1196 (1) 0 0 1 1 0 0 0 0 0 1 0 0

s1269 (1) 1 1 1 1 1 1 1 0 0 1 1 0

s298 (3) 3 3 3 3 3 2 2 3 2 3 3 3

s3330 (2) 0 0 1 1 0 1 0 0 0 1 1 0

s386 (1) 1 0 1 1 0 0 0 1 0 1 1 1

s499 (2) 2 2 2 2 2 1 1 2 2 2 2 2

s510 (3) 2 2 3 2 2 1 1 2 1 3 2 2

s713 (2) 2 2 2 2 2 2 1 2 0 2 2 2

s820 (2) 2 1 2 2 1 0 0 2 0 2 2 2

Sorting_networks (6) 2 5 2 6 5 2 2 3 6 2 2 3

term1 (3) 3 3 3 3 3 3 3 3 3 3 3 3

tipdiam (11) 5 5 3 6 5 7 5 5 1 4 6 6

tipfixpoint (15) 4 2 3 4 2 4 2 4 1 3 3 4

Toilet (4) 2 4 2 4 4 4 4 4 4 3 4 4

ToiletA (7) 7 7 7 7 7 7 7 7 7 7 7 7

ToiletC (20) 20 20 20 20 20 20 20 20 20 20 20 20

z4ml (1) 1 1 1 1 1 1 1 1 1 1 1 1

total (420) 227 179 201 250 179 287 179 324 123 194 196 327

eval10_bloqqer_pp

eval10_bloqqer_pp
	sqube	bghostc	dooqm	rareqs	ghostc	hiqqer	ghost	depqbfm	nenofexm	sdooq	ooqm	ldepqbf
Abduction (29)	27	26	27	28	26	25	27	26	9	27	26	26
Adder (13)	1	1	1	2	1	2	1	1	6	1	1	2
blackbox-01X-QBF (48)	35	10	36	48	10	37	11	33	1	34	36	35
blackbox_design (2)	2	0	2	2	0	2	0	2	0	2	2	2
Blocks (3)	1	3	3	3	3	3	2	3	3	3	3	2
BMC (12)	2	9	10	12	9	10	7	10	11	9	10	9
C432 (4)	2	4	2	4	4	2	3	3	4	2	2	4
C499 (2)	1	2	2	2	2	2	2	2	2	2	2	2
C5315 (7)	2	3	2	3	3	2	2	2	3	2	2	2
C6288 (4)	0	0	0	2	0	0	0	0	0	0	0	0
C880 (1)	0	1	1	1	1	1	1	1	0	1	1	1
circuits (3)	1	2	2	3	2	2	1	2	3	2	2	2
comp (2)	2	2	2	2	2	2	2	2	2	2	2	2
conformant_planning (14)	2	7	4	11	7	4	5	4	7	4	4	4
Connect4 (4)	2	1	1	0	1	1	1	1	0	1	1	1
Counter (3)	1	1	2	3	1	2	2	2	3	2	2	2
Debug (5)	0	0	0	0	0	0	0	0	3	0	0	0
evader-pursuer-4x4-logarithmic (3)	2	3	2	3	3	3	3	2	1	2	2	2
evader-pursuer-4x4-standard (7)	7	7	2	7	7	6	7	6	0	2	1	6
evader-pursuer-6x6-logarithmic (4)	1	1	1	2	1	2	1	4	1	1	3	4
evader-pursuer-6x6-standard (2)	0	0	0	0	0	0	0	0	0	0	0	0
evader-pursuer-8x8-logarithmic (6)	3	1	2	4	1	3	3	5	1	2	5	5
FPGA_PLB_FIT_FAST (2)	2	2	2	2	2	2	2	2	2	2	2	2
FPGA_PLB_FIT_SLOW (1)	1	1	1	1	1	1	1	1	1	1	1	1
jmc_quant (2)	2	1	2	1	1	2	2	2	1	2	2	2
jmc_quant_squaring (1)	1	0	0	0	0	1	0	1	0	0	0	1
k_branch_n (1)	0	0	0	0	0	0	0	0	0	0	0	0
k_branch_p (3)	3	0	0	2	0	3	1	2	0	0	0	2
k_lin_n (1)	1	1	1	1	1	1	1	1	1	1	1	1
k_ph_n (6)	6	6	6	6	6	6	6	6	6	6	6	6
k_ph_p (4)	2	2	2	2	2	2	2	2	2	2	2	2
Logn (1)	1	1	1	1	1	1	1	1	1	1	1	1
mqm (136)	57	23	25	26	23	101	32	136	1	19	14	136
s1196 (1)	0	0	1	1	0	0	0	0	0	1	0	0
s1269 (1)	1	1	1	1	1	1	1	0	0	1	1	0
s298 (3)	3	3	3	3	3	2	2	3	2	3	3	3
s3330 (2)	0	0	1	1	0	1	0	0	0	1	1	0
s386 (1)	1	0	1	1	0	0	0	1	0	1	1	1
s499 (2)	2	2	2	2	2	1	1	2	2	2	2	2
s510 (3)	2	2	3	2	2	1	1	2	1	3	2	2
s713 (2)	2	2	2	2	2	2	1	2	0	2	2	2
s820 (2)	2	1	2	2	1	0	0	2	0	2	2	2
Sorting_networks (6)	2	5	2	6	5	2	2	3	6	2	2	3
term1 (3)	3	3	3	3	3	3	3	3	3	3	3	3
tipdiam (11)	5	5	3	6	5	7	5	5	1	4	6	6
tipfixpoint (15)	4	2	3	4	2	4	2	4	1	3	3	4
Toilet (4)	2	4	2	4	4	4	4	4	4	3	4	4
ToiletA (7)	7	7	7	7	7	7	7	7	7	7	7	7
ToiletC (20)	20	20	20	20	20	20	20	20	20	20	20	20
z4ml (1)	1	1	1	1	1	1	1	1	1	1	1	1
total (420)	227	179	201	250	179	287	179	324	123	194	196	327

sqube bghostc dooqm rareqs ghostc hiqqer ghost depqbfm nenofexm sdooq ooqm ldepqbf

Ansotegui (22) 13 12 7 16 12 14 14 17 3 7 11 17

Ayari (13) 1 1 1 2 1 2 1 1 6 1 1 2

Biere (29) 10 8 8 13 8 13 9 11 5 9 11 12

Castellini (27) 27 27 27 27 27 27 27 27 27 27 27 27

Gent-Rowley (4) 2 1 1 0 1 1 1 1 0 1 1 1

Herbstritt (50) 37 10 38 50 10 39 11 35 1 36 38 37

Katz (3) 3 1 2 1 1 3 2 3 1 2 2 3

Kontchakov (136) 57 23 25 26 23 101 32 136 1 19 14 136

Letombe (29) 27 26 27 28 26 25 27 26 9 27 26 26

Ling (3) 3 3 3 3 3 3 3 3 3 3 3 3

Mangassarian-Veneris (17) 2 9 10 12 9 10 7 10 14 9 10 9

Messinger (3) 1 2 2 3 2 2 1 2 3 2 2 2

Mneimneh-Sakallah (17) 13 11 16 15 11 8 6 12 5 16 14 12

Palacios (14) 2 7 4 11 7 4 5 4 7 4 4 4

Pan (15) 12 9 9 11 9 12 10 11 9 9 9 11

Rintanen (14) 6 13 8 14 13 10 9 11 14 9 10 10

Scholl-Becker (24) 11 16 13 18 16 13 14 14 15 13 13 15

total (420) 227 179 201 250 179 287 179 324 123 194 196 327

eval10_bloqqer_pp

eval10_bloqqer_pp
	sqube	bghostc	dooqm	rareqs	ghostc	hiqqer	ghost	depqbfm	nenofexm	sdooq	ooqm	ldepqbf
Ansotegui (22)	13	12	7	16	12	14	14	17	3	7	11	17
Ayari (13)	1	1	1	2	1	2	1	1	6	1	1	2
Biere (29)	10	8	8	13	8	13	9	11	5	9	11	12
Castellini (27)	27	27	27	27	27	27	27	27	27	27	27	27
Gent-Rowley (4)	2	1	1	0	1	1	1	1	0	1	1	1
Herbstritt (50)	37	10	38	50	10	39	11	35	1	36	38	37
Katz (3)	3	1	2	1	1	3	2	3	1	2	2	3
Kontchakov (136)	57	23	25	26	23	101	32	136	1	19	14	136
Letombe (29)	27	26	27	28	26	25	27	26	9	27	26	26
Ling (3)	3	3	3	3	3	3	3	3	3	3	3	3
Mangassarian-Veneris (17)	2	9	10	12	9	10	7	10	14	9	10	9
Messinger (3)	1	2	2	3	2	2	1	2	3	2	2	2
Mneimneh-Sakallah (17)	13	11	16	15	11	8	6	12	5	16	14	12
Palacios (14)	2	7	4	11	7	4	5	4	7	4	4	4
Pan (15)	12	9	9	11	9	12	10	11	9	9	9	11
Rintanen (14)	6	13	8	14	13	10	9	11	14	9	10	10
Scholl-Becker (24)	11	16	13	18	16	13	14	14	15	13	13	15
total (420)	227	179	201	250	179	287	179	324	123	194	196	327

Formulas with Discrepancies

FORMULA SAT UNSAT

Formulas with Discrepancies