Details of instance cycle_sched_2_10_1.aag

Name: cycle_sched_2_10_1.aag
md5: cf2fdae9e5a467533d3bfd8010deee51
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 (21.8 kB) 
aag 1612 7 129 1 1476
2
4
6
8
10
12
14
16 1
18 1667
20 1673
22 1679
24 1688
26 1698
28 1708
30 1718
32 1728
34 1738
36 1748
38 1758
40 1768
42 1779
44 1788
46 1795
48 1801
50 1810
52 1820
54 1830
56 1840
58 1850
60 1860
62 1870
64 1880
66 1890
68 1901
70 1910
72 1917
74 1923
76 1933
78 1942
80 1952
82 1962
84 1972
86 1982
88 1992
90 2002
92 2012
94 2022
96 2032
98 2039
100 2045
102 2055
104 2064
106 2074
108 2084
110 2094
112 2104
114 2114
116 2124
118 2134
120 2144
122 2154
124 2161
126 2167
128 2177
130 2

... [truncated 20.8 kB]

>
l108 _state_63<0>
l109 _state_61<0>
l110 _state_59<0>
l111 _state_58<0>
l112 _state_57<0>
l113 _state_54<0>
l114 _state_51<0>
l115 _state_49<0>
l116 _state_46<0>
l117 _state_41<0>
l118 _state_36<0>
l119 _state_31<0>
l120 _state_26<0>
l121 _state_21<0>
l122 _state_16<0>
l123 _state_11<0>
l124 _state_8<0>
l125 _state_7<0>
l126 _state_4<0>
l127 _state_2<0>
l128 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 1.64477 [2015-pre-classification]
#.