Name: |
mult_bool_matrix_5_3_5.aag |
md5: |
2395251dc44d5460c9c0c6eb692e27a3 |
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 1071 55 0 1 1016
2
4
6
8
10
12
14
58
60
62
64
128
130
132
134
240
242
244
246
352
354
356
358
464
466
468
470
534
590
684
778
872
874
876
878
942
998
1092
1186
1280
1282
1284
1286
1350
1406
1500
1594
1688
1690
1692
1694
1758
1814
1908
2002
2143
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
... [truncated 13.5 kB]
47 b[0][4]<0>
i48 b[1][4]<0>
i49 b[2][4]<0>
i50 controllable_c[0][4]<0>
i51 controllable_c[1][4]<0>
i52 controllable_c[2][4]<0>
i53 controllable_c[3][4]<0>
i54 controllable_c[4][4]<0>
o0 err<0>
c
#!SYNTCOMP
SOLVED_BY : 2/3 [2015-pre-classification], 3/4 [SYNTCOMP2015-SyntSeq], 3/3 [SYNTCOMP2015-SyntPar], 6/7 [SYNTCOMP2015-RealSeq], 4/4 [SYNTCOMP2015-RealPar]
SOLVED_IN : 1032.24 [2015-pre-classification], 0.059117 [SYNTCOMP2015-RealSeq], 0.052852 [SYNTCOMP2015-RealPar]
REF_SIZE : 1166
STATUS : realizable
#.