From cd96a9a4f54d45cda3ddf5df474946445d557090 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 3 Sep 2023 17:57:38 +0200 Subject: feat: scope propagator in language --- .../store/reasoning/scope/internal/MultiView.java | 23 ++++++++++++++++ .../scope/internal/ScopePropagatorAdapterImpl.java | 7 +++-- .../scope/internal/ScopePropagatorBuilderImpl.java | 18 ++----------- .../store/reasoning/scope/MPSolverTest.java | 31 ++++++++++++++++++++++ 4 files changed, 59 insertions(+), 20 deletions(-) create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/MultiView.java (limited to 'subprojects/store-reasoning-scope/src') diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/MultiView.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/MultiView.java new file mode 100644 index 00000000..cea4e07d --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/MultiView.java @@ -0,0 +1,23 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope.internal; + +import tools.refinery.store.query.view.TuplePreservingView; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.cardinality.CardinalityInterval; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +import tools.refinery.store.tuple.Tuple; + +class MultiView extends TuplePreservingView { + protected MultiView(Symbol symbol) { + super(symbol, "multi"); + } + + @Override + protected boolean doFilter(Tuple key, CardinalityInterval value) { + return !CardinalityIntervals.ONE.equals(value); + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java index 0d594701..c257df6b 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java @@ -210,10 +210,9 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { UpperCardinality upperBound; switch (maximizationResult) { case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); - case UNBOUNDED -> upperBound = UpperCardinalities.UNBOUNDED; - case INFEASIBLE -> { - return RefinementResult.REJECTED; - } + // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is + // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 + case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" .formatted(variable, minimizationResult)); } diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java index f383ebeb..11ca7381 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java @@ -22,12 +22,6 @@ import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; import java.util.*; -import static tools.refinery.store.query.literal.Literals.not; -import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL; -import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; -import static tools.refinery.store.reasoning.literal.PartialLiterals.may; -import static tools.refinery.store.reasoning.literal.PartialLiterals.must; - public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder implements ScopePropagatorBuilder { private Symbol countSymbol = MultiObjectTranslator.COUNT_STORAGE; @@ -66,16 +60,8 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder builder - .clause( - may(EXISTS_SYMBOL.call(instance)), - not(must(EXISTS_SYMBOL.call(instance))) - ) - .clause( - may(EXISTS_SYMBOL.call(instance)), - not(must(EQUALS_SYMBOL.call(instance, instance))) - ) - ); + var multiQuery = Query.of("MULTI", (builder, instance) -> builder.clause( + new MultiView(countSymbol).call(instance))); typeScopePropagatorFactories = new ArrayList<>(scopes.size()); for (var entry : scopes.entrySet()) { var type = entry.getKey(); diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java index c9745d22..95c4ac68 100644 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MPSolverTest.java @@ -49,4 +49,35 @@ class MPSolverTest { assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); assertThat(objective.value(), closeTo(1, 0.01)); } + + @Test + void unboundedIsInfeasibleTest() { + var solver = MPSolver.createSolver("GLOP"); + var x = solver.makeNumVar(0, Double.POSITIVE_INFINITY, "x"); + var objective = solver.objective(); + objective.setCoefficient(x, 1); + + objective.setMinimization(); + assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); + assertThat(objective.value(), closeTo(0, 0.01)); + + objective.setMaximization(); + assertThat(solver.solve(), is(MPSolver.ResultStatus.INFEASIBLE)); + } + + @Test + void constantTest() { + var solver = MPSolver.createSolver("GLOP"); + var x = solver.makeNumVar(1, 1, "x"); + var objective = solver.objective(); + objective.setCoefficient(x, 1); + + objective.setMinimization(); + assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); + assertThat(objective.value(), closeTo(1, 0.01)); + + objective.setMaximization(); + assertThat(solver.solve(), is(MPSolver.ResultStatus.OPTIMAL)); + assertThat(objective.value(), closeTo(1, 0.01)); + } } -- cgit v1.2.3-70-g09d2