Details of instance cycle_sched_2_3_1.aag

Name: cycle_sched_2_3_1.aag
md5: ada6790449cfc2cabb2dd8d8baeac0a8
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 (6.6 kB)
aag 529 7 59 1 463
2
4
6
8
10
12
14
16 1
18 517
20 523
22 529
24 538
26 548
28 559
30 568
32 575
34 581
36 590
38 600
40 611
42 620
44 627
46 633
48 643
50 652
52 662
54 672
56 679
58 685
60 695
62 704
64 714
66 724
68 731
70 737
72 747
74 753
76 759
78 765
80 774
82 784
84 794
86 801
88 807
90 817
92 823
94 833
96 845
98 851
100 857
102 867
104 873
106 879
108 885
110 894
112 904
114 914
116 921
118 927
120 937
122 943
124 953
126 965
128 971
130 994
132 1001
1059
134 17 1
136 43 1
138 10 137
140 139 10
14

... [truncated 5.6 kB]

te_49<0>
l37 _state_47<0>
l38 _state_44<0>
l39 _state_41<0>
l40 _state_40<0>
l41 _state_37<0>
l42 _state_34<0>
l43 _state_32<0>
l44 _state_30<0>
l45 _state_28<0>
l46 _state_26<0>
l47 _state_24<0>
l48 _state_23<0>
l49 _state_22<0>
l50 _state_19<0>
l51 _state_16<0>
l52 _state_14<0>
l53 _state_11<0>
l54 _state_8<0>
l55 _state_7<0>
l56 _state_4<0>
l57 _state_2<0>
l58 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 0.03 [2015-pre-classification]
#.