Details of instance stay20n.aag

Name: stay20n.aag
md5: e86dc4134611cf47cb7f8512ebd7c34f
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 (42.7 kB)
aag 2851 41 22 1 2788
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
54
56
58
60
62
64
66
68
70
72
74
76
78
80
82
84 1
86 303
88 5551
90 5559
92 5567
94 5575
96 5583
98 5591
100 5599
102 5607
104 5615
106 5623
108 5631
110 5639
112 5647
114 5655
116 5663
118 5671
120 5679
122 5687
124 5695
126 5703
292
128 87 84
130 86 84
132 129 84
134 89 84
136 88 84
138 135 84
140 91 84
142 90 84
144 141 84
146 93 84
148 92 84
150 147 84
152 95 84
154 94 84
156 153 84
158 97 84
160 96 84
162 15

... [truncated 41.7 kB]

4:0],15'b000000000000000} : 0;
  assign s16 = b[16] ? {a[3:0],16'b0000000000000000} : 0;
  assign s17 = b[17] ? {a[2:0],17'b00000000000000000} : 0;
  assign s18 = b[18] ? {a[1:0],18'b000000000000000000} : 0;
  assign s19 = b[19] ? {a[0:0],19'b0000000000000000000} : 0;
  assign r  = s0+s1+s2+s3+s4+s5+s6+s7+s8+s9+s10+s11+s12+s13+s14+s15+s16+s17+s18+s19;
endmodule
-------------------------------
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 1/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 5.08432 [SYNTCOMP2014-RealSeq]
#.