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 --- .../cardinality/CbcPolyhedronSolver.xtend | 154 +++++++++++++-------- 1 file changed, 95 insertions(+), 59 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner') 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) { -- cgit v1.2.3-54-g00ecf