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 --- .../viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | 6 +++++- .../logic2viatra/cardinality/RelationConstraintCalculator.xtend | 2 ++ 2 files changed, 7 insertions(+), 1 deletion(-) (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 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 } -- cgit v1.2.3-54-g00ecf