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-54-g00ecf