diff options
Diffstat (limited to 'Solvers')
5 files changed, 134 insertions, 84 deletions
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp index 49994244..ffd35759 100644 --- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp | |||
@@ -36,9 +36,10 @@ static const jint kCbcError = 5; | |||
36 | static CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | 36 | static CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, |
37 | jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, | 37 | jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, |
38 | jdoubleArray entriedArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, | 38 | jdoubleArray entriedArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, |
39 | jdoubleArray objectiveArray); | 39 | jdoubleArray objectiveArray, jboolean lpRelaxation); |
40 | static void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | 40 | static void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, |
41 | jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build); | 41 | jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, jboolean lpRelaxation, |
42 | CoinModel &build); | ||
42 | static void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, | 43 | static void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, |
43 | jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, | 44 | jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, |
44 | CoinModel &build); | 45 | CoinModel &build); |
@@ -83,11 +84,11 @@ jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( | |||
83 | JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, | 84 | JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, |
84 | jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, | 85 | jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, |
85 | jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, | 86 | jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, |
86 | jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent) { | 87 | jdoubleArray outputArray, jboolean lpRelaxation, jdouble timeoutSeconds, jboolean silent) { |
87 | try { | 88 | try { |
88 | auto build = CreateModel(env, columnLowerBoundsArray, columnUpperBoundsArray, | 89 | auto build = CreateModel(env, columnLowerBoundsArray, columnUpperBoundsArray, |
89 | rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, | 90 | rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, |
90 | objectiveArray); | 91 | objectiveArray, lpRelaxation); |
91 | double value; | 92 | double value; |
92 | jint result = SolveModel(build, timeoutSeconds, silent, value); | 93 | jint result = SolveModel(build, timeoutSeconds, silent, value); |
93 | if (result == kCbcSolutionBounded) { | 94 | if (result == kCbcSolutionBounded) { |
@@ -106,16 +107,18 @@ jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( | |||
106 | CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | 107 | CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, |
107 | jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, | 108 | jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, |
108 | jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, | 109 | jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, |
109 | jdoubleArray objectiveArray) { | 110 | jdoubleArray objectiveArray, jboolean lpRelaxation) { |
110 | CoinModel build; | 111 | CoinModel build; |
111 | CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, build); | 112 | CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, |
113 | lpRelaxation, build); | ||
112 | CreateModelRows(env, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, | 114 | CreateModelRows(env, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, |
113 | rowUpperBoundsArray, build); | 115 | rowUpperBoundsArray, build); |
114 | return build; | 116 | return build; |
115 | } | 117 | } |
116 | 118 | ||
117 | void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | 119 | void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, |
118 | jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build) { | 120 | jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, jboolean lpRelaxation, |
121 | CoinModel &build) { | ||
119 | int numColumns = env->GetArrayLength(columnLowerBoundsArray); | 122 | int numColumns = env->GetArrayLength(columnLowerBoundsArray); |
120 | PinnedDoubleArray columnLowerBounds{env, columnLowerBoundsArray}; | 123 | PinnedDoubleArray columnLowerBounds{env, columnLowerBoundsArray}; |
121 | PinnedDoubleArray columnUpperBounds{env, columnUpperBoundsArray}; | 124 | PinnedDoubleArray columnUpperBounds{env, columnUpperBoundsArray}; |
@@ -123,7 +126,9 @@ void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | |||
123 | for (int i = 0; i < numColumns; i++) { | 126 | for (int i = 0; i < numColumns; i++) { |
124 | build.setColumnBounds(i, columnLowerBounds[i], columnUpperBounds[i]); | 127 | build.setColumnBounds(i, columnLowerBounds[i], columnUpperBounds[i]); |
125 | build.setObjective(i, objective[i]); | 128 | build.setObjective(i, objective[i]); |
126 | build.setInteger(i); | 129 | if (!lpRelaxation) { |
130 | build.setInteger(i); | ||
131 | } | ||
127 | } | 132 | } |
128 | } | 133 | } |
129 | 134 | ||
@@ -215,6 +220,9 @@ jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdoub | |||
215 | if (model.isInitialSolveProvenPrimalInfeasible()) { | 220 | if (model.isInitialSolveProvenPrimalInfeasible()) { |
216 | return kCbcUnsat; | 221 | return kCbcUnsat; |
217 | } | 222 | } |
223 | if (model.isInitialSolveProvenDualInfeasible()) { | ||
224 | return kCbcSolutionUnbounded; | ||
225 | } | ||
218 | if (model.isInitialSolveAbandoned()) { | 226 | if (model.isInitialSolveAbandoned()) { |
219 | return kCbcTimeout; | 227 | return kCbcTimeout; |
220 | } | 228 | } |
@@ -226,20 +234,26 @@ jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdoub | |||
226 | 234 | ||
227 | model.branchAndBound(); | 235 | model.branchAndBound(); |
228 | 236 | ||
229 | if (model.isProvenInfeasible()) { | 237 | switch (model.status()) { |
230 | return kCbcUnsat; | 238 | case 0: |
231 | } | 239 | if (model.isProvenInfeasible()) { |
232 | if (model.isProvenDualInfeasible()) { | 240 | return kCbcUnsat; |
233 | return kCbcSolutionUnbounded; | 241 | } |
234 | } | 242 | if (model.isProvenDualInfeasible()) { |
235 | if (model.isProvenOptimal()) { | 243 | return kCbcSolutionUnbounded; |
236 | value = model.getMinimizationObjValue(); | 244 | } |
237 | return kCbcSolutionBounded; | 245 | if (model.isProvenOptimal()) { |
238 | } | 246 | value = model.getMinimizationObjValue(); |
239 | if (model.maximumSecondsReached()) { | 247 | return kCbcSolutionBounded; |
248 | } | ||
249 | throw std::runtime_error("CBC status is 0, but no solution is found"); | ||
250 | case 1: | ||
240 | return kCbcTimeout; | 251 | return kCbcTimeout; |
252 | case 2: | ||
253 | return kCbcAbandoned; | ||
254 | default: | ||
255 | throw std::runtime_error("Unknown CBC status"); | ||
241 | } | 256 | } |
242 | return kCbcAbandoned; | ||
243 | } | 257 | } |
244 | 258 | ||
245 | void ThrowException(JNIEnv *env, const char *message) { | 259 | void ThrowException(JNIEnv *env, const char *message) { |
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp index c65f71e3..12198c8b 100644 --- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp | |||
@@ -9,7 +9,7 @@ JNIEXPORT jint JNICALL Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIl | |||
9 | JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, | 9 | JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, |
10 | jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, | 10 | jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, |
11 | jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, | 11 | jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, |
12 | jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent); | 12 | jdoubleArray outputArray, jboolean lpRelaxation, jdouble timeoutSeconds, jboolean silent); |
13 | 13 | ||
14 | } | 14 | } |
15 | 15 | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so index 21fd2ff2..4eae7de6 100755 --- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so | |||
Binary files differ | |||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java index 39b9d537..085d4448 100644 --- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java | |||
@@ -15,14 +15,14 @@ public class CbcSolver { | |||
15 | } | 15 | } |
16 | 16 | ||
17 | public static CbcResult solve(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, | 17 | public static CbcResult solve(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, |
18 | int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, | 18 | int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, |
19 | double[] objective, double timeoutSeconds, boolean silent) { | 19 | boolean lpRelaxation, double timeoutSeconds, boolean silent) { |
20 | loadNatives(); | 20 | loadNatives(); |
21 | validate(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, rowLowerBounds, | 21 | validate(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, rowLowerBounds, |
22 | rowUpperBounds, objective); | 22 | rowUpperBounds, objective); |
23 | double[] output = new double[1]; | 23 | double[] output = new double[1]; |
24 | int result = solveIlpProblem(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, | 24 | int result = solveIlpProblem(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, |
25 | rowLowerBounds, rowUpperBounds, objective, output, timeoutSeconds, silent); | 25 | rowLowerBounds, rowUpperBounds, objective, output, lpRelaxation, timeoutSeconds, silent); |
26 | if (result == CBC_SOLUTION_BOUNDED) { | 26 | if (result == CBC_SOLUTION_BOUNDED) { |
27 | return new CbcResult.SolutionBounded(output[0]); | 27 | return new CbcResult.SolutionBounded(output[0]); |
28 | } else if (result == CBC_SOLUTION_UNBOUNDED) { | 28 | } else if (result == CBC_SOLUTION_UNBOUNDED) { |
@@ -67,5 +67,5 @@ public class CbcSolver { | |||
67 | 67 | ||
68 | private static native int solveIlpProblem(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, | 68 | private static native int solveIlpProblem(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, |
69 | int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, | 69 | int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, |
70 | double[] output, double timeoutSeconds, boolean silent); | 70 | double[] output, boolean lpRelaxation, double timeoutSeconds, boolean silent); |
71 | } | 71 | } |
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) { |