Skip to content

math_spec.boundedness

Provably unbounded models, named by check instead of by the solver.

A variable that is unbounded on the side its objective term improves toward and appears in no constraint runs to infinity for any data at all — nothing in the model can stop it. A solver answers that with a bare unbounded, naming nothing; check says it with the variable, the side and the reason (#229).

Advice rather than a refusal, because the same shape is what a half-written model looks like — a variable declared before the constraint that will hold it — and no door should close on one. Which means these notes reach a caller who runs check, and nobody else: straight to solve and the solver's answer is still the first word.

The rule is a conjunction and needs both halves. A variable unbounded on the improving side but constrained somewhere is ordinary — the constraint is what bounds it, and "every variable must be defined by a constraint" would reject most working models. A variable in no constraint but bounded on the improving side is ordinary too; its own bounds: are what bound it.

Which side improves is read off the sign the variable enters the objective with, not off the sense alone: under minimize a +v term runs down toward lower and a -v term runs up toward upper. Where that sign is not decidable without data — a parameter coefficient, which may be zero, or occurrences of both signs, which may cancel — nothing is claimed. A false note here would read as a defect in a model that solves, which is worse than saying nothing.

Only the whole-variable case is decidable here. A variable whose slice gets no constraint row, because the mask that would have defined it is false in this data, is the same finding one step later, and the row tables at the end of a build are what would answer it.

Sign = Literal['+', '-'] | None module-attribute #

unbounded_notes(schema) #

Name every variable the objective can drive to infinity unopposed.

Takes an expanded schema: a piecewise: block holds the variables it names, and does so through the constraints it expands into.

RETURNS DESCRIPTION
list[str]

One note per variable that is unbounded on the side its objective term
list[str]

improves toward and named by no constraint — what check warns with,
list[str]

empty for a model this cannot prove anything about.
Source code in src/math_spec/boundedness.py 
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
def unbounded_notes(schema: Model) -> list[str]:
    """Name every variable the objective can drive to infinity unopposed.

    Takes an expanded schema: a ``piecewise:`` block holds the variables it
    names, and does so through the constraints it expands into.

    Returns:
        One note per variable that is unbounded on the side its objective term
        improves toward and named by no constraint — what ``check`` warns with,
        empty for a model this cannot prove anything about.
    """
    if schema.objective is None:
        return []

    ns = Namespace.of(schema)
    objective = expression_of(schema.objective.expression, schema, ns, 'The objective')
    assert not isinstance(objective, ComparisonNode), 'an objective holds no comparison — checked before this runs'

    constrained = {block.variable for block in schema.sos.values()}
    for cname, cdef in schema.constraints.items():
        constrained |= _variables(expression_of(cdef.expression, schema, ns, f"Constraint '{cname}'"))

    signs: dict[str, Sign] = {}
    _walk(objective, '+', signs)

    minimize = schema.objective.sense == 'minimize'
    notes = []
    for vname, sign in signs.items():
        if sign is None or vname in constrained:
            continue
        side = 'lower' if minimize == (sign == '+') else 'upper'
        if _is_open(schema.variables[vname], side):
            notes.append(
                f"Variable '{vname}' makes this model unbounded: no constraint names it, and "
                f'bounds.{side} is {_OPEN[side]}, which is the direction a {sign}{vname} term '
                f'improves a {schema.objective.sense} objective in. No data can change that, so '
                f'the solve would answer `unbounded` and name nothing.\n'
                f'Give it a finite bounds.{side}, or the constraint that was meant to define it.'
            )
    return notes