diff options
7 files changed, 240 insertions, 99 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) { |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend index a51aa082..b22e2a20 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend | |||
@@ -7,11 +7,19 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr | |||
7 | import org.junit.Test | 7 | import org.junit.Test |
8 | 8 | ||
9 | import static org.junit.Assert.* | 9 | import static org.junit.Assert.* |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint | ||
10 | 11 | ||
11 | class CbcPolyhedronSolverTest extends IntegerPolyhedronSolverTest { | 12 | class CbcPolyhedronSolverTest extends IntegerPolyhedronSolverTest { |
12 | 13 | ||
13 | override protected createSolver() { | 14 | override protected createSolver() { |
14 | new CbcPolyhedronSolver(10, true) | 15 | new CbcPolyhedronSolver(false, 10, true) |
16 | } | ||
17 | } | ||
18 | |||
19 | class RelaxedCbcPolyhedronSolverTest extends RelaxedPolyhedronSolverTest { | ||
20 | |||
21 | override protected createSolver() { | ||
22 | new CbcPolyhedronSolver(true, 10, true) | ||
15 | } | 23 | } |
16 | } | 24 | } |
17 | 25 | ||
@@ -19,9 +27,9 @@ class CbcPolyhedronSolverTimeoutTest { | |||
19 | 27 | ||
20 | @Test | 28 | @Test |
21 | def void timeoutTest() { | 29 | def void timeoutTest() { |
22 | val solver = new CbcPolyhedronSolver(0, true) | 30 | val solver = new CbcPolyhedronSolver(false, 0, true) |
23 | val x = new Dimension("x", 0, 1) | 31 | val x = new Dimension("x", 0, 1) |
24 | val polyhedron = new Polyhedron(#[x], #[], #[x]) | 32 | val polyhedron = new Polyhedron(#[x], #[new LinearConstraint(#{x -> 1}, null, 0)], #[x]) |
25 | val operator = solver.createSaturationOperator(polyhedron) | 33 | val operator = solver.createSaturationOperator(polyhedron) |
26 | try { | 34 | try { |
27 | val result = operator.saturate | 35 | val result = operator.saturate |
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend index 1b2dcb00..47534618 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend | |||
@@ -80,26 +80,52 @@ abstract class PolyhedronSolverTest { | |||
80 | 80 | ||
81 | @Test | 81 | @Test |
82 | def void singleDimensionUnboundedFromAboveTest() { | 82 | def void singleDimensionUnboundedFromAboveTest() { |
83 | val x = new Dimension("x", 0, null) | 83 | val x = new Dimension("x", -2, null) |
84 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | 84 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) |
85 | 85 | ||
86 | val result = saturate() | 86 | val result = saturate() |
87 | 87 | ||
88 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | 88 | assertEquals(PolyhedronSaturationResult.SATURATED, result) |
89 | assertEquals(0, x.lowerBound) | 89 | assertEquals(-2, x.lowerBound) |
90 | assertEquals(null, x.upperBound) | 90 | assertEquals(null, x.upperBound) |
91 | } | 91 | } |
92 | 92 | ||
93 | @Test | 93 | @Test |
94 | def void singleDimensionUnboundedFromBelowTest() { | 94 | def void singleDimensionUnboundedFromBelowTest() { |
95 | val x = new Dimension("x", null, 0) | 95 | val x = new Dimension("x", null, 2) |
96 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | 96 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) |
97 | 97 | ||
98 | val result = saturate() | 98 | val result = saturate() |
99 | 99 | ||
100 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | 100 | assertEquals(PolyhedronSaturationResult.SATURATED, result) |
101 | assertEquals(null, x.lowerBound) | 101 | assertEquals(null, x.lowerBound) |
102 | assertEquals(0, x.upperBound) | 102 | assertEquals(2, x.upperBound) |
103 | } | ||
104 | |||
105 | @Test | ||
106 | def void singleDimensionUnboundedTest() { | ||
107 | val x = new Dimension("x", null, null) | ||
108 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
109 | |||
110 | val result = saturate() | ||
111 | |||
112 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
113 | assertEquals(null, x.lowerBound) | ||
114 | assertEquals(null, x.upperBound) | ||
115 | } | ||
116 | |||
117 | @Test | ||
118 | def void singleDimensionUnboundedObjectiveTest() { | ||
119 | val x = new Dimension("x", null, null) | ||
120 | val y = new Dimension("y", 0, 1) | ||
121 | val objective = new LinearConstraint(#{x -> 1, y -> 1}, null, null) | ||
122 | createSaturationOperator(new Polyhedron(#[x, y], #[], #[objective])) | ||
123 | |||
124 | val result = saturate() | ||
125 | |||
126 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
127 | assertEquals(null, objective.lowerBound) | ||
128 | assertEquals(null, objective.upperBound) | ||
103 | } | 129 | } |
104 | 130 | ||
105 | @Test | 131 | @Test |
@@ -174,6 +200,25 @@ abstract class PolyhedronSolverTest { | |||
174 | 200 | ||
175 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | 201 | assertEquals(PolyhedronSaturationResult.EMPTY, result) |
176 | } | 202 | } |
203 | |||
204 | @Test | ||
205 | def void unboundedRelaxationWithIntegerSolutionTest() { | ||
206 | val x = new Dimension("x", 1, 3) | ||
207 | val y = new Dimension("y", null, null) | ||
208 | createSaturationOperator(new Polyhedron( | ||
209 | #[x, y], | ||
210 | #[new LinearConstraint(#{x -> 2}, 2, 6)], | ||
211 | #[x, y] | ||
212 | )) | ||
213 | |||
214 | val result = saturate() | ||
215 | |||
216 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
217 | assertEquals(1, x.lowerBound) | ||
218 | assertEquals(3, x.upperBound) | ||
219 | assertEquals(null, y.lowerBound) | ||
220 | assertEquals(null, y.upperBound) | ||
221 | } | ||
177 | 222 | ||
178 | protected def createSaturationOperator(Polyhedron polyhedron) { | 223 | protected def createSaturationOperator(Polyhedron polyhedron) { |
179 | destroyOperatorIfExists() | 224 | destroyOperatorIfExists() |
@@ -228,7 +273,7 @@ abstract class IntegerPolyhedronSolverTest extends PolyhedronSolverTest { | |||
228 | @Test | 273 | @Test |
229 | def void unboundedRelaxationWithNoIntegerSolutionTest() { | 274 | def void unboundedRelaxationWithNoIntegerSolutionTest() { |
230 | val x = new Dimension("x", 0, 1) | 275 | val x = new Dimension("x", 0, 1) |
231 | val y = new Dimension("y", 0, null) | 276 | val y = new Dimension("y", null, null) |
232 | createSaturationOperator(new Polyhedron( | 277 | createSaturationOperator(new Polyhedron( |
233 | #[x, y], | 278 | #[x, y], |
234 | #[new LinearConstraint(#{x -> 2}, 1, 1)], | 279 | #[new LinearConstraint(#{x -> 2}, 1, 1)], |
@@ -282,21 +327,59 @@ abstract class RelaxedPolyhedronSolverTest extends PolyhedronSolverTest { | |||
282 | } | 327 | } |
283 | 328 | ||
284 | @Test | 329 | @Test |
285 | def void unboundedRelaxationWithNoIntegerSolutionTest() { | 330 | def void unboundedRelaxationWithNoIntegerSolutionUnconstrainedVariableTest() { |
286 | val x = new Dimension("x", 0, 1) | 331 | val x = new Dimension("x", 1, 2) |
287 | val y = new Dimension("y", 0, null) | 332 | val y = new Dimension("y", null, null) |
288 | createSaturationOperator(new Polyhedron( | 333 | createSaturationOperator(new Polyhedron( |
289 | #[x, y], | 334 | #[x, y], |
290 | #[new LinearConstraint(#{x -> 2}, 1, 1)], | 335 | #[new LinearConstraint(#{x -> 2}, 3, 3)], |
291 | #[x, y] | 336 | #[x, y] |
292 | )) | 337 | )) |
293 | 338 | ||
294 | val result = saturate() | 339 | val result = saturate() |
295 | 340 | ||
296 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | 341 | assertEquals(PolyhedronSaturationResult.SATURATED, result) |
297 | assertEquals(0, x.lowerBound) | 342 | assertEquals(1, x.lowerBound) |
298 | assertEquals(1, x.upperBound) | 343 | assertEquals(2, x.upperBound) |
299 | assertEquals(0, y.lowerBound) | 344 | assertEquals(null, y.lowerBound) |
300 | assertEquals(null, y.upperBound) | 345 | assertEquals(null, y.upperBound) |
301 | } | 346 | } |
347 | |||
348 | @Test | ||
349 | def void unboundedRelaxationWithNoIntegerSolutionConstrainedVariableTest() { | ||
350 | val x = new Dimension("x", 1, 2) | ||
351 | val y = new Dimension("y", null, null) | ||
352 | createSaturationOperator(new Polyhedron( | ||
353 | #[x, y], | ||
354 | #[new LinearConstraint(#{x -> 2}, 3, 3), new LinearConstraint(#{y -> 1}, null, 1)], | ||
355 | #[x, y] | ||
356 | )) | ||
357 | |||
358 | val result = saturate() | ||
359 | |||
360 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
361 | assertEquals(1, x.lowerBound) | ||
362 | assertEquals(2, x.upperBound) | ||
363 | assertEquals(null, y.lowerBound) | ||
364 | assertEquals(1, y.upperBound) | ||
365 | } | ||
366 | |||
367 | @Test | ||
368 | def void unboundedRelaxationWithNoIntegerSolutionBoundedVariableTest() { | ||
369 | val x = new Dimension("x", 1, 2) | ||
370 | val y = new Dimension("y", null, 1) | ||
371 | createSaturationOperator(new Polyhedron( | ||
372 | #[x, y], | ||
373 | #[new LinearConstraint(#{x -> 2}, 3, 3)], | ||
374 | #[x, y] | ||
375 | )) | ||
376 | |||
377 | val result = saturate() | ||
378 | |||
379 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
380 | assertEquals(1, x.lowerBound) | ||
381 | assertEquals(2, x.upperBound) | ||
382 | assertEquals(null, y.lowerBound) | ||
383 | assertEquals(1, y.upperBound) | ||
384 | } | ||
302 | } | 385 | } |