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 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (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 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 -- cgit v1.2.3-54-g00ecf