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 --- .../cardinality/CbcPolyhedronSolver.xtend | 36 ++++++++++------------ 1 file changed, 17 insertions(+), 19 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 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 - } } -- cgit v1.2.3-54-g00ecf