Details of instance demo-v25_5_UNREAL.aag

Name: demo-v25_5_UNREAL.aag
md5: d5dd4015707a0f0779be8a482367d2fb
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 (20.5 kB)
aag 1340 4 280 1 1056
2
4
6
8
10 0
12 2155
14 2159
16 2163
18 2167
20 2171
22 2179
24 0
26 1955
28 1959
30 1963
32 1967
34 1971
36 1979
38 1857
40 1859
42 1861
44 1863
46 1865
48 1867
50 1869
52 1857
54 1859
56 1861
58 1863
60 1865
62 1867
64 1869
66 1857
68 1859
70 1861
72 1863
74 1865
76 1867
78 1869
80 0
82 1905
84 1909
86 1913
88 1917
90 1921
92 1947
94 0
96 2135
98 2137
100 2139
102 2141
104 2143
106 2151
108 0
110 1905
112 1909
114 1913
116 1917
118 1921
120 1947
122 0
124 1857
126 1859
128 1861
130 1

... [truncated 19.5 kB]

5-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 : 4.32827 [SYNTCOMP2014-RealSeq], 0.873074 [SYNTCOMP2015-RealSeq], 0.399282 [SYNTCOMP2015-RealPar], 0.692 [SYNTCOMP2016-RealSeq], 0.375715 [SYNTCOMP2016-RealPar], 0.688 [SYNTCOMP2017-RealSeq], 0.367595 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.