Details of instance cycle_sched_12_3_3.aag

Name: cycle_sched_12_3_3.aag
md5: 4bcbd33d037de66ca798ece53b5a8831
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 (78.9 kB)
aag 5546 38 341 1 5167
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 1
80 7869
82 7875
84 7881
86 7890
88 7900
90 7911
92 7920
94 7927
96 7933
98 7942
100 7952
102 7963
104 7972
106 7979
108 7985
110 7994
112 8004
114 8015
116 8024
118 8031
120 8037
122 8046
124 8056
126 8067
128 8076
130 8083
132 8089
134 8098
136 8108
138 8119
140 8128
142 8135
144 8141
146 8150
148 8160
150 8171
152 8180
154 8187
156 8193
158 8202
160 8212
162 8223
164 82

... [truncated 77.9 kB]

>
l320 _state_43<0>
l321 _state_40<0>
l322 _state_38<0>
l323 _state_35<0>
l324 _state_32<0>
l325 _state_31<0>
l326 _state_28<0>
l327 _state_26<0>
l328 _state_25<0>
l329 _state_22<0>
l330 _state_20<0>
l331 _state_19<0>
l332 _state_16<0>
l333 _state_14<0>
l334 _state_13<0>
l335 _state_10<0>
l336 _state_8<0>
l337 _state_7<0>
l338 _state_4<0>
l339 _state_2<0>
l340 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 11.0499 [2015-pre-classification]
#.