diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | 216 |
1 files changed, 216 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend new file mode 100644 index 00000000..4bd46fbf --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | |||
@@ -0,0 +1,216 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult | ||
6 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver | ||
7 | import java.util.HashSet | ||
8 | import java.util.List | ||
9 | import java.util.Map | ||
10 | import java.util.Set | ||
11 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
12 | |||
13 | @FinalFieldsConstructor | ||
14 | class CbcPolyhedronSolver implements PolyhedronSolver { | ||
15 | val boolean lpRelaxation | ||
16 | val double timeoutSeconds | ||
17 | val boolean silent | ||
18 | |||
19 | new() { | ||
20 | this(false, -1, true) | ||
21 | } | ||
22 | |||
23 | override createSaturationOperator(Polyhedron polyhedron) { | ||
24 | new CbcSaturationOperator(polyhedron, lpRelaxation, timeoutSeconds, silent) | ||
25 | } | ||
26 | } | ||
27 | |||
28 | class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | ||
29 | val boolean lpRelaxation | ||
30 | val double timeoutSeconds | ||
31 | val boolean silent | ||
32 | val double[] columnLowerBounds | ||
33 | val double[] columnUpperBounds | ||
34 | val double[] objective | ||
35 | val Map<Dimension, Integer> dimensionsToIndicesMap | ||
36 | |||
37 | new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds, boolean silent) { | ||
38 | super(polyhedron) | ||
39 | this.lpRelaxation = lpRelaxation | ||
40 | this.timeoutSeconds = timeoutSeconds | ||
41 | this.silent = silent | ||
42 | val numDimensions = polyhedron.dimensions.size | ||
43 | columnLowerBounds = newDoubleArrayOfSize(numDimensions) | ||
44 | columnUpperBounds = newDoubleArrayOfSize(numDimensions) | ||
45 | objective = newDoubleArrayOfSize(numDimensions) | ||
46 | dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) | ||
47 | } | ||
48 | |||
49 | override doSaturate() { | ||
50 | val numDimensions = polyhedron.dimensions.size | ||
51 | for (var int j = 0; j < numDimensions; j++) { | ||
52 | val dimension = polyhedron.dimensions.get(j) | ||
53 | columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
54 | columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
55 | } | ||
56 | val constraints = nonTrivialConstraints | ||
57 | val numConstraints = constraints.size | ||
58 | val rowStarts = newIntArrayOfSize(numConstraints + 1) | ||
59 | val rowLowerBounds = newDoubleArrayOfSize(numConstraints) | ||
60 | val rowUpperBounds = newDoubleArrayOfSize(numConstraints) | ||
61 | val numEntries = constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 | ||
62 | rowStarts.set(numConstraints, numEntries) | ||
63 | val columnIndices = newIntArrayOfSize(numEntries) | ||
64 | val entries = newDoubleArrayOfSize(numEntries) | ||
65 | val unconstrainedDimensions = new HashSet | ||
66 | for (dimension : polyhedron.dimensions) { | ||
67 | if (dimension.lowerBound === null && dimension.upperBound === null) { | ||
68 | unconstrainedDimensions += dimension | ||
69 | } | ||
70 | } | ||
71 | var int index = 0 | ||
72 | for (var int i = 0; i < numConstraints; i++) { | ||
73 | rowStarts.set(i, index) | ||
74 | val constraint = constraints.get(i) | ||
75 | rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
76 | rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
77 | if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { | ||
78 | throw new IllegalArgumentException("Constrains has unknown dimensions") | ||
79 | } | ||
80 | for (var int j = 0; j < numDimensions; j++) { | ||
81 | val dimension = polyhedron.dimensions.get(j) | ||
82 | val coefficient = constraint.coefficients.get(dimension) | ||
83 | if (coefficient !== null && coefficient != 0) { | ||
84 | unconstrainedDimensions -= dimension | ||
85 | columnIndices.set(index, j) | ||
86 | entries.set(index, coefficient) | ||
87 | index++ | ||
88 | } | ||
89 | } | ||
90 | } | ||
91 | if (index != numEntries) { | ||
92 | throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") | ||
93 | } | ||
94 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
95 | val result = saturate(expressionToSaturate, rowStarts, columnIndices, entries, rowLowerBounds, | ||
96 | rowUpperBounds, unconstrainedDimensions, constraints) | ||
97 | if (result != PolyhedronSaturationResult.SATURATED) { | ||
98 | return result | ||
99 | } | ||
100 | } | ||
101 | PolyhedronSaturationResult.SATURATED | ||
102 | } | ||
103 | |||
104 | protected def saturate(LinearBoundedExpression expressionToSaturate, int[] rowStarts, int[] columnIndices, | ||
105 | double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, Set<Dimension> unconstrainedDimensions, | ||
106 | ImmutableList<LinearConstraint> constraints) { | ||
107 | val numDimensions = objective.size | ||
108 | for (var int j = 0; j < numDimensions; j++) { | ||
109 | objective.set(j, 0) | ||
110 | } | ||
111 | switch (expressionToSaturate) { | ||
112 | Dimension: { | ||
113 | // CBC will return nonsensical results or call free() with invalid arguments if | ||
114 | // it is passed a fully unconstrained (-Inf lower and +Int upper bound, no inequalities) variable | ||
115 | // in the objective function. | ||
116 | if (unconstrainedDimensions.contains(expressionToSaturate)) { | ||
117 | return PolyhedronSaturationResult.SATURATED | ||
118 | } | ||
119 | val j = getIndex(expressionToSaturate) | ||
120 | objective.set(j, 1) | ||
121 | } | ||
122 | LinearConstraint: { | ||
123 | for (pair : expressionToSaturate.coefficients.entrySet) { | ||
124 | val dimension = pair.key | ||
125 | // We also have to check for unconstrained dimensions here to avoid crashing. | ||
126 | if (unconstrainedDimensions.contains(dimension)) { | ||
127 | expressionToSaturate.lowerBound = null | ||
128 | expressionToSaturate.upperBound = null | ||
129 | return PolyhedronSaturationResult.SATURATED | ||
130 | } | ||
131 | val j = getIndex(dimension) | ||
132 | objective.set(j, pair.value) | ||
133 | } | ||
134 | } | ||
135 | default: | ||
136 | throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) | ||
137 | } | ||
138 | val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
139 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) | ||
140 | switch (minimizationResult) { | ||
141 | CbcResult.SolutionBounded: { | ||
142 | val value = Math.floor(minimizationResult.value) | ||
143 | expressionToSaturate.lowerBound = value as int | ||
144 | setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) | ||
145 | } | ||
146 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
147 | expressionToSaturate.lowerBound = null | ||
148 | setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) | ||
149 | } | ||
150 | case CbcResult.UNSAT: | ||
151 | return PolyhedronSaturationResult.EMPTY | ||
152 | case CbcResult.ABANDONED, | ||
153 | case CbcResult.TIMEOUT: | ||
154 | return PolyhedronSaturationResult.UNKNOWN | ||
155 | default: | ||
156 | throw new RuntimeException("Unknown CbcResult: " + minimizationResult) | ||
157 | } | ||
158 | for (var int j = 0; j < numDimensions; j++) { | ||
159 | val objectiveCoefficient = objective.get(j) | ||
160 | objective.set(j, -objectiveCoefficient) | ||
161 | } | ||
162 | val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
163 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) | ||
164 | switch (maximizationResult) { | ||
165 | CbcResult.SolutionBounded: { | ||
166 | val value = Math.ceil(-maximizationResult.value) | ||
167 | expressionToSaturate.upperBound = value as int | ||
168 | setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) | ||
169 | } | ||
170 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
171 | expressionToSaturate.upperBound = null | ||
172 | setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) | ||
173 | } | ||
174 | case CbcResult.UNSAT: | ||
175 | throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") | ||
176 | case CbcResult.ABANDONED, | ||
177 | case CbcResult.TIMEOUT: | ||
178 | return PolyhedronSaturationResult.UNKNOWN | ||
179 | default: | ||
180 | throw new RuntimeException("Unknown CbcResult: " + maximizationResult) | ||
181 | } | ||
182 | return PolyhedronSaturationResult.SATURATED | ||
183 | } | ||
184 | |||
185 | private def toDouble(Integer nullableInt, double defaultValue) { | ||
186 | if (nullableInt === null) { | ||
187 | defaultValue | ||
188 | } else { | ||
189 | nullableInt.doubleValue | ||
190 | } | ||
191 | } | ||
192 | |||
193 | private def int getIndex(Dimension dimension) { | ||
194 | val index = dimensionsToIndicesMap.get(dimension) | ||
195 | if (index === null) { | ||
196 | throw new IllegalArgumentException("Unknown dimension: " + dimension) | ||
197 | } | ||
198 | index | ||
199 | } | ||
200 | |||
201 | private def void setBound(LinearBoundedExpression expression, List<LinearConstraint> constraints, double bound, | ||
202 | double[] columnBounds, double[] rowBounds) { | ||
203 | switch (expression) { | ||
204 | Dimension: { | ||
205 | val j = getIndex(expression) | ||
206 | columnBounds.set(j, bound) | ||
207 | } | ||
208 | LinearConstraint: { | ||
209 | val i = constraints.indexOf(expression) | ||
210 | if (i >= 0) { | ||
211 | rowBounds.set(i, bound) | ||
212 | } | ||
213 | } | ||
214 | } | ||
215 | } | ||
216 | } | ||