| Name: |
mult_bool_matrix_6_6_6.aag |
| md5: |
bcce62804a43fe2a24b062f377c28f75 |
| 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 |
aag 12157 108 0 1 12049
2
4
6
8
10
12
14
16
18
20
22
24
26
122
124
126
128
130
132
134
334
336
338
340
342
344
346
1112
1114
1116
1118
1120
1122
1124
1890
1892
1894
1896
1898
1900
1902
2668
2670
2672
2674
2676
2678
2680
3446
3448
3450
3452
3454
3456
3458
3658
3858
4332
4806
5280
5754
5756
5758
5760
5762
5764
5766
6532
7294
8056
8818
9580
10342
10344
10346
10348
10350
10352
10354
11120
11882
12644
13406
14168
14930
14932
14934
14936
14938
14940
14942
15708
16470
17232
17994
18756
19518
19520
19522
19524
1952
... [truncated 191.6 kB]
ble_c[5][5]<0>
o0 err<0>
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2015-pre-classification], 0/4 [SYNTCOMP2015-SyntSeq], 0/3 [SYNTCOMP2015-SyntPar], 1/7 [SYNTCOMP2015-RealSeq], 2/4 [SYNTCOMP2015-RealPar], 1/7 [SYNTCOMP2016-SyntSeq], 2/4 [SYNTCOMP2016-SyntPar], 1/11 [SYNTCOMP2016-RealSeq], 2/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 0.0 [2015-pre-classification], 3.46836 [SYNTCOMP2015-RealSeq], 3.81001 [SYNTCOMP2015-RealPar], 3.028 [SYNTCOMP2016-RealSeq], 3.3966 [SYNTCOMP2016-RealPar]
REF_SIZE : 15015
STATUS : realizable
#.