Details of instance ltl2dpa_01_2_REAL.aag

Name: ltl2dpa_01_2_REAL.aag
md5: f5f512c095faf33aec81b0282889adf4
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 (18.2 kB)
aag 1297 4 172 1 1121
2
4
6
8
10 1617
12 1621
14 1625
16 1629
18 0
20 1465
22 1469
24 1477
26 1633
28 1637
30 1641
32 1645
34 2315
36 2319
38 2323
40 2327
42 0
44 2371
46 2375
48 2383
50 2387
52 2391
54 2395
56 2399
58 1673
60 1677
62 1681
64 1685
66 0
68 1441
70 1445
72 1453
74 1841
76 1845
78 1849
80 1853
82 2355
84 2359
86 2363
88 2367
90 2467
92 2471
94 2475
96 2479
98 2105
100 2109
102 2113
104 2117
106 2153
108 2157
110 2161
112 2165
114 696
116 0
118 0
120 0
122 0
124 2443
126 2447
128 2455
130 1769


... [truncated 17.2 kB]

ch144
l145 latch145
l146 latch146
l147 latch147
l148 latch148
l149 latch149
l150 latch150
l151 latch151
l152 latch152
l153 latch153
l154 latch154
l155 latch155
l156 latch156
l157 latch157
l158 latch158
l159 latch159
l160 latch160
l161 latch161
l162 latch162
l163 latch163
l164 latch164
l165 latch165
l166 latch166
l167 latch167
l168 latch168
l169 latch169
l170 latch170
l171 latch171
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 0.852052 [SYNTCOMP2014-RealSeq]
#.