heretiq results solving families

heretiq results solving families - 2017

Family	# Total	# Sat	# Unsat	Time
Abduction	26	0	0	23400
Adder	114	0	2	86416.82
amba	22	1	1	9124.69
arithmetic	22	4	0	4500.22
blackbox-01X-QBF	133	0	13	40811.14
BMC	98	4	2	40980.99
C432	21	0	2	49.98
C499	31	0	0	27900
C5315	57	0	1	40522.92
C6288	76	0	0	68400
C880	60	0	2	42889.75
circuits	84	2	0	72070.36
conformant_planning	60	0	5	25940.48
Connect2	1	1	0	13.76
Connect3	2	0	0	1800
Connect4	43	0	1	37800.06
Connect5	2	0	1	900.64
Connect6	3	0	1	1800.06
Connect7	4	0	0	3600
Connect8	2	0	2	0.5
Counter	22	2	0	14283.19
cycle-sched	24	2	0	14847.66
Debug	125	2	0	109589.88
disjunctive_decomposition	23	3	0	7200.85
driver	18	2	2	2
dungeon	115	1	6	87863.04
evader-pursuer-4x4-logarithmic	10	1	0	83.8
evader-pursuer-4x4-standard	65	4	0	26450.94
evader-pursuer-6x6-logarithmic	50	0	2	34220.44
evader-pursuer-6x6-standard	77	0	0	69300
evader-pursuer-8x8-logarithmic	51	0	2	39753
formula_add	39	4	0	26780.83
fpu	20	0	20	23.63
genbuf	22	0	0	19800
Generalized-Tic-Tac-Toe	32	1	5	8249.9
genpatch	20	1	1	12191.48
HardwareFixpoint	125	2	3	97254.05
hwmcc	16	0	2	10824.32
hyperLTL	4	1	1	0.02
incrementer-encoder	55	2	11	245.31
irqlkeapclte	121	0	0	108900
ISCAS89	7	2	2	10.7
ITC99	57	2	1	43721.91
jmc_quant	6	0	0	5400
jmc_quant_squaring	98	1	0	77053.15
k_branch_n	56	3	0	22199.19
k_branch_p	85	0	6	14478.08
k_ph_p	80	0	0	72000
LinearBitvectorRankingFunction	119	1	3	83428.27
ltl2aig-comp	19	0	2	5611.65
LTL2DBA	9	1	1	1.69
LTL2DPA	10	1	1	9.86
mqm	34	3	0	17771.39
mult-matrix	24	1	0	15301.82
Planning-CTE	131	2	27	25125.09
QBF-Hardness	60	0	4	37044.52
qbfeval12	7	2	0	2900.26
RankingFunctions	2	2	0	0.13
Reduction-finding	45	0	2	31943.51
s1196	15	0	0	13500
s1269	17	0	0	15300
s298	14	1	0	6592.39
s3330	21	0	0	18900
s499	13	0	0	11700
s510	9	0	0	8100
s641	16	1	1	3447.92
s713	15	0	1	11229.03
s820	15	0	0	13500
sketch	16	0	0	14400
Sorting_networks	81	2	4	5948.48
SzymanskiP	25	0	2	1098.52
terminator	78	0	8	10032.85
tipdiam	85	0	0	76500
tipfixpoint	93	0	0	83700
toy	14	2	2	2065.54
trafficlight-controller	10	0	10	19.83
uclid	30	0	0	27000

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

heretiq results solving families - 2017