Polyhedron solver SAT fix and initial scope filtering

2 files changed, 7 insertions, 1 deletions

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
         }