Details of instance load_4c_comp_comp7_REAL.aag

Name: load_4c_comp_comp7_REAL.aag
md5: 07c4a09b5d394cd2af3eb98e6139ac9b
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.5 kB)
aag 11089 9 864 1 10216
2
4
6
8
10
12
14
16
18
20 0
22 4685
24 4689
26 4693
28 4697
30 4701
32 4705
34 4709
36 4717
38 0
40 4379
42 4383
44 4387
46 4391
48 4395
50 4399
52 4403
54 4411
56 0
58 4195
60 4199
62 4203
64 4207
66 4211
68 4215
70 4219
72 4227
74 4665
76 4667
78 4669
80 4671
82 4673
84 4675
86 4677
88 4679
90 4681
92 4231
94 4235
96 4239
98 4243
100 4247
102 4251
104 4255
106 4259
108 4263
110 0
112 3835
114 3839
116 3843
118 3847
120 3851
122 3855
124 3859
126 3867
128 0
130 3799
132 3803
134 380

... [truncated 177.5 kB]

863 latch863
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2015-pre-classification], 0/4 [SYNTCOMP2015-SyntSeq], 0/3 [SYNTCOMP2015-SyntPar], 3/7 [SYNTCOMP2015-RealSeq], 2/4 [SYNTCOMP2015-RealPar], 3/7 [SYNTCOMP2016-SyntSeq], 2/4 [SYNTCOMP2016-SyntPar], 6/11 [SYNTCOMP2016-RealSeq], 2/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 0.0 [2015-pre-classification], 76.1761 [SYNTCOMP2015-RealSeq], 87.8889 [SYNTCOMP2015-RealPar], 122.316 [SYNTCOMP2016-RealSeq], 107.342 [SYNTCOMP2016-RealPar]
REF_SIZE : 11530
STATUS : realizable
#.