discopt.decomposition.ir.certificate

discopt.decomposition.ir.certificate#

Soundness certificates and variable mappings for reformulations.

The correctness spine of the reformulation IR (design §8.2). A SoundnessCertificate records why a decomposition represents the original model — exactly, as a relaxation, or property-dependent — and refuses outright to run a method that carries no guarantee (HEURISTIC). A VariableMapping records which original variables live in the master versus which subproblem block, so results come back in the user’s variable space and the partition is inspectable.

The certificate is advisory, not the contract. is_sound() admits RELAXATION and UNKNOWN (only HEURISTIC is refused), so the authority on whether a run actually certified optimality is the driver’s returned SolveResult (status / bound / gap_certified), which self-polices: GBD withholds its bound unless a convexity classifier proves the recourse convex, and Lagrangian certifies only when a recovered primal meets the dual bound. SoundnessCertificate.check_result() turns that division of labour into a checked post-condition — after DecomposedModel.solve() it raises if a merely-RELAXATION/UNKNOWN certificate returns gap_certified=True without the finite dual bound that a real proof leaves behind (the only way a non-self-policing future driver could smuggle an unearned certificate past the gate), and it reports the driver’s gap_certified as the authoritative signal so a GBD UNKNOWN certificate that the driver resolved to exact no longer disagrees with the run.

Classes#

VariableMapping

Original-variable ↔ (master | subproblem-block) mapping.

SoundnessCertificate

Why a reformulation is (or is not) a faithful stand-in for the monolith.

Module Contents#

class discopt.decomposition.ir.certificate.VariableMapping#

Original-variable ↔ (master | subproblem-block) mapping.

Variables:

  • master_vars (tuple[str, ...]) – Variables held in the coordinating master (complicating vars for Benders; empty for Lagrangian / independent-block decompositions).

  • block_of_var (dict[str, int]) – Subproblem block id per variable; -1 for a master variable.

  • num_blocks (int) – Number of subproblem blocks.

master_vars: tuple[str, ...]#
block_of_var: dict[str, int]#
num_blocks: int#
role(var: str) → str#

Human label for a variable’s role: "master" or "block{i}".

class discopt.decomposition.ir.certificate.SoundnessCertificate#

Why a reformulation is (or is not) a faithful stand-in for the monolith.

Variables:

  • method (MethodKind) – The decomposition method certified.

  • level (Soundness) – PROVEN_EQUIVALENT (same optimum), RELAXATION (valid bound), UNKNOWN (property-dependent, e.g. GBD needs convexity), or HEURISTIC (no guarantee).

  • rationale (str) – One-line justification.

  • caveats (tuple[str, ...]) – Conditions the guarantee depends on.

method: discopt.decomposition.advisor.types.MethodKind#
level: discopt.decomposition.advisor.types.Soundness#
rationale: str#
caveats: tuple[str, ...] = ()#
is_sound() → bool#

True unless the certificate is merely heuristic.

A relaxation (valid bound) and an unknown-but-not-refuted certificate are both allowed to run; only a purely heuristic reformulation is refused by default (correctness-first, design goal #1).

assert_sound() → None#

Raise ValueError if the reformulation is unsound to run.

check_result(result) → None#

Post-condition: the driver’s result must not out-claim this cert.

is_sound() is deliberately permissive (RELAXATION / UNKNOWN are allowed to run), so the driver — not this certificate — is the authority on whether a run certified optimality. This method enforces the contract that ties the two together: a static RELAXATION / UNKNOWN certificate is allowed to return gap_certified=True only when the driver actually proved it, and the proof always leaves a finite dual ``bound`` behind (a valid lower bound for a min-sense problem). A gap_certified=True with no finite bound from such a certificate would be an unearned certificate — exactly what a future driver that failed to self-police would produce — so we raise rather than let it pass.

SolveResult.__post_init__ already downgrades gap_certified when the bound is absent/non-finite for a non-infeasible status; this is the decomposition-layer backstop that also refuses the case (status="infeasible") that guard exempts, keeping the certificate a real checked post-condition rather than documentation.

Raises:

AssertionError – If the result claims a certified gap the certificate cannot justify.

effective_level(result) → discopt.decomposition.advisor.types.Soundness#

Authoritative soundness for result, driver-first (#391 item 1).

The stored level is the static estimate made before the solve; the driver may resolve it. In particular GBD attaches an UNKNOWN certificate but, when its convexity gate proves the recourse convex, returns gap_certified=True — a genuinely exact run. Surfacing the driver’s verdict avoids the user-facing disagreement where the run certified optimality yet the attached certificate still reads UNKNOWN. Never upgrades past what the driver proved: a certified gap upgrades a permissive certificate to PROVEN_EQUIVALENT; otherwise the static level stands.

summary() → str#

One-line human-readable certificate.