Details of instance ltl2dpa_E4_comp2_REAL.aag

Name: ltl2dpa_E4_comp2_REAL.aag
md5: 57665369bff9a56d99fb6b8cb306d168
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 (178.6 kB)
aag 11308 8 680 1 10620
2
4
6
8
10
12
14
16
18 0
20 1423
22 1427
24 1435
26 1397
28 28
30 30
32 32
34 0
36 21797
38 21801
40 21809
42 0
44 3567
46 3571
48 3579
50 19749
52 19753
54 19757
56 19761
58 19733
60 19737
62 19741
64 19745
66 19765
68 19769
70 19773
72 19777
74 12683
76 12685
78 12687
80 12689
82 12659
84 12661
86 12663
88 12665
90 12635
92 12637
94 12639
96 12641
98 19469
100 19473
102 19477
104 19481
106 12507
108 12509
110 12511
112 12513
114 12379
116 12381
118 12383
120 12385
122 12387
124 123

... [truncated 177.6 kB]

76
l677 latch677
l678 latch678
l679 latch679
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2016-pre-classification], 0/11 [SYNTCOMP2016-RealSeq], 1/6 [SYNTCOMP2016-RealPar], 0/4 [2017-pre-classification], 0/10 [SYNTCOMP2017-RealSeq], 1/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [2016-pre-classification], 0.0 [SYNTCOMP2016-RealSeq], 818.471 [SYNTCOMP2016-RealPar], 0.0 [SYNTCOMP2017-RealSeq], 825.502 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 10864
#.