Details of instance ltl2dba_E4_comp4_REAL.aag

Name: ltl2dba_E4_comp4_REAL.aag
md5: bfc119c4fbb911d3029e14f9c9b9f8da
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 (85.5 kB)
aag 5787 5 450 1 5332
2
4
6
8
10
12 9199
14 9203
16 9207
18 9211
20 9215
22 9219
24 9175
26 9179
28 9183
30 9187
32 9191
34 9195
36 10315
38 10319
40 10323
42 10327
44 10331
46 10335
48 0
50 6199
52 6203
54 6207
56 6211
58 6219
60 9691
62 9695
64 9699
66 9703
68 9707
70 9711
72 9667
74 9671
76 9675
78 9679
80 9683
82 9687
84 9643
86 9647
88 9651
90 9655
92 9659
94 9663
96 9619
98 9623
100 9627
102 9631
104 9635
106 9639
108 9595
110 9599
112 9603
114 9607
116 9611
118 9615
120 9571
122 9575
124 9579
126 958

... [truncated 84.5 kB]


l423 latch423
l424 latch424
l425 latch425
l426 latch426
l427 latch427
l428 latch428
l429 latch429
l430 latch430
l431 latch431
l432 latch432
l433 latch433
l434 latch434
l435 latch435
l436 latch436
l437 latch437
l438 latch438
l439 latch439
l440 latch440
l441 latch441
l442 latch442
l443 latch443
l444 latch444
l445 latch445
l446 latch446
l447 latch447
l448 latch448
l449 latch449
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 1/3 [2016-pre-classification]
SOLVED_IN : 196.352 [2016-pre-classification]
#.