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/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc | |
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/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc')
4 files changed, 39 insertions, 25 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 | } |