Name: |
mult_bool_matrix_3_5_5.aag |
md5: |
4c9422421a6c98fd255cd683587862c9 |
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 1542 55 0 1 1487
2
4
6
8
10
12
14
16
18
20
22
86
88
90
92
94
96
182
184
186
188
190
192
674
676
678
680
682
684
770
848
1270
1272
1274
1276
1278
1280
1366
1444
1866
1868
1870
1872
1874
1876
1962
2040
2462
2464
2466
2468
2470
2472
2558
2636
3085
24 23 1
26 11 1
28 20 27
30 29 1
32 9 31
34 9 33
36 18 35
38 19 31
40 37 39
42 7 41
44 7 43
46 16 45
48 17 41
50 47 49
52 3 51
54 3 53
56 12 55
58 13 51
60 57 59
62 12 55
64 13 51
66 63 65
68 22 61
70 23 66
72 69 71
74 4 25
76 5 73
78 75 77
80 14 79
82 15 73
84 8
... [truncated 19.8 kB]
<0>
i37 controllable_c[1][2]<0>
i38 controllable_c[2][2]<0>
i39 b[0][3]<0>
i40 b[1][3]<0>
i41 b[2][3]<0>
i42 b[3][3]<0>
i43 b[4][3]<0>
i44 controllable_c[0][3]<0>
i45 controllable_c[1][3]<0>
i46 controllable_c[2][3]<0>
i47 b[0][4]<0>
i48 b[1][4]<0>
i49 b[2][4]<0>
i50 b[3][4]<0>
i51 b[4][4]<0>
i52 controllable_c[0][4]<0>
i53 controllable_c[1][4]<0>
i54 controllable_c[2][4]<0>
o0 err<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 75.4152 [2015-pre-classification]
#.