Details of instance amba2match5.aag

Name: amba2match5.aag
md5: f13e3a70094b9b7164e60cf7a6b7c079
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 (59.6 kB) 
aag 4228 19 55 1 4154
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40 1
42 4
44 749
46 12
48 1130
50 1554
52 14
54 1758
56 3006
58 3074
60 3078
62 3087
64 10
66 2
68 6
70 3228
72 3326
74 3693
76 3723
78 3867
80 3908
82 3995
84 8
86 4124
88 3909
90 18
92 4725
94 26
96 5106
98 5530
100 28
102 5734
104 6982
106 7050
108 7054
110 7063
112 24
114 16
116 20
118 7204
120 7302
122 7669
124 7699
126 7843
128 7884
130 7971
132 22
134 8100
136 8416
138 1
140 30
142 32
144 34
146 36
148 38
8456
150 80 40
152 50

... [truncated 58.6 kB]

8 sink
l49 init
l50 L: F 5337
l51 L: X 9150
l52 L: X 7103
l53 L: X 6695
l54 L: X 404
c
#!SYNTCOMP
SOLVED_BY : 7/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 11/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.288 [SYNTCOMP2016-RealSeq], 0.049547 [SYNTCOMP2016-RealPar], 0.284 [SYNTCOMP2017-RealSeq], 0.049658 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.