eval10

Overview

number of participating solvers: 12
number of participating formulas: 568

Overall Solving Statistics

SOLVER SAT UNSAT TOTAL

hiqqer3 221 238 459

pre_dual_ooq.py 190 227 417

ghost-bq-cegar.sh 195 214 409

dual_ooq 185 224 409

ghost-cegar.sh 191 209 400

depqbf-lazy-qup 171 224 395

depqbf 167 219 386

squeezebf1.2-qube3.0 161 210 371

ghost-plain.sh 172 173 345

ooq 99 165 264

rareqs-1.1 96 162 258

nenofex 106 114 220

Number of Solved Formulas

Number of Solved Formulas
SOLVER	SAT	UNSAT	TOTAL
hiqqer3	221	238	459
pre_dual_ooq.py	190	227	417
ghost-bq-cegar.sh	195	214	409
dual_ooq	185	224	409
ghost-cegar.sh	191	209	400
depqbf-lazy-qup	171	224	395
depqbf	167	219	386
squeezebf1.2-qube3.0	161	210	371
ghost-plain.sh	172	173	345
ooq	99	165	264
rareqs-1.1	96	162	258
nenofex	106	114	220

solver AVERAGE SUM

hiqqer3 223.12 126737.69

pre_dual_ooq.py 275.70 156599.65

dual_ooq 283.56 161065.59

ghost-bq-cegar.sh 289.68 164543.47

depqbf-lazy-qup 300.46 170663.72

ghost-cegar.sh 306.37 174019.93

depqbf 309.95 176051.64

squeezebf1.2-qube3.0 356.94 202747.59

ghost-plain.sh 382.35 217176.95

ooq 497.66 282671.54

rareqs-1.1 502.63 285498.93

nenofex 561.09 318701.25

Time Statistics (overall runtime, average runtime)

Time Statistics (overall runtime, average runtime)
solver	AVERAGE	SUM
hiqqer3	223.12	126737.69
pre_dual_ooq.py	275.70	156599.65
dual_ooq	283.56	161065.59
ghost-bq-cegar.sh	289.68	164543.47
depqbf-lazy-qup	300.46	170663.72
ghost-cegar.sh	306.37	174019.93
depqbf	309.95	176051.64
squeezebf1.2-qube3.0	356.94	202747.59
ghost-plain.sh	382.35	217176.95
ooq	497.66	282671.54
rareqs-1.1	502.63	285498.93
nenofex	561.09	318701.25

formula

C6288.blif_0.10_1.00_0_0_inp_exact

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

C6288.blif_0.10_0.20_0_0_out_exact

connect_6x5_5_R

connect_7x6_4_R

connect_9x8_3_R

c1_BMC_p1_k2048

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

s3330_d10_u

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

blocks_enc_2_b4_ser--opt-26_

f600-00

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

C5315.blif_0.10_0.20_0_0_inp_exact

C5315.blif_0.10_0.20_0_0_out_exact

k5_3_2

C5315.blif_0.10_0.20_0_1_inp_exact

c3_Debug_s3_f2_e2_v2

Adder2-10-s

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

c4_Debug_s3_f2_e1_v3

c2_Debug_s5_f1_e1_v3

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
C6288.blif_0.10_1.00_0_0_inp_exact
ev-pr-6x6-7-5-0-1-2-s
C6288.blif_0.10_0.20_0_0_out_exact
connect_6x5_5_R
connect_7x6_4_R
connect_9x8_3_R
c1_BMC_p1_k2048
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
s3330_d10_u
ev-pr-8x8-19-7-0-1-2-lg
blocks_enc_2_b4_ser--opt-26_
f600-00
ev-pr-6x6-5-5-0-1-2-s
C5315.blif_0.10_0.20_0_0_inp_exact
C5315.blif_0.10_0.20_0_0_out_exact
k5_3_2
C5315.blif_0.10_0.20_0_1_inp_exact
c3_Debug_s3_f2_e2_v2
Adder2-10-s
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
c4_Debug_s3_f2_e1_v3
c2_Debug_s5_f1_e1_v3
C5315.blif_0.10_0.20_0_1_out_exact
k_ph_p-12
k_branch_n-20

FORMULA SOLVER

adder-10-sat nenofex

adder-10-unsat nenofex

adder-12-sat nenofex

adder-12-unsat nenofex

adder-14-sat nenofex

adder-14-unsat nenofex

adder-16-unsat nenofex

adder-8-sat nenofex

adder-8-unsat nenofex

Adder2-6-s hiqqer3

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 squeezebf1.2-qube3.0

c4_Debug_s3_f1_e1_v3 nenofex

c4_Debug_s3_f1_e2_v3 nenofex

counter_32 hiqqer3

counter_e_8 nenofex

cube_c7_ser---23_ rareqs-1.1

emptyroom_e4_ser--opt-44_ rareqs-1.1

k_branch_p-11 hiqqer3

k_branch_p-14 hiqqer3

k_branch_p-17 hiqqer3

ring_r6_ser--opt-17_ rareqs-1.1

ring_r7_ser---19_ rareqs-1.1

Formulas only solved by one solver

Formulas only solved by one solver
FORMULA	SOLVER
adder-10-sat	nenofex
adder-10-unsat	nenofex
adder-12-sat	nenofex
adder-12-unsat	nenofex
adder-14-sat	nenofex
adder-14-unsat	nenofex
adder-16-unsat	nenofex
adder-8-sat	nenofex
adder-8-unsat	nenofex
Adder2-6-s	hiqqer3
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	squeezebf1.2-qube3.0
c4_Debug_s3_f1_e1_v3	nenofex
c4_Debug_s3_f1_e2_v3	nenofex
counter_32	hiqqer3
counter_e_8	nenofex
cube_c7_ser---23_	rareqs-1.1
emptyroom_e4_ser--opt-44_	rareqs-1.1
k_branch_p-11	hiqqer3
k_branch_p-14	hiqqer3
k_branch_p-17	hiqqer3
ring_r6_ser--opt-17_	rareqs-1.1
ring_r7_ser---19_	rareqs-1.1

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

Abduction (52) 50 50 50 50 50 50 51 49 41 51 50 50

Adder (15) 0 2 2 1 0 5 0 0 12 2 0 0

blackbox-01X-QBF (59) 52 35 43 41 35 43 37 53 11 46 46 54

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

Blocks (5) 2 5 5 5 5 4 4 4 5 5 5 5

BMC (18) 6 14 13 17 13 16 8 12 15 12 13 13

C432 (4) 1 4 2 4 4 2 4 2 2 2 2 2

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

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

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

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

Chain (1) 1 1 0 0 0 1 1 0 1 1 0 0

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

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

conformant_planning (15) 3 10 5 14 10 5 4 5 9 5 5 5

Connect4 (11) 8 8 8 7 8 8 8 8 5 8 8 8

Counter (4) 1 1 2 0 1 3 2 2 3 2 2 2

Debug (5) 0 0 0 0 0 0 0 0 2 0 0 0

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

evader-pursuer-4x4-standard (7) 7 0 0 0 0 5 0 0 0 6 0 0

evader-pursuer-6x6-logarithmic (4) 1 1 2 1 1 2 1 4 0 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 3 4 1 3 3 5 0 3 4 5

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

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

Impl (1) 1 1 1 0 1 1 1 1 1 1 1 1

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

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

k_branch_n (4) 1 3 2 0 2 3 3 1 1 2 1 1

k_branch_p (7) 1 4 1 0 2 7 3 1 1 1 1 1

k_d4_n (10) 0 10 0 0 10 10 10 0 0 0 0 0

k_d4_p (5) 1 5 5 0 5 5 5 1 3 5 5 2

k_dum_n (2) 0 2 0 0 2 2 2 0 2 1 0 0

k_dum_p (4) 2 4 4 0 4 4 4 1 4 4 4 1

k_grz_n (4) 2 4 3 0 4 4 4 3 4 3 3 4

k_grz_p (3) 2 3 2 0 3 3 3 2 3 3 2 3

k_lin_n (5) 5 4 5 1 4 5 5 5 3 5 5 5

k_lin_p (4) 4 4 4 4 4 4 4 4 4 4 4 4

k_path_n (3) 0 3 0 0 3 3 3 0 1 0 0 0

k_path_p (4) 0 4 0 0 4 4 4 0 3 1 0 0

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

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

k_poly_n (4) 4 4 0 0 4 4 4 0 2 4 0 0

k_poly_p (2) 2 2 2 0 2 2 2 0 1 2 2 0

k_t4p_n (4) 0 4 0 0 4 4 4 0 1 0 0 0

k_t4p_p (5) 1 5 1 0 5 5 5 1 1 1 1 1

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

mqm (136) 89 75 133 19 75 134 22 136 0 120 13 136

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

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

s27 (1) 1 1 1 0 1 1 1 0 1 1 0 0

s298 (4) 4 4 4 0 4 4 4 0 1 4 0 0

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

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

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

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

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

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

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

SzymanskiP (2) 2 1 2 1 0 2 0 0 0 2 1 0

term1 (3) 3 3 3 3 3 3 3 2 1 3 2 3

tipdiam (14) 13 14 6 3 14 7 14 3 1 11 3 3

tipfixpoint (24) 20 24 15 9 24 12 24 9 4 14 9 9

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

ToiletA (10) 10 10 10 10 10 10 10 10 10 10 10 10

ToiletC (23) 23 23 23 23 23 23 23 23 23 23 23 23

ToiletG (4) 4 4 4 4 4 4 4 4 4 4 4 4

VonNeumann (2) 2 2 2 2 1 2 1 2 2 2 2 2

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

total (568) 371 409 409 258 400 459 345 386 220 417 264 395

eval10

eval10
	sqube	bghostc	dooqm	rareqs	ghostc	hiqqer	ghost	depqbfm	nenofexm	sdooq	ooqm	ldepqbf
Abduction (52)	50	50	50	50	50	50	51	49	41	51	50	50
Adder (15)	0	2	2	1	0	5	0	0	12	2	0	0
blackbox-01X-QBF (59)	52	35	43	41	35	43	37	53	11	46	46	54
blackbox_design (2)	2	2	2	0	2	2	2	0	0	2	0	0
Blocks (5)	2	5	5	5	5	4	4	4	5	5	5	5
BMC (18)	6	14	13	17	13	16	8	12	15	12	13	13
C432 (4)	1	4	2	4	4	2	4	2	2	2	2	2
C499 (2)	1	2	1	2	2	1	2	1	2	1	1	1
C5315 (7)	2	3	2	3	3	2	2	2	3	2	2	2
C6288 (4)	1	0	0	0	0	0	2	0	0	2	0	0
C880 (1)	1	1	1	1	1	1	1	1	0	1	1	1
Chain (1)	1	1	0	0	0	1	1	0	1	1	0	0
circuits (3)	1	2	1	2	2	2	1	2	2	1	2	2
comp (2)	2	2	2	2	2	2	2	2	2	2	2	2
conformant_planning (15)	3	10	5	14	10	5	4	5	9	5	5	5
Connect4 (11)	8	8	8	7	8	8	8	8	5	8	8	8
Counter (4)	1	1	2	0	1	3	2	2	3	2	2	2
Debug (5)	0	0	0	0	0	0	0	0	2	0	0	0
evader-pursuer-4x4-logarithmic (3)	2	3	2	2	3	3	3	2	0	2	3	3
evader-pursuer-4x4-standard (7)	7	0	0	0	0	5	0	0	0	6	0	0
evader-pursuer-6x6-logarithmic (4)	1	1	2	1	1	2	1	4	0	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	3	4	1	3	3	5	0	3	4	5
FPGA_PLB_FIT_FAST (2)	1	2	2	2	2	2	2	2	2	2	2	2
FPGA_PLB_FIT_SLOW (1)	0	1	1	1	1	1	0	1	1	1	1	1
Impl (1)	1	1	1	0	1	1	1	1	1	1	1	1
jmc_quant (2)	2	0	0	0	0	2	0	0	1	2	0	0
jmc_quant_squaring (1)	1	0	0	0	0	1	0	0	0	1	0	0
k_branch_n (4)	1	3	2	0	2	3	3	1	1	2	1	1
k_branch_p (7)	1	4	1	0	2	7	3	1	1	1	1	1
k_d4_n (10)	0	10	0	0	10	10	10	0	0	0	0	0
k_d4_p (5)	1	5	5	0	5	5	5	1	3	5	5	2
k_dum_n (2)	0	2	0	0	2	2	2	0	2	1	0	0
k_dum_p (4)	2	4	4	0	4	4	4	1	4	4	4	1
k_grz_n (4)	2	4	3	0	4	4	4	3	4	3	3	4
k_grz_p (3)	2	3	2	0	3	3	3	2	3	3	2	3
k_lin_n (5)	5	4	5	1	4	5	5	5	3	5	5	5
k_lin_p (4)	4	4	4	4	4	4	4	4	4	4	4	4
k_path_n (3)	0	3	0	0	3	3	3	0	1	0	0	0
k_path_p (4)	0	4	0	0	4	4	4	0	3	1	0	0
k_ph_n (6)	6	6	6	6	6	6	6	6	5	6	6	6
k_ph_p (4)	2	3	2	2	3	2	3	2	2	2	2	2
k_poly_n (4)	4	4	0	0	4	4	4	0	2	4	0	0
k_poly_p (2)	2	2	2	0	2	2	2	0	1	2	2	0
k_t4p_n (4)	0	4	0	0	4	4	4	0	1	0	0	0
k_t4p_p (5)	1	5	1	0	5	5	5	1	1	1	1	1
Logn (1)	1	1	1	1	1	1	1	1	1	1	1	1
mqm (136)	89	75	133	19	75	134	22	136	0	120	13	136
s1196 (1)	0	1	0	0	1	0	1	0	0	0	0	0
s1269 (1)	0	1	1	0	1	1	1	0	0	1	0	0
s27 (1)	1	1	1	0	1	1	1	0	1	1	0	0
s298 (4)	4	4	4	0	4	4	4	0	1	4	0	0
s3330 (2)	0	1	1	0	1	0	1	0	0	0	0	0
s386 (1)	1	1	1	0	1	0	1	0	0	1	0	0
s499 (2)	2	2	2	0	2	1	2	0	0	1	0	0
s510 (3)	2	3	2	0	3	1	3	0	0	1	0	0
s713 (2)	2	2	2	0	2	2	2	0	0	2	0	0
s820 (2)	2	2	2	0	2	0	2	0	0	2	0	0
Sorting_networks (6)	2	4	3	6	4	3	5	6	6	2	3	6
SzymanskiP (2)	2	1	2	1	0	2	0	0	0	2	1	0
term1 (3)	3	3	3	3	3	3	3	2	1	3	2	3
tipdiam (14)	13	14	6	3	14	7	14	3	1	11	3	3
tipfixpoint (24)	20	24	15	9	24	12	24	9	4	14	9	9
Toilet (4)	2	4	3	4	4	3	4	4	4	3	3	4
ToiletA (10)	10	10	10	10	10	10	10	10	10	10	10	10
ToiletC (23)	23	23	23	23	23	23	23	23	23	23	23	23
ToiletG (4)	4	4	4	4	4	4	4	4	4	4	4	4
VonNeumann (2)	2	2	2	2	1	2	1	2	2	2	2	2
z4ml (1)	1	1	1	1	1	1	1	1	1	1	1	1
total (568)	371	409	409	258	400	459	345	386	220	417	264	395

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

Ansotegui (22) 13 5 7 7 5 13 7 11 0 12 10 12

Ayari (19) 4 5 6 4 1 9 1 2 14 6 3 2

Biere (42) 34 39 23 12 39 22 40 14 8 27 14 14

Castellini (37) 37 37 37 37 37 37 37 37 37 37 37 37

Gent-Rowley (11) 8 8 8 7 8 8 8 8 5 8 8 8

Herbstritt (61) 54 37 45 41 37 45 39 53 11 48 46 54

Katz (3) 3 0 0 0 0 3 0 0 1 3 0 0

Kontchakov (136) 89 75 133 19 75 134 22 136 0 120 13 136

Letombe (52) 50 50 50 50 50 50 51 49 41 51 50 50

Ling (3) 1 3 3 3 3 3 2 3 3 3 3 3

Mangassarian-Veneris (23) 6 14 13 17 13 16 8 12 17 12 13 13

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

Mneimneh-Sakallah (19) 14 18 16 0 18 10 18 0 2 13 0 0

Palacios (15) 3 10 5 14 10 5 4 5 9 5 5 5

Pan (80) 33 74 37 13 71 77 74 27 41 44 36 30

Rintanen (18) 9 16 13 16 15 13 16 16 18 13 13 17

Scholl-Becker (24) 12 16 12 16 16 12 17 11 11 14 11 12

total (568) 371 409 409 258 400 459 345 386 220 417 264 395

eval10

eval10
	sqube	bghostc	dooqm	rareqs	ghostc	hiqqer	ghost	depqbfm	nenofexm	sdooq	ooqm	ldepqbf
Ansotegui (22)	13	5	7	7	5	13	7	11	0	12	10	12
Ayari (19)	4	5	6	4	1	9	1	2	14	6	3	2
Biere (42)	34	39	23	12	39	22	40	14	8	27	14	14
Castellini (37)	37	37	37	37	37	37	37	37	37	37	37	37
Gent-Rowley (11)	8	8	8	7	8	8	8	8	5	8	8	8
Herbstritt (61)	54	37	45	41	37	45	39	53	11	48	46	54
Katz (3)	3	0	0	0	0	3	0	0	1	3	0	0
Kontchakov (136)	89	75	133	19	75	134	22	136	0	120	13	136
Letombe (52)	50	50	50	50	50	50	51	49	41	51	50	50
Ling (3)	1	3	3	3	3	3	2	3	3	3	3	3
Mangassarian-Veneris (23)	6	14	13	17	13	16	8	12	17	12	13	13
Messinger (3)	1	2	1	2	2	2	1	2	2	1	2	2
Mneimneh-Sakallah (19)	14	18	16	0	18	10	18	0	2	13	0	0
Palacios (15)	3	10	5	14	10	5	4	5	9	5	5	5
Pan (80)	33	74	37	13	71	77	74	27	41	44	36	30
Rintanen (18)	9	16	13	16	15	13	16	16	18	13	13	17
Scholl-Becker (24)	12	16	12	16	16	12	17	11	11	14	11	12
total (568)	371	409	409	258	400	459	345	386	220	417	264	395

Formulas with Discrepancies

FORMULA SAT UNSAT

Formulas with Discrepancies