Details of instance ltl2dba_U1-4_comp3_REAL.aag

Name: ltl2dba_U1-4_comp3_REAL.aag
md5: cee84057dbaf75f996143f1612870529
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 (41.2 kB)
aag 2880 5 255 1 2620
2
4
6
8
10
12 4545
14 4549
16 4553
18 4557
20 4561
22 4565
24 4569
26 4573
28 4577
30 4581
32 0
34 2543
36 2547
38 2551
40 2559
42 3473
44 3477
46 3481
48 3485
50 3489
52 5525
54 5529
56 5533
58 5537
60 5541
62 4605
64 4609
66 4613
68 4617
70 4621
72 4525
74 4529
76 4533
78 4537
80 4541
82 0
84 2413
86 2417
88 2421
90 2429
92 2493
94 2497
96 2501
98 2505
100 2509
102 3653
104 3657
106 3661
108 3665
110 3669
112 2433
114 2437
116 2441
118 2445
120 2449
122 4275
124 4279
126 4283
128 428

... [truncated 40.2 kB]

27
l228 latch228
l229 latch229
l230 latch230
l231 latch231
l232 latch232
l233 latch233
l234 latch234
l235 latch235
l236 latch236
l237 latch237
l238 latch238
l239 latch239
l240 latch240
l241 latch241
l242 latch242
l243 latch243
l244 latch244
l245 latch245
l246 latch246
l247 latch247
l248 latch248
l249 latch249
l250 latch250
l251 latch251
l252 latch252
l253 latch253
l254 latch254
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2016-pre-classification]
SOLVED_IN : 10.38 [2016-pre-classification]
#.