From b217dfc7e7bd7beb73c8cc23ad82383309ceb697 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 18 Jul 2019 15:21:56 +0200 Subject: Implement Coin-OR CBC polyhedron saturation operator --- .../cardinality/CbcPolyhedronSolver.xtend | 182 +++++++++++++++++++++ 1 file changed, 182 insertions(+) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend') 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 new file mode 100644 index 00000000..1f6d4e8f --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend @@ -0,0 +1,182 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.collect.ImmutableMap +import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult +import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +@FinalFieldsConstructor +class CbcPolyhedronSolver implements PolyhedronSolver { + val double timeoutSeconds + val boolean silent + + new() { + this(10, true) + } + + override createSaturationOperator(Polyhedron polyhedron) { + new CbcSaturationOperator(polyhedron, timeoutSeconds, silent) + } +} + +class CbcSaturationOperator implements PolyhedronSaturationOperator { + @Accessors val Polyhedron polyhedron + val double timeoutSeconds + val boolean silent + val double[] columnLowerBounds + val double[] columnUpperBounds + val double[] objective + val Map dimensionsToIndicesMap + + new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { + this.polyhedron = polyhedron + this.timeoutSeconds = timeoutSeconds + this.silent = silent + val numDimensions = polyhedron.dimensions.size + columnLowerBounds = newDoubleArrayOfSize(numDimensions) + columnUpperBounds = newDoubleArrayOfSize(numDimensions) + objective = newDoubleArrayOfSize(numDimensions) + dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) + } + + override saturate() { + val numDimensions = polyhedron.dimensions.size + for (var int j = 0; j < numDimensions; j++) { + val dimension = polyhedron.dimensions.get(j) + columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) + columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) + } + val numConstraints = polyhedron.constraints.size + val rowStarts = newIntArrayOfSize(numConstraints + 1) + val rowLowerBounds = newDoubleArrayOfSize(numConstraints) + val rowUpperBounds = newDoubleArrayOfSize(numConstraints) + val numEntries = polyhedron.constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 + rowStarts.set(numConstraints, numEntries) + val columnIndices = newIntArrayOfSize(numEntries) + val entries = newDoubleArrayOfSize(numEntries) + var int index = 0 + for (var int i = 0; i < numConstraints; i++) { + rowStarts.set(i, index) + val constraint = polyhedron.constraints.get(i) + rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) + rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) + if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { + throw new IllegalArgumentException("Constrains has unknown dimensions") + } + for (var int j = 0; j < numDimensions; j++) { + val dimension = polyhedron.dimensions.get(j) + val coefficient = constraint.coefficients.get(dimension) + if (coefficient !== null && coefficient != 0) { + columnIndices.set(index, j) + entries.set(index, coefficient) + index++ + } + } + } + if (index != numEntries) { + throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") + } + for (expressionToSaturate : polyhedron.expressionsToSaturate) { + for (var int j = 0; j < numDimensions; j++) { + objective.set(j, 0) + } + switch (expressionToSaturate) { + Dimension: { + val j = getIndex(expressionToSaturate) + objective.set(j, 1) + } + LinearConstraint: { + for (pair : expressionToSaturate.coefficients.entrySet) { + val j = getIndex(pair.key) + objective.set(j, pair.value) + } + } + default: + throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) + } + val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, + entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) + switch (minimizationResult) { + CbcResult.SolutionBounded: { + val value = Math.floor(minimizationResult.value) + expressionToSaturate.lowerBound = value as int + setBound(expressionToSaturate, value, columnLowerBounds, rowLowerBounds) + } + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.lowerBound = null + setBound(expressionToSaturate, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) + } + case CbcResult.UNSAT: + return PolyhedronSaturationResult.EMPTY + case CbcResult.ABANDONED, + case CbcResult.TIMEOUT: + return PolyhedronSaturationResult.UNKNOWN + default: + throw new RuntimeException("Unknown CbcResult: " + minimizationResult) + } + for (var int j = 0; j < numDimensions; j++) { + val objectiveCoefficient = objective.get(j) + objective.set(j, -objectiveCoefficient) + } + val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, + entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) + switch (maximizationResult) { + CbcResult.SolutionBounded: { + val value = Math.ceil(-maximizationResult.value) + expressionToSaturate.upperBound = value as int + setBound(expressionToSaturate, value, columnUpperBounds, rowUpperBounds) + } + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.upperBound = null + setBound(expressionToSaturate, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) + } + case CbcResult.UNSAT: + throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") + case CbcResult.ABANDONED, + case CbcResult.TIMEOUT: + return PolyhedronSaturationResult.UNKNOWN + default: + throw new RuntimeException("Unknown CbcResult: " + maximizationResult) + } + } + PolyhedronSaturationResult.SATURATED + } + + private def toDouble(Integer nullableInt, double defaultValue) { + if (nullableInt === null) { + defaultValue + } else { + nullableInt.doubleValue + } + } + + private def int getIndex(Dimension dimension) { + val index = dimensionsToIndicesMap.get(dimension) + if (index === null) { + throw new IllegalArgumentException("Unknown dimension: " + dimension) + } + index + } + + private def void setBound(LinearBoundedExpression expression, double bound, double[] columnBounds, + double[] rowBounds) { + switch (expression) { + Dimension: { + val j = getIndex(expression) + columnBounds.set(j, bound) + } + LinearConstraint: { + val i = polyhedron.constraints.indexOf(expression) + if (i >= 0) { + rowBounds.set(i, bound) + } + } + } + } + + override close() throws Exception { + // Nothing to close + } +} -- cgit v1.2.3-70-g09d2 From 52a015c1558b9ce5fb10f27d41e508dfec1e79d6 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 25 Jul 2019 19:03:01 +0200 Subject: Make polyhedron solvers more robust --- .../AbstractPolyhedronSaturationOperator.xtend | 53 ++++++++++++++++++++++ .../cardinality/CbcPolyhedronSolver.xtend | 36 +++++++-------- .../cardinality/PolyhedronScopePropagator.xtend | 4 +- .../cardinality/Z3PolyhedronSolver.xtend | 17 +++---- 4 files changed, 81 insertions(+), 29 deletions(-) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend') 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 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.collect.ImmutableList +import org.eclipse.xtend.lib.annotations.Accessors + +abstract class AbstractPolyhedronSaturationOperator implements PolyhedronSaturationOperator { + @Accessors val Polyhedron polyhedron + + new(Polyhedron polyhedron) { + if (polyhedron.dimensions.empty) { + throw new IllegalArgumentException("Polyhedron must have at least one dimension.") + } + this.polyhedron = polyhedron + } + + override saturate() { + if (polyhedron.expressionsToSaturate.empty) { + return PolyhedronSaturationResult.SATURATED + } + for (constraint : polyhedron.constraints) { + if (constraint.zero) { + if (constraint.lowerBound !== null && constraint.lowerBound > 0) { + return PolyhedronSaturationResult.EMPTY + } + if (constraint.upperBound !== null && constraint.upperBound < 0) { + return PolyhedronSaturationResult.EMPTY + } + } else { + if (constraint.lowerBound !== null && constraint.upperBound !== null && + constraint.upperBound < constraint.lowerBound) { + return PolyhedronSaturationResult.EMPTY + } + } + } + doSaturate() + } + + protected def PolyhedronSaturationResult doSaturate() + + protected def getNonTrivialConstraints() { + ImmutableList.copyOf(polyhedron.constraints.filter [ constraint | + (constraint.lowerBound !== null || constraint.upperBound !== null) && !constraint.zero + ]) + } + + private static def isZero(LinearConstraint constraint) { + constraint.coefficients.values.forall[it == 0] + } + + override close() throws Exception { + // Nothing to close by default. + } +} 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 import com.google.common.collect.ImmutableMap import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver +import java.util.List import java.util.Map -import org.eclipse.xtend.lib.annotations.Accessors import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor @FinalFieldsConstructor @@ -21,8 +21,7 @@ class CbcPolyhedronSolver implements PolyhedronSolver { } } -class CbcSaturationOperator implements PolyhedronSaturationOperator { - @Accessors val Polyhedron polyhedron +class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { val double timeoutSeconds val boolean silent val double[] columnLowerBounds @@ -31,7 +30,7 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { val Map dimensionsToIndicesMap new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { - this.polyhedron = polyhedron + super(polyhedron) this.timeoutSeconds = timeoutSeconds this.silent = silent val numDimensions = polyhedron.dimensions.size @@ -41,25 +40,26 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) } - override saturate() { + override doSaturate() { val numDimensions = polyhedron.dimensions.size for (var int j = 0; j < numDimensions; j++) { val dimension = polyhedron.dimensions.get(j) columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) } - val numConstraints = polyhedron.constraints.size + val constraints = nonTrivialConstraints + val numConstraints = constraints.size val rowStarts = newIntArrayOfSize(numConstraints + 1) val rowLowerBounds = newDoubleArrayOfSize(numConstraints) val rowUpperBounds = newDoubleArrayOfSize(numConstraints) - val numEntries = polyhedron.constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 + val numEntries = constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 rowStarts.set(numConstraints, numEntries) val columnIndices = newIntArrayOfSize(numEntries) val entries = newDoubleArrayOfSize(numEntries) var int index = 0 for (var int i = 0; i < numConstraints; i++) { rowStarts.set(i, index) - val constraint = polyhedron.constraints.get(i) + val constraint = constraints.get(i) rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { @@ -102,11 +102,12 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { CbcResult.SolutionBounded: { val value = Math.floor(minimizationResult.value) expressionToSaturate.lowerBound = value as int - setBound(expressionToSaturate, value, columnLowerBounds, rowLowerBounds) + setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) } case CbcResult.SOLUTION_UNBOUNDED: { expressionToSaturate.lowerBound = null - setBound(expressionToSaturate, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) + setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, + rowLowerBounds) } case CbcResult.UNSAT: return PolyhedronSaturationResult.EMPTY @@ -126,11 +127,12 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { CbcResult.SolutionBounded: { val value = Math.ceil(-maximizationResult.value) expressionToSaturate.upperBound = value as int - setBound(expressionToSaturate, value, columnUpperBounds, rowUpperBounds) + setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) } case CbcResult.SOLUTION_UNBOUNDED: { expressionToSaturate.upperBound = null - setBound(expressionToSaturate, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) + setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, + rowUpperBounds) } case CbcResult.UNSAT: throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") @@ -160,23 +162,19 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator { index } - private def void setBound(LinearBoundedExpression expression, double bound, double[] columnBounds, - double[] rowBounds) { + private def void setBound(LinearBoundedExpression expression, List constraints, double bound, + double[] columnBounds, double[] rowBounds) { switch (expression) { Dimension: { val j = getIndex(expression) columnBounds.set(j, bound) } LinearConstraint: { - val i = polyhedron.constraints.indexOf(expression) + val i = constraints.indexOf(expression) if (i >= 0) { rowBounds.set(i, bound) } } } } - - override close() throws Exception { - // Nothing to close - } } 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 { override void propagateAllScopeConstraints() { resetBounds() populatePolyhedronFromScope() - println(polyhedron) +// println(polyhedron) val result = operator.saturate() if (result == PolyhedronSaturationResult.EMPTY) { throw new IllegalStateException("Scope bounds cannot be satisfied") @@ -71,7 +71,7 @@ class PolyhedronScopePropagator extends ScopePropagator { super.propagateAllScopeConstraints() } } - println(polyhedron) +// println(polyhedron) } 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 import com.microsoft.z3.Status import com.microsoft.z3.Symbol import java.util.Map -import org.eclipse.xtend.lib.annotations.Accessors import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor class Z3PolyhedronSolver implements PolyhedronSolver { @@ -27,21 +26,20 @@ class Z3PolyhedronSolver implements PolyhedronSolver { } } -class Z3SaturationOperator implements PolyhedronSaturationOperator { +class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { static val INFINITY_SYMBOL_NAME = "oo" static val MULT_SYMBOL_NAME = "*" extension val Context context val Symbol infinitySymbol val Symbol multSymbol - @Accessors val Polyhedron polyhedron val Map variables new(Polyhedron polyhedron, boolean lpRelaxation) { + super(polyhedron) context = new Context infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) - this.polyhedron = polyhedron variables = polyhedron.dimensions.toInvertedMap [ dimension | val name = dimension.name if (lpRelaxation) { @@ -52,8 +50,8 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { ] } - override saturate() { - val status = doSaturate() + override doSaturate() { + val status = executeSolver() convertStatusToSaturationResult(status) } @@ -70,7 +68,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { } } - private def doSaturate() { + private def executeSolver() { for (expressionToSaturate : polyhedron.expressionsToSaturate) { val expr = expressionToSaturate.toExpr val lowerResult = saturateLowerBound(expr, expressionToSaturate) @@ -147,7 +145,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { for (pair : variables.entrySet) { assertBounds(pair.value, pair.key) } - for (constraint : polyhedron.constraints) { + for (constraint : nonTrivialConstraints) { val expr = createLinearCombination(constraint.coefficients) assertBounds(expr, constraint) } @@ -181,6 +179,9 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator { private def createLinearCombination(Map coefficients) { val size = coefficients.size + if (size == 0) { + return mkInt(0) + } val array = newArrayOfSize(size) var int i = 0 for (pair : coefficients.entrySet) { -- cgit v1.2.3-70-g09d2 From b4bf8d387e430600790f6b30d9e88ec785148cd7 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 29 Jul 2019 14:21:36 +0200 Subject: Make CbcPolyhedronSolver more robust --- .../cpp/viatracbc.cpp | 54 +++++--- .../cpp/viatracbc.hpp | 2 +- .../lib/libviatracbc.so | Bin 38248 -> 33944 bytes .../bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java | 8 +- .../cardinality/CbcPolyhedronSolver.xtend | 154 +++++++++++++-------- .../cardinality/CbcPolyhedronSolverTest.xtend | 14 +- .../tests/cardinality/PolyhedronSolverTest.xtend | 107 ++++++++++++-- 7 files changed, 240 insertions(+), 99 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend') 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; static CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriedArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, - jdoubleArray objectiveArray); + jdoubleArray objectiveArray, jboolean lpRelaxation); static void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, - jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build); + jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, jboolean lpRelaxation, + CoinModel &build); static void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, CoinModel &build); @@ -83,11 +84,11 @@ jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, - jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent) { + jdoubleArray outputArray, jboolean lpRelaxation, jdouble timeoutSeconds, jboolean silent) { try { auto build = CreateModel(env, columnLowerBoundsArray, columnUpperBoundsArray, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, - objectiveArray); + objectiveArray, lpRelaxation); double value; jint result = SolveModel(build, timeoutSeconds, silent, value); if (result == kCbcSolutionBounded) { @@ -106,16 +107,18 @@ jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, - jdoubleArray objectiveArray) { + jdoubleArray objectiveArray, jboolean lpRelaxation) { CoinModel build; - CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, build); + CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, + lpRelaxation, build); CreateModelRows(env, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, build); return build; } void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, - jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build) { + jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, jboolean lpRelaxation, + CoinModel &build) { int numColumns = env->GetArrayLength(columnLowerBoundsArray); PinnedDoubleArray columnLowerBounds{env, columnLowerBoundsArray}; PinnedDoubleArray columnUpperBounds{env, columnUpperBoundsArray}; @@ -123,7 +126,9 @@ void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, for (int i = 0; i < numColumns; i++) { build.setColumnBounds(i, columnLowerBounds[i], columnUpperBounds[i]); build.setObjective(i, objective[i]); - build.setInteger(i); + if (!lpRelaxation) { + build.setInteger(i); + } } } @@ -215,6 +220,9 @@ jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdoub if (model.isInitialSolveProvenPrimalInfeasible()) { return kCbcUnsat; } + if (model.isInitialSolveProvenDualInfeasible()) { + return kCbcSolutionUnbounded; + } if (model.isInitialSolveAbandoned()) { return kCbcTimeout; } @@ -226,20 +234,26 @@ jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdoub model.branchAndBound(); - if (model.isProvenInfeasible()) { - return kCbcUnsat; - } - if (model.isProvenDualInfeasible()) { - return kCbcSolutionUnbounded; - } - if (model.isProvenOptimal()) { - value = model.getMinimizationObjValue(); - return kCbcSolutionBounded; - } - if (model.maximumSecondsReached()) { + switch (model.status()) { + case 0: + if (model.isProvenInfeasible()) { + return kCbcUnsat; + } + if (model.isProvenDualInfeasible()) { + return kCbcSolutionUnbounded; + } + if (model.isProvenOptimal()) { + value = model.getMinimizationObjValue(); + return kCbcSolutionBounded; + } + throw std::runtime_error("CBC status is 0, but no solution is found"); + case 1: return kCbcTimeout; + case 2: + return kCbcAbandoned; + default: + throw std::runtime_error("Unknown CBC status"); } - return kCbcAbandoned; } 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 JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, - jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent); + jdoubleArray outputArray, jboolean lpRelaxation, jdouble timeoutSeconds, jboolean silent); } 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 Binary files a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so 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 { } public static CbcResult solve(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, - int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, - double[] objective, double timeoutSeconds, boolean silent) { + int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, + boolean lpRelaxation, double timeoutSeconds, boolean silent) { loadNatives(); validate(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, rowLowerBounds, rowUpperBounds, objective); double[] output = new double[1]; int result = solveIlpProblem(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, - rowLowerBounds, rowUpperBounds, objective, output, timeoutSeconds, silent); + rowLowerBounds, rowUpperBounds, objective, output, lpRelaxation, timeoutSeconds, silent); if (result == CBC_SOLUTION_BOUNDED) { return new CbcResult.SolutionBounded(output[0]); } else if (result == CBC_SOLUTION_UNBOUNDED) { @@ -67,5 +67,5 @@ public class CbcSolver { private static native int solveIlpProblem(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, - double[] output, double timeoutSeconds, boolean silent); + double[] output, boolean lpRelaxation, double timeoutSeconds, boolean silent); } 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 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality +import com.google.common.collect.ImmutableList import com.google.common.collect.ImmutableMap import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver +import java.util.HashSet import java.util.List import java.util.Map +import java.util.Set import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor @FinalFieldsConstructor class CbcPolyhedronSolver implements PolyhedronSolver { + val boolean lpRelaxation val double timeoutSeconds val boolean silent new() { - this(10, true) + this(false, -1, true) } override createSaturationOperator(Polyhedron polyhedron) { - new CbcSaturationOperator(polyhedron, timeoutSeconds, silent) + new CbcSaturationOperator(polyhedron, lpRelaxation, timeoutSeconds, silent) } } class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { + val boolean lpRelaxation val double timeoutSeconds val boolean silent val double[] columnLowerBounds @@ -29,8 +34,9 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { val double[] objective val Map dimensionsToIndicesMap - new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { + new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds, boolean silent) { super(polyhedron) + this.lpRelaxation = lpRelaxation this.timeoutSeconds = timeoutSeconds this.silent = silent val numDimensions = polyhedron.dimensions.size @@ -56,6 +62,12 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { rowStarts.set(numConstraints, numEntries) val columnIndices = newIntArrayOfSize(numEntries) val entries = newDoubleArrayOfSize(numEntries) + val unconstrainedDimensions = new HashSet + for (dimension : polyhedron.dimensions) { + if (dimension.lowerBound === null && dimension.upperBound === null) { + unconstrainedDimensions += dimension + } + } var int index = 0 for (var int i = 0; i < numConstraints; i++) { rowStarts.set(i, index) @@ -69,6 +81,7 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { val dimension = polyhedron.dimensions.get(j) val coefficient = constraint.coefficients.get(dimension) if (coefficient !== null && coefficient != 0) { + unconstrainedDimensions -= dimension columnIndices.set(index, j) entries.set(index, coefficient) index++ @@ -79,71 +92,94 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") } for (expressionToSaturate : polyhedron.expressionsToSaturate) { - for (var int j = 0; j < numDimensions; j++) { - objective.set(j, 0) + val result = saturate(expressionToSaturate, rowStarts, columnIndices, entries, rowLowerBounds, + rowUpperBounds, unconstrainedDimensions, constraints) + if (result != PolyhedronSaturationResult.SATURATED) { + return result } - switch (expressionToSaturate) { - Dimension: { - val j = getIndex(expressionToSaturate) - objective.set(j, 1) + } + PolyhedronSaturationResult.SATURATED + } + + protected def saturate(LinearBoundedExpression expressionToSaturate, int[] rowStarts, int[] columnIndices, + double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, Set unconstrainedDimensions, + ImmutableList constraints) { + val numDimensions = objective.size + for (var int j = 0; j < numDimensions; j++) { + objective.set(j, 0) + } + switch (expressionToSaturate) { + Dimension: { + // CBC will return nonsensical results or call free() with invalid arguments if + // it is passed a fully unconstrained (-Inf lower and +Int upper bound, no inequalities) variable + // in the objective function. + if (unconstrainedDimensions.contains(expressionToSaturate)) { + return PolyhedronSaturationResult.SATURATED } - LinearConstraint: { - for (pair : expressionToSaturate.coefficients.entrySet) { - val j = getIndex(pair.key) - objective.set(j, pair.value) + val j = getIndex(expressionToSaturate) + objective.set(j, 1) + } + LinearConstraint: { + for (pair : expressionToSaturate.coefficients.entrySet) { + val dimension = pair.key + // We also have to check for unconstrained dimensions here to avoid crashing. + if (unconstrainedDimensions.contains(dimension)) { + expressionToSaturate.lowerBound = null + expressionToSaturate.upperBound = null + return PolyhedronSaturationResult.SATURATED } + val j = getIndex(dimension) + objective.set(j, pair.value) } - default: - throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) } - val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, - entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) - switch (minimizationResult) { - CbcResult.SolutionBounded: { - val value = Math.floor(minimizationResult.value) - expressionToSaturate.lowerBound = value as int - setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) - } - case CbcResult.SOLUTION_UNBOUNDED: { - expressionToSaturate.lowerBound = null - setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, - rowLowerBounds) - } - case CbcResult.UNSAT: - return PolyhedronSaturationResult.EMPTY - case CbcResult.ABANDONED, - case CbcResult.TIMEOUT: - return PolyhedronSaturationResult.UNKNOWN - default: - throw new RuntimeException("Unknown CbcResult: " + minimizationResult) + default: + throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) + } + val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, + entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) + switch (minimizationResult) { + CbcResult.SolutionBounded: { + val value = Math.floor(minimizationResult.value) + expressionToSaturate.lowerBound = value as int + setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) } - for (var int j = 0; j < numDimensions; j++) { - val objectiveCoefficient = objective.get(j) - objective.set(j, -objectiveCoefficient) + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.lowerBound = null + setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) } - val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, - entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) - switch (maximizationResult) { - CbcResult.SolutionBounded: { - val value = Math.ceil(-maximizationResult.value) - expressionToSaturate.upperBound = value as int - setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) - } - case CbcResult.SOLUTION_UNBOUNDED: { - expressionToSaturate.upperBound = null - setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, - rowUpperBounds) - } - case CbcResult.UNSAT: - throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") - case CbcResult.ABANDONED, - case CbcResult.TIMEOUT: - return PolyhedronSaturationResult.UNKNOWN - default: - throw new RuntimeException("Unknown CbcResult: " + maximizationResult) + case CbcResult.UNSAT: + return PolyhedronSaturationResult.EMPTY + case CbcResult.ABANDONED, + case CbcResult.TIMEOUT: + return PolyhedronSaturationResult.UNKNOWN + default: + throw new RuntimeException("Unknown CbcResult: " + minimizationResult) + } + for (var int j = 0; j < numDimensions; j++) { + val objectiveCoefficient = objective.get(j) + objective.set(j, -objectiveCoefficient) + } + val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, + entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) + switch (maximizationResult) { + CbcResult.SolutionBounded: { + val value = Math.ceil(-maximizationResult.value) + expressionToSaturate.upperBound = value as int + setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) } + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.upperBound = null + setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) + } + case CbcResult.UNSAT: + throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") + case CbcResult.ABANDONED, + case CbcResult.TIMEOUT: + return PolyhedronSaturationResult.UNKNOWN + default: + throw new RuntimeException("Unknown CbcResult: " + maximizationResult) } - PolyhedronSaturationResult.SATURATED + return PolyhedronSaturationResult.SATURATED } 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 import org.junit.Test import static org.junit.Assert.* +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint class CbcPolyhedronSolverTest extends IntegerPolyhedronSolverTest { override protected createSolver() { - new CbcPolyhedronSolver(10, true) + new CbcPolyhedronSolver(false, 10, true) + } +} + +class RelaxedCbcPolyhedronSolverTest extends RelaxedPolyhedronSolverTest { + + override protected createSolver() { + new CbcPolyhedronSolver(true, 10, true) } } @@ -19,9 +27,9 @@ class CbcPolyhedronSolverTimeoutTest { @Test def void timeoutTest() { - val solver = new CbcPolyhedronSolver(0, true) + val solver = new CbcPolyhedronSolver(false, 0, true) val x = new Dimension("x", 0, 1) - val polyhedron = new Polyhedron(#[x], #[], #[x]) + val polyhedron = new Polyhedron(#[x], #[new LinearConstraint(#{x -> 1}, null, 0)], #[x]) val operator = solver.createSaturationOperator(polyhedron) try { 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 { @Test def void singleDimensionUnboundedFromAboveTest() { - val x = new Dimension("x", 0, null) + val x = new Dimension("x", -2, null) createSaturationOperator(new Polyhedron(#[x], #[], #[x])) val result = saturate() assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) + assertEquals(-2, x.lowerBound) assertEquals(null, x.upperBound) } @Test def void singleDimensionUnboundedFromBelowTest() { - val x = new Dimension("x", null, 0) + val x = new Dimension("x", null, 2) createSaturationOperator(new Polyhedron(#[x], #[], #[x])) val result = saturate() assertEquals(PolyhedronSaturationResult.SATURATED, result) assertEquals(null, x.lowerBound) - assertEquals(0, x.upperBound) + assertEquals(2, x.upperBound) + } + + @Test + def void singleDimensionUnboundedTest() { + val x = new Dimension("x", null, null) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(null, x.lowerBound) + assertEquals(null, x.upperBound) + } + + @Test + def void singleDimensionUnboundedObjectiveTest() { + val x = new Dimension("x", null, null) + val y = new Dimension("y", 0, 1) + val objective = new LinearConstraint(#{x -> 1, y -> 1}, null, null) + createSaturationOperator(new Polyhedron(#[x, y], #[], #[objective])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(null, objective.lowerBound) + assertEquals(null, objective.upperBound) } @Test @@ -174,6 +200,25 @@ abstract class PolyhedronSolverTest { assertEquals(PolyhedronSaturationResult.EMPTY, result) } + + @Test + def void unboundedRelaxationWithIntegerSolutionTest() { + val x = new Dimension("x", 1, 3) + val y = new Dimension("y", null, null) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 2, 6)], + #[x, y] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(3, x.upperBound) + assertEquals(null, y.lowerBound) + assertEquals(null, y.upperBound) + } protected def createSaturationOperator(Polyhedron polyhedron) { destroyOperatorIfExists() @@ -228,7 +273,7 @@ abstract class IntegerPolyhedronSolverTest extends PolyhedronSolverTest { @Test def void unboundedRelaxationWithNoIntegerSolutionTest() { val x = new Dimension("x", 0, 1) - val y = new Dimension("y", 0, null) + val y = new Dimension("y", null, null) createSaturationOperator(new Polyhedron( #[x, y], #[new LinearConstraint(#{x -> 2}, 1, 1)], @@ -282,21 +327,59 @@ abstract class RelaxedPolyhedronSolverTest extends PolyhedronSolverTest { } @Test - def void unboundedRelaxationWithNoIntegerSolutionTest() { - val x = new Dimension("x", 0, 1) - val y = new Dimension("y", 0, null) + def void unboundedRelaxationWithNoIntegerSolutionUnconstrainedVariableTest() { + val x = new Dimension("x", 1, 2) + val y = new Dimension("y", null, null) createSaturationOperator(new Polyhedron( #[x, y], - #[new LinearConstraint(#{x -> 2}, 1, 1)], + #[new LinearConstraint(#{x -> 2}, 3, 3)], #[x, y] )) val result = saturate() assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) - assertEquals(1, x.upperBound) - assertEquals(0, y.lowerBound) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + assertEquals(null, y.lowerBound) assertEquals(null, y.upperBound) } + + @Test + def void unboundedRelaxationWithNoIntegerSolutionConstrainedVariableTest() { + val x = new Dimension("x", 1, 2) + val y = new Dimension("y", null, null) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 3, 3), new LinearConstraint(#{y -> 1}, null, 1)], + #[x, y] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + assertEquals(null, y.lowerBound) + assertEquals(1, y.upperBound) + } + + @Test + def void unboundedRelaxationWithNoIntegerSolutionBoundedVariableTest() { + val x = new Dimension("x", 1, 2) + val y = new Dimension("y", null, 1) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 3, 3)], + #[x, y] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + assertEquals(null, y.lowerBound) + assertEquals(1, y.upperBound) + } } -- cgit v1.2.3-70-g09d2 From 07664df29b4aa491597ca76c31556a746ae95635 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 2 Aug 2019 01:26:19 +0200 Subject: Handle floating point rounding errors in Cbc --- .../cardinality/CbcPolyhedronSolver.xtend | 35 +++++++++++++++++----- 1 file changed, 28 insertions(+), 7 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend') 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 4bd46fbf..c772aebc 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 @@ -26,6 +26,8 @@ class CbcPolyhedronSolver implements PolyhedronSolver { } class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { + static val EPSILON = 1e-6 + val boolean lpRelaxation val double timeoutSeconds val boolean silent @@ -139,12 +141,21 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) switch (minimizationResult) { CbcResult.SolutionBounded: { - val value = Math.floor(minimizationResult.value) - expressionToSaturate.lowerBound = value as int - setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) + val doubleValue = minimizationResult.value + val roundedValue = Math.floor(doubleValue) + val intValue = roundedValue as int + val oldBound = expressionToSaturate.lowerBound + if (oldBound === null || intValue > oldBound) { + expressionToSaturate.lowerBound = intValue + setBound(expressionToSaturate, constraints, roundedValue, columnLowerBounds, rowLowerBounds) + } else if (oldBound - doubleValue > EPSILON) { + throw new IllegalStateException("Unexpected decrease of lower bound by " + (oldBound - doubleValue)) + } } case CbcResult.SOLUTION_UNBOUNDED: { - expressionToSaturate.lowerBound = null + if (expressionToSaturate.lowerBound !== null) { + throw new IllegalStateException("Finite lower bound became infinite") + } setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) } case CbcResult.UNSAT: @@ -163,11 +174,21 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) switch (maximizationResult) { CbcResult.SolutionBounded: { - val value = Math.ceil(-maximizationResult.value) - expressionToSaturate.upperBound = value as int - setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) + val doubleValue = -maximizationResult.value + val roundedValue = Math.ceil(doubleValue) + val intValue = roundedValue as int + val oldBound = expressionToSaturate.upperBound + if (oldBound === null || intValue < oldBound) { + expressionToSaturate.upperBound = intValue + setBound(expressionToSaturate, constraints, roundedValue, columnUpperBounds, rowUpperBounds) + } else if (doubleValue - oldBound > EPSILON) { + throw new IllegalStateException("Unexpected increase of upper bound by " + (doubleValue - oldBound)) + } } case CbcResult.SOLUTION_UNBOUNDED: { + if (expressionToSaturate.lowerBound !== null) { + throw new IllegalStateException("Finite upper bound became infinite") + } expressionToSaturate.upperBound = null setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) } -- cgit v1.2.3-70-g09d2 From 15fafc1b66a38e362f4aca49a8848d080f760310 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 2 Aug 2019 19:04:40 +0200 Subject: Be more lenient with rounding IP solver results --- .../logic2viatra/cardinality/CbcPolyhedronSolver.xtend | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend') 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 c772aebc..75c396b4 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 @@ -142,13 +142,13 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { switch (minimizationResult) { CbcResult.SolutionBounded: { val doubleValue = minimizationResult.value - val roundedValue = Math.floor(doubleValue) + val roundedValue = Math.ceil(doubleValue - EPSILON) val intValue = roundedValue as int val oldBound = expressionToSaturate.lowerBound - if (oldBound === null || intValue > oldBound) { + if (oldBound === null || intValue >= oldBound) { expressionToSaturate.lowerBound = intValue setBound(expressionToSaturate, constraints, roundedValue, columnLowerBounds, rowLowerBounds) - } else if (oldBound - doubleValue > EPSILON) { + } else { throw new IllegalStateException("Unexpected decrease of lower bound by " + (oldBound - doubleValue)) } } @@ -175,13 +175,13 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { switch (maximizationResult) { CbcResult.SolutionBounded: { val doubleValue = -maximizationResult.value - val roundedValue = Math.ceil(doubleValue) + val roundedValue = Math.floor(doubleValue + EPSILON) val intValue = roundedValue as int val oldBound = expressionToSaturate.upperBound - if (oldBound === null || intValue < oldBound) { + if (oldBound === null || intValue <= oldBound) { expressionToSaturate.upperBound = intValue setBound(expressionToSaturate, constraints, roundedValue, columnUpperBounds, rowUpperBounds) - } else if (doubleValue - oldBound > EPSILON) { + } else { throw new IllegalStateException("Unexpected increase of upper bound by " + (doubleValue - oldBound)) } } -- cgit v1.2.3-70-g09d2 From 6dca5681757fef7d65ffa051ff59ba8332c74a83 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 29 Oct 2019 17:33:15 +0100 Subject: Polyhedron solver SAT fix and initial scope filtering --- .../cardinality/CbcPolyhedronSolver.xtend | 6 +++++- .../cardinality/RelationConstraintCalculator.xtend | 2 ++ .../InstanceModel2PartialInterpretation.xtend | 23 +++++++++++++++++----- 3 files changed, 25 insertions(+), 6 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend') 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 75c396b4..708f93dc 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 @@ -193,7 +193,11 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) } case CbcResult.UNSAT: - throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") + if (lpRelaxation) { + return PolyhedronSaturationResult.EMPTY + } else { + throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") + } case CbcResult.ABANDONED, case CbcResult.TIMEOUT: return PolyhedronSaturationResult.UNKNOWN diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend index c92260ea..3e4fea8a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend @@ -44,6 +44,8 @@ class RelationMultiplicityConstraint { } def constrainsUnrepairable() { + // TODO Optimize the unrepairable matches computation, + // or come up with a heuristic when does computing unrepairables worth the overhead. constrainsUnfinished && canHaveMultipleSourcesPerTarget && false } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend index 8aaaacb5..cb5b587f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic +import com.google.common.collect.ImmutableList import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput @@ -12,18 +13,18 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.Par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.Problem2PartialInterpretationTrace import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory +import java.math.BigDecimal import java.util.HashMap +import java.util.HashSet import java.util.List import java.util.Map +import java.util.Set import org.eclipse.emf.common.util.Enumerator +import org.eclipse.emf.ecore.EAttribute import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.resource.Resource import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import java.util.HashSet -import java.util.Set -import java.math.BigDecimal -import org.eclipse.emf.ecore.EAttribute class InstanceModel2PartialInterpretation { val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE @@ -36,7 +37,19 @@ class InstanceModel2PartialInterpretation { Resource resource, boolean withID) { - val objects = resource.allContents.toList + val objectsBuilder = ImmutableList.builder + val treeIterator = resource.allContents + val referencesUsed = ecore2Logic.allReferencesInScope(metamodelTranslationResult.trace).toSet + while (treeIterator.hasNext) { + val object = treeIterator.next + val containingReference = object.eContainmentFeature + if (containingReference === null || referencesUsed.contains(containingReference)) { + objectsBuilder.add(object) + } else { + treeIterator.prune + } + } + val objects = objectsBuilder.build return transform(metamodelTranslationResult,objects,withID) } -- cgit v1.2.3-70-g09d2