Details of instance mult_bool_matrix_dyn_4_4.aag

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
Download instance (6.8 kB)
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]
#.