Details of instance load_5c_comp_comp3_UNREAL.aag

Name: load_5c_comp_comp3_UNREAL.aag
md5: b96123082090daeb8e08ec4adc6eb5a0
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 (124.3 kB)
aag 8027 11 590 1 7426
2
4
6
8
10
12
14
16
18
20
22
24 0
26 2935
28 2939
30 2943
32 2951
34 0
36 2765
38 2769
40 2773
42 2781
44 0
46 2659
48 2663
50 2667
52 2675
54 2923
56 2925
58 2927
60 2929
62 2931
64 2679
66 2683
68 2687
70 2691
72 2695
74 0
76 2459
78 2463
80 2467
82 2475
84 0
86 2439
88 2443
90 2447
92 2455
94 2149
96 2153
98 2157
100 2161
102 2165
104 0
106 2955
108 2959
110 2963
112 2971
114 2129
116 2133
118 2137
120 2141
122 2145
124 2725
126 2729
128 2733
130 2737
132 2741
134 2699
136 2703
138

... [truncated 123.3 kB]

015-RealPar], 4/7 [SYNTCOMP2016-SyntSeq], 3/4 [SYNTCOMP2016-SyntPar], 5/11 [SYNTCOMP2016-RealSeq], 3/6 [SYNTCOMP2016-RealPar], 3/10 [SYNTCOMP2017-RealSeq], 3/6 [SYNTCOMP2017-RealPar], 2/6 [SYNTCOMP2017-SyntSeq], 3/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [2015-pre-classification], 149.357 [SYNTCOMP2015-RealSeq], 328.385 [SYNTCOMP2015-RealPar], 126.704 [SYNTCOMP2016-RealSeq], 474.222 [SYNTCOMP2016-RealPar], 729.516 [SYNTCOMP2017-RealSeq], 404.678 [SYNTCOMP2017-RealPar]
REF_SIZE : 8714
STATUS : realizable
#.