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