diff options
author | 2019-07-25 19:03:01 +0200 | |
---|---|---|
committer | 2019-07-25 19:04:58 +0200 | |
commit | 52a015c1558b9ce5fb10f27d41e508dfec1e79d6 (patch) | |
tree | a0868c35b857c82eec8641e6dfcb07f2c9859dc5 | |
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
4 files changed, 81 insertions, 29 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend new file mode 100644 index 00000000..94f97e94 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend | |||
@@ -0,0 +1,53 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import org.eclipse.xtend.lib.annotations.Accessors | ||
5 | |||
6 | abstract class AbstractPolyhedronSaturationOperator implements PolyhedronSaturationOperator { | ||
7 | @Accessors val Polyhedron polyhedron | ||
8 | |||
9 | new(Polyhedron polyhedron) { | ||
10 | if (polyhedron.dimensions.empty) { | ||
11 | throw new IllegalArgumentException("Polyhedron must have at least one dimension.") | ||
12 | } | ||
13 | this.polyhedron = polyhedron | ||
14 | } | ||
15 | |||
16 | override saturate() { | ||
17 | if (polyhedron.expressionsToSaturate.empty) { | ||
18 | return PolyhedronSaturationResult.SATURATED | ||
19 | } | ||
20 | for (constraint : polyhedron.constraints) { | ||
21 | if (constraint.zero) { | ||
22 | if (constraint.lowerBound !== null && constraint.lowerBound > 0) { | ||
23 | return PolyhedronSaturationResult.EMPTY | ||
24 | } | ||
25 | if (constraint.upperBound !== null && constraint.upperBound < 0) { | ||
26 | return PolyhedronSaturationResult.EMPTY | ||
27 | } | ||
28 | } else { | ||
29 | if (constraint.lowerBound !== null && constraint.upperBound !== null && | ||
30 | constraint.upperBound < constraint.lowerBound) { | ||
31 | return PolyhedronSaturationResult.EMPTY | ||
32 | } | ||
33 | } | ||
34 | } | ||
35 | doSaturate() | ||
36 | } | ||
37 | |||
38 | protected def PolyhedronSaturationResult doSaturate() | ||
39 | |||
40 | protected def getNonTrivialConstraints() { | ||
41 | ImmutableList.copyOf(polyhedron.constraints.filter [ constraint | | ||
42 | (constraint.lowerBound !== null || constraint.upperBound !== null) && !constraint.zero | ||
43 | ]) | ||
44 | } | ||
45 | |||
46 | private static def isZero(LinearConstraint constraint) { | ||
47 | constraint.coefficients.values.forall[it == 0] | ||
48 | } | ||
49 | |||
50 | override close() throws Exception { | ||
51 | // Nothing to close by default. | ||
52 | } | ||
53 | } | ||
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 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index ce357272..3fd50071 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -61,7 +61,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
61 | override void propagateAllScopeConstraints() { | 61 | override void propagateAllScopeConstraints() { |
62 | resetBounds() | 62 | resetBounds() |
63 | populatePolyhedronFromScope() | 63 | populatePolyhedronFromScope() |
64 | println(polyhedron) | 64 | // println(polyhedron) |
65 | val result = operator.saturate() | 65 | val result = operator.saturate() |
66 | if (result == PolyhedronSaturationResult.EMPTY) { | 66 | if (result == PolyhedronSaturationResult.EMPTY) { |
67 | throw new IllegalStateException("Scope bounds cannot be satisfied") | 67 | throw new IllegalStateException("Scope bounds cannot be satisfied") |
@@ -71,7 +71,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
71 | super.propagateAllScopeConstraints() | 71 | super.propagateAllScopeConstraints() |
72 | } | 72 | } |
73 | } | 73 | } |
74 | println(polyhedron) | 74 | // println(polyhedron) |
75 | } | 75 | } |
76 | 76 | ||
77 | def resetBounds() { | 77 | def resetBounds() { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend index f1a84f2d..c8759a46 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -8,7 +8,6 @@ import com.microsoft.z3.Optimize | |||
8 | import com.microsoft.z3.Status | 8 | import com.microsoft.z3.Status |
9 | import com.microsoft.z3.Symbol | 9 | import com.microsoft.z3.Symbol |
10 | import java.util.Map | 10 | import java.util.Map |
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 11 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
13 | 12 | ||
14 | class Z3PolyhedronSolver implements PolyhedronSolver { | 13 | class Z3PolyhedronSolver implements PolyhedronSolver { |
@@ -27,21 +26,20 @@ class Z3PolyhedronSolver implements PolyhedronSolver { | |||
27 | } | 26 | } |
28 | } | 27 | } |
29 | 28 | ||
30 | class Z3SaturationOperator implements PolyhedronSaturationOperator { | 29 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { |
31 | static val INFINITY_SYMBOL_NAME = "oo" | 30 | static val INFINITY_SYMBOL_NAME = "oo" |
32 | static val MULT_SYMBOL_NAME = "*" | 31 | static val MULT_SYMBOL_NAME = "*" |
33 | 32 | ||
34 | extension val Context context | 33 | extension val Context context |
35 | val Symbol infinitySymbol | 34 | val Symbol infinitySymbol |
36 | val Symbol multSymbol | 35 | val Symbol multSymbol |
37 | @Accessors val Polyhedron polyhedron | ||
38 | val Map<Dimension, ArithExpr> variables | 36 | val Map<Dimension, ArithExpr> variables |
39 | 37 | ||
40 | new(Polyhedron polyhedron, boolean lpRelaxation) { | 38 | new(Polyhedron polyhedron, boolean lpRelaxation) { |
39 | super(polyhedron) | ||
41 | context = new Context | 40 | context = new Context |
42 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) | 41 | infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) |
43 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) | 42 | multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) |
44 | this.polyhedron = polyhedron | ||
45 | variables = polyhedron.dimensions.toInvertedMap [ dimension | | 43 | variables = polyhedron.dimensions.toInvertedMap [ dimension | |
46 | val name = dimension.name | 44 | val name = dimension.name |
47 | if (lpRelaxation) { | 45 | if (lpRelaxation) { |
@@ -52,8 +50,8 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
52 | ] | 50 | ] |
53 | } | 51 | } |
54 | 52 | ||
55 | override saturate() { | 53 | override doSaturate() { |
56 | val status = doSaturate() | 54 | val status = executeSolver() |
57 | convertStatusToSaturationResult(status) | 55 | convertStatusToSaturationResult(status) |
58 | } | 56 | } |
59 | 57 | ||
@@ -70,7 +68,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
70 | } | 68 | } |
71 | } | 69 | } |
72 | 70 | ||
73 | private def doSaturate() { | 71 | private def executeSolver() { |
74 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | 72 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { |
75 | val expr = expressionToSaturate.toExpr | 73 | val expr = expressionToSaturate.toExpr |
76 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) | 74 | val lowerResult = saturateLowerBound(expr, expressionToSaturate) |
@@ -147,7 +145,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
147 | for (pair : variables.entrySet) { | 145 | for (pair : variables.entrySet) { |
148 | assertBounds(pair.value, pair.key) | 146 | assertBounds(pair.value, pair.key) |
149 | } | 147 | } |
150 | for (constraint : polyhedron.constraints) { | 148 | for (constraint : nonTrivialConstraints) { |
151 | val expr = createLinearCombination(constraint.coefficients) | 149 | val expr = createLinearCombination(constraint.coefficients) |
152 | assertBounds(expr, constraint) | 150 | assertBounds(expr, constraint) |
153 | } | 151 | } |
@@ -181,6 +179,9 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { | |||
181 | 179 | ||
182 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { | 180 | private def createLinearCombination(Map<Dimension, Integer> coefficients) { |
183 | val size = coefficients.size | 181 | val size = coefficients.size |
182 | if (size == 0) { | ||
183 | return mkInt(0) | ||
184 | } | ||
184 | val array = newArrayOfSize(size) | 185 | val array = newArrayOfSize(size) |
185 | var int i = 0 | 186 | var int i = 0 |
186 | for (pair : coefficients.entrySet) { | 187 | for (pair : coefficients.entrySet) { |