Name: |
mult_bool_matrix_dyn_5_5.aag |
md5: |
0cf0a1cf05e336e0a6dd41b0212981d0 |
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 1080 25 26 1 1029
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52 481
54 549
56 621
58 689
60 761
62 829
64 901
66 969
68 1041
70 1109
72 1181
74 1249
76 1321
78 1389
80 1461
82 1529
84 1601
86 1669
88 1741
90 1809
92 1881
94 1949
96 2021
98 2089
100 2161
102 154
409
104 53 1
106 55 1
108 57 1
110 59 1
112 61 1
114 63 1
116 65 1
118 67 1
120 69 1
122 71 1
124 73 1
126 75 1
128 77 1
130 79 1
132 81 1
134 83 1
136 85 1
138 87 1
140 89 1
142 91 1
144 93 1
146 95 1
148 97 1
150 99
... [truncated 13.1 kB]
atch<0>
o0 err<0>
c
#!SYNTCOMP
SOLVED_BY : 2/3 [2015-pre-classification], 2/4 [SYNTCOMP2015-SyntSeq], 3/3 [SYNTCOMP2015-SyntPar], 5/7 [SYNTCOMP2015-RealSeq], 4/4 [SYNTCOMP2015-RealPar], 6/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 10/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 137.917 [2015-pre-classification], 3.72517 [SYNTCOMP2015-RealSeq], 0.580359 [SYNTCOMP2015-RealPar], 0.988 [SYNTCOMP2016-RealSeq], 0.519966 [SYNTCOMP2016-RealPar]
REF_SIZE : 1044
STATUS : realizable
#.