Details of instance mult_bool_matrix_dyn_6_6.aag

Name: mult_bool_matrix_dyn_6_6.aag
md5: 08d4791419a6247d73a186ee16c6c617
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 (23.5 kB)
aag 1799 36 37 1 1726
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52
54
56
58
60
62
64
66
68
70
72
74 661
76 743
78 829
80 911
82 997
84 1079
86 1161
88 1247
90 1329
92 1415
94 1497
96 1583
98 1669
100 1751
102 1837
104 1919
106 2005
108 2087
110 2169
112 2255
114 2337
116 2423
118 2505
120 2591
122 2677
124 2759
126 2845
128 2927
130 3013
132 3095
134 3177
136 3263
138 3345
140 3431
142 3513
144 3599
146 220
575
148 75 1
150 77 1
152 79 1
154 81 1
156 83 1
158 85 1
160 87 1
162 8

... [truncated 22.5 kB]

[5]<0>
l12 a[2][0]<0>
l13 a[2][1]<0>
l14 a[2][2]<0>
l15 a[2][3]<0>
l16 a[2][4]<0>
l17 a[2][5]<0>
l18 a[3][0]<0>
l19 a[3][1]<0>
l20 a[3][2]<0>
l21 a[3][3]<0>
l22 a[3][4]<0>
l23 a[3][5]<0>
l24 a[4][0]<0>
l25 a[4][1]<0>
l26 a[4][2]<0>
l27 a[4][3]<0>
l28 a[4][4]<0>
l29 a[4][5]<0>
l30 a[5][0]<0>
l31 a[5][1]<0>
l32 a[5][2]<0>
l33 a[5][3]<0>
l34 a[5][4]<0>
l35 a[5][5]<0>
l36 init_latch<0>
o0 err<0>
c
#!SYNTCOMP
STATUS : unknown
SOLVED_BY : 0/3 [2015-pre-classification]
SOLVED_IN : 0.0 [2015-pre-classification]
#.