Details of instance cycle_sched_6_5_3.aag

Name: cycle_sched_6_5_3.aag
md5: b3319486de219eb26e0be1cc315e7821
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 (50.2 kB)
aag 3601 20 233 1 3348
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42 1
44 4881
46 4887
48 4893
50 4902
52 4912
54 4922
56 4932
58 4943
60 4952
62 4959
64 4965
66 4974
68 4984
70 4994
72 5004
74 5015
76 5024
78 5031
80 5037
82 5046
84 5056
86 5066
88 5076
90 5087
92 5096
94 5103
96 5109
98 5118
100 5128
102 5138
104 5148
106 5159
108 5168
110 5175
112 5181
114 5190
116 5200
118 5210
120 5220
122 5231
124 5240
126 5247
128 5253
130 5262
132 5272
134 5282
136 5292
138 5303
140 5312
142 5319
144 53

... [truncated 49.2 kB]

>
l212 _state_48<0>
l213 _state_46<0>
l214 _state_45<0>
l215 _state_44<0>
l216 _state_41<0>
l217 _state_38<0>
l218 _state_36<0>
l219 _state_33<0>
l220 _state_28<0>
l221 _state_23<0>
l222 _state_20<0>
l223 _state_19<0>
l224 _state_16<0>
l225 _state_14<0>
l226 _state_13<0>
l227 _state_10<0>
l228 _state_8<0>
l229 _state_7<0>
l230 _state_4<0>
l231 _state_2<0>
l232 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 4.63406 [2015-pre-classification]
#.