Details of instance cnt30n.aag

Name: cnt30n.aag
md5: 348c7b8f0ebc56aba8f216eaf2d27ce7
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 (7.3 kB)
aag 483 2 31 1 450
2
4
6 1
8 793
10 799
12 805
14 811
16 817
18 823
20 829
22 835
24 841
26 847
28 853
30 859
32 865
34 871
36 877
38 883
40 889
42 895
44 901
46 907
48 913
50 919
52 925
54 931
56 937
58 943
60 949
62 955
64 961
66 967
304
68 9 6
70 8 6
72 69 6
74 11 6
76 10 6
78 75 6
80 13 6
82 12 6
84 81 6
86 15 6
88 14 6
90 87 6
92 17 6
94 16 6
96 93 6
98 19 6
100 18 6
102 99 6
104 21 6
106 20 6
108 105 6
110 23 6
112 22 6
114 111 6
116 25 6
118 24 6
120 117 6
122 27 6
124 26 6
126 123 6
128 29 6
130 28 

... [truncated 6.3 kB]

1/4 [SYNTCOMP2015-RealPar], 0/7 [SYNTCOMP2016-SyntSeq], 1/4 [SYNTCOMP2016-SyntPar], 0/11 [SYNTCOMP2016-RealSeq], 1/6 [SYNTCOMP2016-RealPar], 0/10 [SYNTCOMP2017-RealSeq], 1/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [SYNTCOMP2014-RealSeq], 0.0 [SYNTCOMP2015-RealSeq], 0.374473 [SYNTCOMP2015-RealPar], 0.0 [SYNTCOMP2016-RealSeq], 0.27045 [SYNTCOMP2016-RealPar], 0.0 [SYNTCOMP2017-RealSeq], 0.274254 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 451
#.