`Reformulation`¶

class formulation_bench.reformulation.Reformulation(a, b, is_reformulation)[source]¶

A pair of MILP formulations with a reformulation label.

Consists of two MILP formulations a and b and a boolean is_reformulation label indicating whether b is a reformulation of a. The formal definition of reformulation is given in Reformulation. Positive entries (is_reformulation=True) are accompanied by a Lean 4 proof whose path is accessible via the lean_proof_path attribute; negative entries have no proof and lean_proof_path resolves to None.

Attributes:

aFormulation: The base formulation.
bFormulation: The reformulation candidate.
is_reformulationbool: True iff b is a reformulation of a.
lean_proof_pathpathlib.Path or None: For positive entries, the path to the accompanying Lean 4 proof file. For negative entries, None since no proof exists.

Examples

Formulation b of p12 | Traveling Salesman Problem (TSP) is a reformulation of formulation a:

>>> from formulation_bench import Dataset
>>> ds = Dataset("dataset")
>>> reform = ds.reformulations[80]  # corresponds to p12.a -> p12.b
>>> reform.a.problem.name
'Traveling Salesman Problem (TSP)'
>>> reform.b.problem.name
'Traveling Salesman Problem (TSP)'
>>> reform.b.constraints[-1].description  # cutting plane added by p12.b
'Depot-Exit Position Bound (EC1)...'
>>> reform.is_reformulation
True

Reformulation¶

`Reformulation`¶