Details of instance gb_s2_r2_comp2_UNREAL.aag

Name: gb_s2_r2_comp2_UNREAL.aag
md5: c6489de67bb66677b8b0c6b663d1edc4
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 (54.0 kB)
aag 3587 8 472 1 3107
2
4
6
8
10
12
14
16
18 1737
20 1741
22 1745
24 1749
26 1343
28 1345
30 1347
32 1349
34 0
36 1663
38 1667
40 1675
42 0
44 1453
46 1457
48 1485
50 1453
52 1457
54 1461
56 1465
58 0
60 1251
62 1255
64 1263
66 1112
68 0
70 0
72 0
74 0
76 1343
78 1345
80 1353
82 0
84 1343
86 1345
88 1353
90 1405
92 1409
94 1413
96 1417
98 0
100 1705
102 1709
104 1717
106 1469
108 1473
110 1477
112 1481
114 1613
116 1617
118 1621
120 1625
122 1539
124 1543
126 1547
128 1551
130 1597
132 1601
134 1605
136 160

... [truncated 53.0 kB]

015-RealPar], 3/7 [SYNTCOMP2016-SyntSeq], 3/4 [SYNTCOMP2016-SyntPar], 6/11 [SYNTCOMP2016-RealSeq], 5/6 [SYNTCOMP2016-RealPar], 6/10 [SYNTCOMP2017-RealSeq], 5/6 [SYNTCOMP2017-RealPar], 3/6 [SYNTCOMP2017-SyntSeq], 3/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [2015-pre-classification], 4.52188 [SYNTCOMP2015-RealSeq], 0.959889 [SYNTCOMP2015-RealPar], 13.452 [SYNTCOMP2016-RealSeq], 0.894453 [SYNTCOMP2016-RealPar], 15.728 [SYNTCOMP2017-RealSeq], 0.887385 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.