Details of instance cycle_sched_6_5_2.aag

Name: cycle_sched_6_5_2.aag
md5: 06817593ac148eb8a7ff73fa59c4216d
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.6 kB) 
aag 3267 20 236 1 3011
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42 1
44 4171
46 4177
48 4183
50 4192
52 4202
54 4212
56 4222
58 4233
60 4242
62 4249
64 4255
66 4264
68 4274
70 4284
72 4294
74 4305
76 4314
78 4321
80 4327
82 4336
84 4346
86 4356
88 4366
90 4377
92 4386
94 4393
96 4399
98 4408
100 4418
102 4428
104 4438
106 4449
108 4458
110 4465
112 4471
114 4480
116 4490
118 4500
120 4510
122 4521
124 4530
126 4537
128 4543
130 4552
132 4562
134 4572
136 4582
138 4593
140 4602
142 4609
144 46

... [truncated 44.6 kB]

>
l215 _state_50<0>
l216 _state_47<0>
l217 _state_44<0>
l218 _state_42<0>
l219 _state_39<0>
l220 _state_34<0>
l221 _state_29<0>
l222 _state_26<0>
l223 _state_25<0>
l224 _state_22<0>
l225 _state_20<0>
l226 _state_19<0>
l227 _state_16<0>
l228 _state_14<0>
l229 _state_13<0>
l230 _state_10<0>
l231 _state_8<0>
l232 _state_7<0>
l233 _state_4<0>
l234 _state_2<0>
l235 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 5.02304 [2015-pre-classification]
#.