stormvogel.teaching.lp¶

Classes¶

`LP`	LP formulation for MDP reachability, as sympy expressions.
`LPSolution`	Exact rational solution to an LP returned by `solve_lp()`.

Functions¶

`_expr_to_z3`(→ Any)
`_constraint_to_z3`(→ Any)
`solve_lp`(→ LPSolution \| None)	Solve an LP using z3 (exact rational arithmetic).
`lp_prob`(→ LP)	Build the LP formulation for MDP reachability as sympy expressions.
`lp_dual_prob`(→ LP)	Occupancy-measure (dual) LP for single-objective reachability.
`lp_dual_maxreachprob`(→ LP)	Dual LP for maximum reachability probability to states labelled target_label.
`lp_maxreachprob`(→ LP)	LP for maximum reachability probability to states labelled target_label.
`lp_minreachprob`(→ LP)	LP for minimum reachability probability to states labelled target_label.
`extract_policy_from_dual_lp`(→ dict)	Extract a deterministic policy from an occupancy-measure (dual) LP solution.

Module Contents¶

class stormvogel.teaching.lp.LP¶

LP formulation for MDP reachability, as sympy expressions.

Renders as a formatted LP in Jupyter via _repr_latex_.

sense: str¶

objective: sympy.Expr¶

constraints: list[sympy.Basic] = []¶

_repr_latex_() → str¶

class stormvogel.teaching.lp.LPSolution¶

Exact rational solution to an LP returned by solve_lp().

Parameters:

objective – Optimal objective value.
values – Variable assignments, keyed by the sympy Symbol used in the LP.

objective: fractions.Fraction¶

values: dict[sympy.Symbol, fractions.Fraction]¶

stormvogel.teaching.lp._expr_to_z3(expr: sympy.Expr, var_map: dict[sympy.Symbol, Any]) → Any¶

stormvogel.teaching.lp._constraint_to_z3(c: sympy.Basic, var_map: dict[sympy.Symbol, Any]) → Any¶

stormvogel.teaching.lp.solve_lp(lp: LP) → LPSolution | None¶

Solve an LP using z3 (exact rational arithmetic).

Parameters:: lp – The LP to solve.
Returns:: Exact rational solution, or None if infeasible or unbounded.
Raises:: ImportError – If z3-solver is not installed.

stormvogel.teaching.lp.lp_prob(mdp: stormvogel.model.Model[float], min: bool, zero_states: Iterable[stormvogel.model.State], one_states: Iterable[stormvogel.model.State]) → LP¶

Build the LP formulation for MDP reachability as sympy expressions.

Parameters:

mdp – The stormvogel MDP.
min – True for min-reachability (maximize), False for max-reachability (minimize).
zero_states – States fixed at value 0.
one_states – States fixed at value 1 (target states).

Returns:

LP with objective and constraints as sympy expressions.

stormvogel.teaching.lp.lp_dual_prob(mdp: stormvogel.model.Model[float], zero_states: Iterable[stormvogel.model.State], one_states: Iterable[stormvogel.model.State]) → LP¶: Occupancy-measure (dual) LP for single-objective reachability.

stormvogel.teaching.lp.lp_dual_maxreachprob(mdp: stormvogel.model.Model[float], target_label: str) → LP¶: Dual LP for maximum reachability probability to states labelled target_label.

stormvogel.teaching.lp.lp_maxreachprob(mdp: stormvogel.model.Model[float], target_label: str) → LP¶: LP for maximum reachability probability to states labelled target_label.

stormvogel.teaching.lp.lp_minreachprob(mdp: stormvogel.model.Model[float], target_label: str) → LP¶: LP for minimum reachability probability to states labelled target_label.

stormvogel.teaching.lp.extract_policy_from_dual_lp(mdp: stormvogel.model.Model[float], sol: LPSolution) → dict¶

Extract a deterministic policy from an occupancy-measure (dual) LP solution.

The dual LP variables y_{s,a} represent expected visit counts for each state-action pair under the optimal policy. For each state the action with the largest y value is chosen. States that are unreachable under the optimal policy (all y values zero or absent in sol) receive the first available non-empty action as a default; the choice does not affect the objective value.

Parameters:

mdp – The MDP for which the dual LP was built.
sol – Solution returned by solve_lp().

Returns:

Dict mapping each state with at least one non-empty action to its chosen Action.