diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-29 14:21:36 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-29 14:21:36 +0200 |
commit | b4bf8d387e430600790f6b30d9e88ec785148cd7 (patch) | |
tree | fdf6df1437823c9880b031405be498782109fdd8 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu | |
parent | Parse rational numbers in Z3PolyhedronSolver (diff) | |
download | VIATRA-Generator-b4bf8d387e430600790f6b30d9e88ec785148cd7.tar.gz VIATRA-Generator-b4bf8d387e430600790f6b30d9e88ec785148cd7.tar.zst VIATRA-Generator-b4bf8d387e430600790f6b30d9e88ec785148cd7.zip |
Make CbcPolyhedronSolver more robust
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | 154 |
1 files changed, 95 insertions, 59 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 7753e68e..4bd46fbf 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 | |||
@@ -1,27 +1,32 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
3 | import com.google.common.collect.ImmutableMap | 4 | import com.google.common.collect.ImmutableMap |
4 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult | 5 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult |
5 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver | 6 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver |
7 | import java.util.HashSet | ||
6 | import java.util.List | 8 | import java.util.List |
7 | import java.util.Map | 9 | import java.util.Map |
10 | import java.util.Set | ||
8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 11 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
9 | 12 | ||
10 | @FinalFieldsConstructor | 13 | @FinalFieldsConstructor |
11 | class CbcPolyhedronSolver implements PolyhedronSolver { | 14 | class CbcPolyhedronSolver implements PolyhedronSolver { |
15 | val boolean lpRelaxation | ||
12 | val double timeoutSeconds | 16 | val double timeoutSeconds |
13 | val boolean silent | 17 | val boolean silent |
14 | 18 | ||
15 | new() { | 19 | new() { |
16 | this(10, true) | 20 | this(false, -1, true) |
17 | } | 21 | } |
18 | 22 | ||
19 | override createSaturationOperator(Polyhedron polyhedron) { | 23 | override createSaturationOperator(Polyhedron polyhedron) { |
20 | new CbcSaturationOperator(polyhedron, timeoutSeconds, silent) | 24 | new CbcSaturationOperator(polyhedron, lpRelaxation, timeoutSeconds, silent) |
21 | } | 25 | } |
22 | } | 26 | } |
23 | 27 | ||
24 | class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | 28 | class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { |
29 | val boolean lpRelaxation | ||
25 | val double timeoutSeconds | 30 | val double timeoutSeconds |
26 | val boolean silent | 31 | val boolean silent |
27 | val double[] columnLowerBounds | 32 | val double[] columnLowerBounds |
@@ -29,8 +34,9 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
29 | val double[] objective | 34 | val double[] objective |
30 | val Map<Dimension, Integer> dimensionsToIndicesMap | 35 | val Map<Dimension, Integer> dimensionsToIndicesMap |
31 | 36 | ||
32 | new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { | 37 | new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds, boolean silent) { |
33 | super(polyhedron) | 38 | super(polyhedron) |
39 | this.lpRelaxation = lpRelaxation | ||
34 | this.timeoutSeconds = timeoutSeconds | 40 | this.timeoutSeconds = timeoutSeconds |
35 | this.silent = silent | 41 | this.silent = silent |
36 | val numDimensions = polyhedron.dimensions.size | 42 | val numDimensions = polyhedron.dimensions.size |
@@ -56,6 +62,12 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
56 | rowStarts.set(numConstraints, numEntries) | 62 | rowStarts.set(numConstraints, numEntries) |
57 | val columnIndices = newIntArrayOfSize(numEntries) | 63 | val columnIndices = newIntArrayOfSize(numEntries) |
58 | val entries = newDoubleArrayOfSize(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 | } | ||
59 | var int index = 0 | 71 | var int index = 0 |
60 | for (var int i = 0; i < numConstraints; i++) { | 72 | for (var int i = 0; i < numConstraints; i++) { |
61 | rowStarts.set(i, index) | 73 | rowStarts.set(i, index) |
@@ -69,6 +81,7 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
69 | val dimension = polyhedron.dimensions.get(j) | 81 | val dimension = polyhedron.dimensions.get(j) |
70 | val coefficient = constraint.coefficients.get(dimension) | 82 | val coefficient = constraint.coefficients.get(dimension) |
71 | if (coefficient !== null && coefficient != 0) { | 83 | if (coefficient !== null && coefficient != 0) { |
84 | unconstrainedDimensions -= dimension | ||
72 | columnIndices.set(index, j) | 85 | columnIndices.set(index, j) |
73 | entries.set(index, coefficient) | 86 | entries.set(index, coefficient) |
74 | index++ | 87 | index++ |
@@ -79,71 +92,94 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
79 | throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") | 92 | throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") |
80 | } | 93 | } |
81 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | 94 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { |
82 | for (var int j = 0; j < numDimensions; j++) { | 95 | val result = saturate(expressionToSaturate, rowStarts, columnIndices, entries, rowLowerBounds, |
83 | objective.set(j, 0) | 96 | rowUpperBounds, unconstrainedDimensions, constraints) |
97 | if (result != PolyhedronSaturationResult.SATURATED) { | ||
98 | return result | ||
84 | } | 99 | } |
85 | switch (expressionToSaturate) { | 100 | } |
86 | Dimension: { | 101 | PolyhedronSaturationResult.SATURATED |
87 | val j = getIndex(expressionToSaturate) | 102 | } |
88 | objective.set(j, 1) | 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 | ||
89 | } | 118 | } |
90 | LinearConstraint: { | 119 | val j = getIndex(expressionToSaturate) |
91 | for (pair : expressionToSaturate.coefficients.entrySet) { | 120 | objective.set(j, 1) |
92 | val j = getIndex(pair.key) | 121 | } |
93 | objective.set(j, pair.value) | 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 | ||
94 | } | 130 | } |
131 | val j = getIndex(dimension) | ||
132 | objective.set(j, pair.value) | ||
95 | } | 133 | } |
96 | default: | ||
97 | throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) | ||
98 | } | 134 | } |
99 | val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | 135 | default: |
100 | entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) | 136 | throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) |
101 | switch (minimizationResult) { | 137 | } |
102 | CbcResult.SolutionBounded: { | 138 | val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, |
103 | val value = Math.floor(minimizationResult.value) | 139 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) |
104 | expressionToSaturate.lowerBound = value as int | 140 | switch (minimizationResult) { |
105 | setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) | 141 | CbcResult.SolutionBounded: { |
106 | } | 142 | val value = Math.floor(minimizationResult.value) |
107 | case CbcResult.SOLUTION_UNBOUNDED: { | 143 | expressionToSaturate.lowerBound = value as int |
108 | expressionToSaturate.lowerBound = null | 144 | setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) |
109 | setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, | ||
110 | rowLowerBounds) | ||
111 | } | ||
112 | case CbcResult.UNSAT: | ||
113 | return PolyhedronSaturationResult.EMPTY | ||
114 | case CbcResult.ABANDONED, | ||
115 | case CbcResult.TIMEOUT: | ||
116 | return PolyhedronSaturationResult.UNKNOWN | ||
117 | default: | ||
118 | throw new RuntimeException("Unknown CbcResult: " + minimizationResult) | ||
119 | } | 145 | } |
120 | for (var int j = 0; j < numDimensions; j++) { | 146 | case CbcResult.SOLUTION_UNBOUNDED: { |
121 | val objectiveCoefficient = objective.get(j) | 147 | expressionToSaturate.lowerBound = null |
122 | objective.set(j, -objectiveCoefficient) | 148 | setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) |
123 | } | 149 | } |
124 | val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | 150 | case CbcResult.UNSAT: |
125 | entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) | 151 | return PolyhedronSaturationResult.EMPTY |
126 | switch (maximizationResult) { | 152 | case CbcResult.ABANDONED, |
127 | CbcResult.SolutionBounded: { | 153 | case CbcResult.TIMEOUT: |
128 | val value = Math.ceil(-maximizationResult.value) | 154 | return PolyhedronSaturationResult.UNKNOWN |
129 | expressionToSaturate.upperBound = value as int | 155 | default: |
130 | setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) | 156 | throw new RuntimeException("Unknown CbcResult: " + minimizationResult) |
131 | } | 157 | } |
132 | case CbcResult.SOLUTION_UNBOUNDED: { | 158 | for (var int j = 0; j < numDimensions; j++) { |
133 | expressionToSaturate.upperBound = null | 159 | val objectiveCoefficient = objective.get(j) |
134 | setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, | 160 | objective.set(j, -objectiveCoefficient) |
135 | rowUpperBounds) | 161 | } |
136 | } | 162 | val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, |
137 | case CbcResult.UNSAT: | 163 | entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) |
138 | throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") | 164 | switch (maximizationResult) { |
139 | case CbcResult.ABANDONED, | 165 | CbcResult.SolutionBounded: { |
140 | case CbcResult.TIMEOUT: | 166 | val value = Math.ceil(-maximizationResult.value) |
141 | return PolyhedronSaturationResult.UNKNOWN | 167 | expressionToSaturate.upperBound = value as int |
142 | default: | 168 | setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) |
143 | throw new RuntimeException("Unknown CbcResult: " + maximizationResult) | ||
144 | } | 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) | ||
145 | } | 181 | } |
146 | PolyhedronSaturationResult.SATURATED | 182 | return PolyhedronSaturationResult.SATURATED |
147 | } | 183 | } |
148 | 184 | ||
149 | private def toDouble(Integer nullableInt, double defaultValue) { | 185 | private def toDouble(Integer nullableInt, double defaultValue) { |