diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-25 19:03:01 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-25 19:04:58 +0200 |
commit | 52a015c1558b9ce5fb10f27d41e508dfec1e79d6 (patch) | |
tree | a0868c35b857c82eec8641e6dfcb07f2c9859dc5 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | |
parent | Containment root constraint propagator (diff) | |
download | VIATRA-Generator-52a015c1558b9ce5fb10f27d41e508dfec1e79d6.tar.gz VIATRA-Generator-52a015c1558b9ce5fb10f27d41e508dfec1e79d6.tar.zst VIATRA-Generator-52a015c1558b9ce5fb10f27d41e508dfec1e79d6.zip |
Make polyhedron solvers more robust
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 | 36 |
1 files changed, 17 insertions, 19 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 index 1f6d4e8f..7753e68e 100644 --- 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 | |||
@@ -3,8 +3,8 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | |||
3 | import com.google.common.collect.ImmutableMap | 3 | import com.google.common.collect.ImmutableMap |
4 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult | 4 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult |
5 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver | 5 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver |
6 | import java.util.List | ||
6 | import java.util.Map | 7 | import java.util.Map |
7 | import org.eclipse.xtend.lib.annotations.Accessors | ||
8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
9 | 9 | ||
10 | @FinalFieldsConstructor | 10 | @FinalFieldsConstructor |
@@ -21,8 +21,7 @@ class CbcPolyhedronSolver implements PolyhedronSolver { | |||
21 | } | 21 | } |
22 | } | 22 | } |
23 | 23 | ||
24 | class CbcSaturationOperator implements PolyhedronSaturationOperator { | 24 | class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { |
25 | @Accessors val Polyhedron polyhedron | ||
26 | val double timeoutSeconds | 25 | val double timeoutSeconds |
27 | val boolean silent | 26 | val boolean silent |
28 | val double[] columnLowerBounds | 27 | val double[] columnLowerBounds |
@@ -31,7 +30,7 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { | |||
31 | val Map<Dimension, Integer> dimensionsToIndicesMap | 30 | val Map<Dimension, Integer> dimensionsToIndicesMap |
32 | 31 | ||
33 | new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { | 32 | new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { |
34 | this.polyhedron = polyhedron | 33 | super(polyhedron) |
35 | this.timeoutSeconds = timeoutSeconds | 34 | this.timeoutSeconds = timeoutSeconds |
36 | this.silent = silent | 35 | this.silent = silent |
37 | val numDimensions = polyhedron.dimensions.size | 36 | val numDimensions = polyhedron.dimensions.size |
@@ -41,25 +40,26 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { | |||
41 | dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) | 40 | dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) |
42 | } | 41 | } |
43 | 42 | ||
44 | override saturate() { | 43 | override doSaturate() { |
45 | val numDimensions = polyhedron.dimensions.size | 44 | val numDimensions = polyhedron.dimensions.size |
46 | for (var int j = 0; j < numDimensions; j++) { | 45 | for (var int j = 0; j < numDimensions; j++) { |
47 | val dimension = polyhedron.dimensions.get(j) | 46 | val dimension = polyhedron.dimensions.get(j) |
48 | columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | 47 | columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) |
49 | columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) | 48 | columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) |
50 | } | 49 | } |
51 | val numConstraints = polyhedron.constraints.size | 50 | val constraints = nonTrivialConstraints |
51 | val numConstraints = constraints.size | ||
52 | val rowStarts = newIntArrayOfSize(numConstraints + 1) | 52 | val rowStarts = newIntArrayOfSize(numConstraints + 1) |
53 | val rowLowerBounds = newDoubleArrayOfSize(numConstraints) | 53 | val rowLowerBounds = newDoubleArrayOfSize(numConstraints) |
54 | val rowUpperBounds = newDoubleArrayOfSize(numConstraints) | 54 | val rowUpperBounds = newDoubleArrayOfSize(numConstraints) |
55 | val numEntries = polyhedron.constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 | 55 | val numEntries = constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 |
56 | rowStarts.set(numConstraints, numEntries) | 56 | rowStarts.set(numConstraints, numEntries) |
57 | val columnIndices = newIntArrayOfSize(numEntries) | 57 | val columnIndices = newIntArrayOfSize(numEntries) |
58 | val entries = newDoubleArrayOfSize(numEntries) | 58 | val entries = newDoubleArrayOfSize(numEntries) |
59 | var int index = 0 | 59 | var int index = 0 |
60 | for (var int i = 0; i < numConstraints; i++) { | 60 | for (var int i = 0; i < numConstraints; i++) { |
61 | rowStarts.set(i, index) | 61 | rowStarts.set(i, index) |
62 | val constraint = polyhedron.constraints.get(i) | 62 | val constraint = constraints.get(i) |
63 | rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | 63 | rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) |
64 | rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) | 64 | rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) |
65 | if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { | 65 | if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { |
@@ -102,11 +102,12 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { | |||
102 | CbcResult.SolutionBounded: { | 102 | CbcResult.SolutionBounded: { |
103 | val value = Math.floor(minimizationResult.value) | 103 | val value = Math.floor(minimizationResult.value) |
104 | expressionToSaturate.lowerBound = value as int | 104 | expressionToSaturate.lowerBound = value as int |
105 | setBound(expressionToSaturate, value, columnLowerBounds, rowLowerBounds) | 105 | setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) |
106 | } | 106 | } |
107 | case CbcResult.SOLUTION_UNBOUNDED: { | 107 | case CbcResult.SOLUTION_UNBOUNDED: { |
108 | expressionToSaturate.lowerBound = null | 108 | expressionToSaturate.lowerBound = null |
109 | setBound(expressionToSaturate, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) | 109 | setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, |
110 | rowLowerBounds) | ||
110 | } | 111 | } |
111 | case CbcResult.UNSAT: | 112 | case CbcResult.UNSAT: |
112 | return PolyhedronSaturationResult.EMPTY | 113 | return PolyhedronSaturationResult.EMPTY |
@@ -126,11 +127,12 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { | |||
126 | CbcResult.SolutionBounded: { | 127 | CbcResult.SolutionBounded: { |
127 | val value = Math.ceil(-maximizationResult.value) | 128 | val value = Math.ceil(-maximizationResult.value) |
128 | expressionToSaturate.upperBound = value as int | 129 | expressionToSaturate.upperBound = value as int |
129 | setBound(expressionToSaturate, value, columnUpperBounds, rowUpperBounds) | 130 | setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) |
130 | } | 131 | } |
131 | case CbcResult.SOLUTION_UNBOUNDED: { | 132 | case CbcResult.SOLUTION_UNBOUNDED: { |
132 | expressionToSaturate.upperBound = null | 133 | expressionToSaturate.upperBound = null |
133 | setBound(expressionToSaturate, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) | 134 | setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, |
135 | rowUpperBounds) | ||
134 | } | 136 | } |
135 | case CbcResult.UNSAT: | 137 | case CbcResult.UNSAT: |
136 | throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") | 138 | throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") |
@@ -160,23 +162,19 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { | |||
160 | index | 162 | index |
161 | } | 163 | } |
162 | 164 | ||
163 | private def void setBound(LinearBoundedExpression expression, double bound, double[] columnBounds, | 165 | private def void setBound(LinearBoundedExpression expression, List<LinearConstraint> constraints, double bound, |
164 | double[] rowBounds) { | 166 | double[] columnBounds, double[] rowBounds) { |
165 | switch (expression) { | 167 | switch (expression) { |
166 | Dimension: { | 168 | Dimension: { |
167 | val j = getIndex(expression) | 169 | val j = getIndex(expression) |
168 | columnBounds.set(j, bound) | 170 | columnBounds.set(j, bound) |
169 | } | 171 | } |
170 | LinearConstraint: { | 172 | LinearConstraint: { |
171 | val i = polyhedron.constraints.indexOf(expression) | 173 | val i = constraints.indexOf(expression) |
172 | if (i >= 0) { | 174 | if (i >= 0) { |
173 | rowBounds.set(i, bound) | 175 | rowBounds.set(i, bound) |
174 | } | 176 | } |
175 | } | 177 | } |
176 | } | 178 | } |
177 | } | 179 | } |
178 | |||
179 | override close() throws Exception { | ||
180 | // Nothing to close | ||
181 | } | ||
182 | } | 180 | } |