Details of instance interface-with-overflows-k5-liveness.aag
Name: |
interface-with-overflows-k5-liveness.aag |
md5: |
4cf9df8e2be141e5ef8ee50967e91dae |
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 (27.4 kB)
aag 1958 7 50 1 1901
2
4
6
8
10
12
14
16 958
18 962
20 966
22 970
24 974
26 978
28 982
30 986
32 990
34 13
36 1014
38 1020
40 1026
42 1032
44 1038
46 1054
48 1062
50 1070
52 1078
54 1086
56 1092
58 1098
60 1104
62 1110
64 1116
66 1132
68 1186
70 1236
72 1310
74 1378
76 1395
78 2284
80 2670
82 2950
84 3168
86 3406
88 3630
90 3671
92 3694
94 3718
96 3735
98 3736
100 3795
102 3832
104 3837
106 3846
108 3852
110 3854
112 3859
114 3901
3917
116 34 33
118 116 31
120 118 28
122 120 27
124 122 25
126 124 23
128 126
... [truncated 26.4 kB]
-RealPar], 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 : 2.52992 [2015-pre-classification], 2.55133 [SYNTCOMP2015-RealSeq], 0.426354 [SYNTCOMP2015-RealPar], 1.172 [SYNTCOMP2016-RealSeq], 0.376617 [SYNTCOMP2016-RealPar], 2.04 [SYNTCOMP2017-RealSeq], 0.375851 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.