Details of instance genbuf20b3unrealy.aag

Name: genbuf20b3unrealy.aag
md5: 38672f4958a314e47cf1f2ac9ded4352
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 (106.5 kB)
aag 974 53 83 1 838
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
86
88
90
92
94
96
98
100
102
104
106
108 1
110 70
112 78
114 10
116 1752
118 1754
120 80
122 8
124 82
126 1756
128 1866
130 6
132 1868
134 24
136 84
138 1870
140 4
142 26
144 2
146 28
148 1872
150 52
152 1874
154 88
156 30
158 1876
160 1878
162 32
164 56
166 22
168 1880
170 34
172 1882
174 36
176 1884
178 38
180 1897
182 40
184 42
186 1898
188 1910
190 44
192 46
194 1

... [truncated 105.5 kB]

LC2 =  controllable_SLC2;
   reg_controllable_SLC3 =  controllable_SLC3;
   reg_controllable_SLC4 =  controllable_SLC4;

 end
endmodule

-------------------------------
#!SYNTCOMP
SOLVED_BY : 3/3 [2015-pre-classification], 3/4 [2017-pre-classification], 8/10 [SYNTCOMP2017-RealSeq], 5/6 [SYNTCOMP2017-RealPar], 5/6 [SYNTCOMP2017-SyntSeq], 3/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 6.95127 [2015-pre-classification], 6.384 [SYNTCOMP2017-RealSeq], 7.28648 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.