Details of instance cycle_sched_4_8_2.aag

Name: cycle_sched_4_8_2.aag
md5: 6c37b6e992fde1654af32ef6ba3d0fbe
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 (42.1 kB) 
aag 3033 14 219 1 2800
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30 1
32 3639
34 3645
36 3651
38 3660
40 3670
42 3680
44 3690
46 3700
48 3710
50 3720
52 3731
54 3740
56 3747
58 3753
60 3762
62 3772
64 3782
66 3792
68 3802
70 3812
72 3822
74 3833
76 3842
78 3849
80 3855
82 3864
84 3874
86 3884
88 3894
90 3904
92 3914
94 3924
96 3935
98 3944
100 3951
102 3957
104 3966
106 3976
108 3986
110 3996
112 4006
114 4016
116 4026
118 4037
120 4046
122 4053
124 4059
126 4069
128 4078
130 4088
132 4098
134 4108
136 4118
138

... [truncated 41.1 kB]

te_28<0>
l207 _state_23<0>
l208 _state_20<0>
l209 _state_19<0>
l210 _state_16<0>
l211 _state_14<0>
l212 _state_13<0>
l213 _state_10<0>
l214 _state_8<0>
l215 _state_7<0>
l216 _state_4<0>
l217 _state_2<0>
l218 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
SOLVED_BY : 4/4 [2017-pre-classification], 9/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 4.72 [SYNTCOMP2017-RealSeq], 7.11735 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 3462
#.