Details of instance mult_bool_matrix_dyn_5_5.aag

Name: mult_bool_matrix_dyn_5_5.aag
md5: f606d4d58abdbb0fce83a56268b5546a
FractionOfBinaryClauses None
FractionOfNegativeLiteralsPerClauseEntropy None
FractionOfNegativeLiteralsPerClauseMax None
FractionOfNegativeLiteralsPerClauseMean None
FractionOfNegativeLiteralsPerClauseMin None
FractionOfNegativeLiteralsPerClauseVariationCoefficient None
FractionOfNegativeVariablesEntropy None
FractionOfNegativeVariablesMax None
FractionOfNegativeVariablesMean None
FractionOfNegativeVariablesMin None
FractionOfNegativeVariablesVariationCoefficient None
FractionOfPositiveLiteralsPerClauseEntropy None
FractionOfPositiveLiteralsPerClauseMax None
FractionOfPositiveLiteralsPerClauseMean None
FractionOfPositiveLiteralsPerClauseMin None
FractionOfPositiveLiteralsPerClauseVariationCoefficient None
FractionOfPositiveVariablesEntropy None
FractionOfPositiveVariablesMax None
FractionOfPositiveVariablesMean None
FractionOfPositiveVariablesMin None
FractionOfPositiveVariablesVariationCoefficient None
FractionOfTernaryClauses None
FractionOfUnaryClauses None
ClausesToVariablesRatio None
ClausesToVariablesRatioCubic None
ClausesToVariablesRatioQuadratic None
LinearizedClausesToVariablesRatio None
LinearizedClausesToVariablesRatioQuadratic None
LinearizedClaustesToVariablesRatioCubic None
NumberOfClauses None
NumberOfVariables None
VariablesToClausesRatio None
VariablesToClausesRatioCubic None
VariablesToClausesRatioQuadratic None
ClauseNodeDegreesEntropy None
ClauseNodeDegreesMax None
ClauseNodeDegreesMean None
ClauseNodeDegreesMin None
ClauseNodeDegreesVariationCoefficient None
VariableNodeDegreesEntropy None
VariableNodeDegreesMax None
VariableNodeDegreesMean None
VariableNodeDegreesMin None
VariableNodeDegreesVariationCoefficient None
DegreeEntropy None
DegreeMax None
DegreeMean None
DegreeMin None
DegreeVariationCoefficient None
Download instance (13.8 kB)
aag 1080 25 26 1 1029
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52 481
54 549
56 621
58 689
60 761
62 829
64 901
66 969
68 1041
70 1109
72 1181
74 1249
76 1321
78 1389
80 1461
82 1529
84 1601
86 1669
88 1741
90 1809
92 1881
94 1949
96 2021
98 2089
100 2161
102 154
409
104 53 1
106 55 1
108 57 1
110 59 1
112 61 1
114 63 1
116 65 1
118 67 1
120 69 1
122 71 1
124 73 1
126 75 1
128 77 1
130 79 1
132 81 1
134 83 1
136 85 1
138 87 1
140 89 1
142 91 1
144 93 1
146 95 1
148 97 1
150 99 

... [truncated 12.8 kB]

0][0]<0>
l1 a[0][1]<0>
l2 a[0][2]<0>
l3 a[0][3]<0>
l4 a[0][4]<0>
l5 a[1][0]<0>
l6 a[1][1]<0>
l7 a[1][2]<0>
l8 a[1][3]<0>
l9 a[1][4]<0>
l10 a[2][0]<0>
l11 a[2][1]<0>
l12 a[2][2]<0>
l13 a[2][3]<0>
l14 a[2][4]<0>
l15 a[3][0]<0>
l16 a[3][1]<0>
l17 a[3][2]<0>
l18 a[3][3]<0>
l19 a[3][4]<0>
l20 a[4][0]<0>
l21 a[4][1]<0>
l22 a[4][2]<0>
l23 a[4][3]<0>
l24 a[4][4]<0>
l25 init_latch<0>
o0 err<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 137.917 [2015-pre-classification]
#.