Name: |
mult_bool_matrix_4_3_3.aag |
md5: |
fbf2ccb69ca75709f6e5335ec697c50f |
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 500 33 0 1 467
2
4
6
8
10
12
14
58
60
62
64
128
130
132
134
240
242
244
246
352
354
356
358
422
478
572
666
668
670
672
736
792
886
1001
16 15 1
18 7 1
20 12 19
22 21 1
24 3 23
26 3 25
28 8 27
30 9 23
32 29 31
34 8 27
36 9 23
38 35 37
40 14 33
42 15 38
44 41 43
46 4 17
48 5 45
50 47 49
52 10 51
54 11 45
56 53 55
66 65 1
68 63 1
70 12 69
72 71 1
74 59 73
76 59 75
78 59 73
80 59 79
82 64 77
84 65 80
86 83 85
88 60 67
90 61 87
92 89 91
94 12 69
96 95 1
98 64 73
100 65 96
102 99 101
104 60 67
106 61 103
108
... [truncated 5.1 kB]
]<0>
i16 a[3][1]<0>
i17 a[3][2]<0>
i18 controllable_c[3][0]<0>
i19 b[0][1]<0>
i20 b[1][1]<0>
i21 b[2][1]<0>
i22 controllable_c[0][1]<0>
i23 controllable_c[1][1]<0>
i24 controllable_c[2][1]<0>
i25 controllable_c[3][1]<0>
i26 b[0][2]<0>
i27 b[1][2]<0>
i28 b[2][2]<0>
i29 controllable_c[0][2]<0>
i30 controllable_c[1][2]<0>
i31 controllable_c[2][2]<0>
i32 controllable_c[3][2]<0>
o0 err<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 0.302377 [2015-pre-classification]
#.