Details of instance cycle_sched_24_2_4.aag

Name: cycle_sched_24_2_4.aag
md5: 32b7a07a8d5add597b7340c252f8186e
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 (223.0 kB)
aag 14386 74 551 1 13761
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
110
112
114
116
118
120
122
124
126
128
130
132
134
136
138
140
142
144
146
148
150 1
152 23547
154 23553
156 23559
158 23568
160 23579
162 23588
164 23595
166 23601
168 23610
170 23621
172 23630
174 23637
176 23643
178 23652
180 23663
182 23672
184 23679
186 23685
188 23694
190 23705
192 23714
194 23721
196 23727
198 2373

... [truncated 222.0 kB]

>
l530 _state_40<0>
l531 _state_38<0>
l532 _state_37<0>
l533 _state_34<0>
l534 _state_32<0>
l535 _state_31<0>
l536 _state_28<0>
l537 _state_26<0>
l538 _state_25<0>
l539 _state_22<0>
l540 _state_20<0>
l541 _state_19<0>
l542 _state_16<0>
l543 _state_14<0>
l544 _state_13<0>
l545 _state_10<0>
l546 _state_8<0>
l547 _state_7<0>
l548 _state_4<0>
l549 _state_2<0>
l550 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 1/3 [2015-pre-classification]
SOLVED_IN : 200.557 [2015-pre-classification]
#.