Details of instance bs128y.aag

Name: bs128y.aag
md5: 5b8aabae57390132c15b0f59315eabbb
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 (45.9 kB)
aag 3337 8 129 1 3200
2
4
6
8
10
12
14
16
18 1
20 1299
22 2067
24 2451
26 2835
28 3027
30 3219
32 3411
34 3603
36 3699
38 3795
40 3891
42 3987
44 4083
46 4179
48 4275
50 4371
52 4419
54 4467
56 4515
58 4563
60 4611
62 4659
64 4707
66 4755
68 4803
70 4851
72 4899
74 4947
76 4995
78 5043
80 5091
82 5139
84 5163
86 5187
88 5211
90 5235
92 5259
94 5283
96 5307
98 5331
100 5355
102 5379
104 5403
106 5427
108 5451
110 5475
112 5499
114 5523
116 5547
118 5571
120 5595
122 5619
124 5643
126 5667
128 5691
130 5715
1

... [truncated 44.9 kB]

pos
  assign t3 = s[2] ? {t2[123:0],t2[127:124]} : t2; // shift by 4 pos
  assign t4 = s[3] ? {t3[119:0],t3[127:120]} : t3; // shift by 8 pos
  assign t5 = s[4] ? {t4[111:0],t4[127:112]} : t4; // shift by 16 pos
  assign t6 = s[5] ? {t5[95:0],t5[127:96]} : t5;   // shift by 32 pos
  assign o  = s[6] ? {t6[63:0],t6[127:64]} : t6;   // shift by 64 pos
endmodule

-------------------------------
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 0.096005 [SYNTCOMP2014-RealSeq]
#.