Name: |
mult_bool_matrix_dyn_4_4.aag |
md5: |
aaaeb2efa8a798c2089ebd7b914ec14a |
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 |
aag 583 16 17 1 550
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34 329
36 383
38 441
40 495
42 549
44 607
46 661
48 719
50 777
52 831
54 889
56 943
58 997
60 1055
62 1109
64 1167
66 100
271
68 35 1
70 37 1
72 39 1
74 41 1
76 43 1
78 45 1
80 47 1
82 49 1
84 51 1
86 53 1
88 55 1
90 57 1
92 59 1
94 61 1
96 63 1
98 65 1
100 1 1
102 68 1
104 71 103
106 105 1
108 73 107
110 109 1
112 75 111
114 113 1
116 66 115
118 117 1
120 68 1
122 71 121
124 123 1
126 73 125
128 127 1
130 75 129
132 131 1
134 66 133
136 135 1
... [truncated 5.8 kB]
lable_c[0][3]<0>
i12 controllable_c[1][0]<0>
i13 controllable_c[1][1]<0>
i14 controllable_c[1][2]<0>
i15 controllable_c[1][3]<0>
l0 a[0][0]<0>
l1 a[0][1]<0>
l2 a[0][2]<0>
l3 a[0][3]<0>
l4 a[1][0]<0>
l5 a[1][1]<0>
l6 a[1][2]<0>
l7 a[1][3]<0>
l8 a[2][0]<0>
l9 a[2][1]<0>
l10 a[2][2]<0>
l11 a[2][3]<0>
l12 a[3][0]<0>
l13 a[3][1]<0>
l14 a[3][2]<0>
l15 a[3][3]<0>
l16 init_latch<0>
o0 err<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 0.147624 [2015-pre-classification]
#.