Details of instance driver_d10y.aag

Name: driver_d10y.aag
md5: 57e8b649a3b90a7c85926ec3ec3518ab
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 (23.9 kB)
aag 538 40 56 1 442
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 1
84 231
86 239
88 247
90 259
92 267
94 281
96 289
98 297
100 305
102 313
104 321
106 329
108 337
110 407
112 419
114 426
116 441
118 449
120 457
122 465
124 473
126 481
128 497
130 507
132 517
134 12
136 8
138 633
140 645
142 651
144 657
146 663
148 923
150 943
152 953
154 961
156 967
158 973
160 979
162 985
164 991
166 10
168 994
170 1002
172 1010
174 1018
176 1029
178

... [truncated 22.9 kB]

          = next_state_os_lba0_abs ;
  state_os_lba1_abs              = next_state_os_lba1_abs ;
  state_os_sect0_abs             = next_state_os_sect0_abs ;
  state_os_sect1_abs             = next_state_os_sect1_abs ;
  state_os_buf_abs               = next_state_os_buf_abs ;
  state_osState_conc             = next_state_osState_conc ;
 end
 
 
endmodule
-------------------------------
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 28.9724 [2015-pre-classification]
#.