`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.
pathpathlib.Path: Resolved absolute path to this pair’s directory.
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.
parameter_mapParameterMap: The loaded map.json, which states how each parameter of b is computed from the parameters of a.

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[73]  # 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

gen_map_py()[source]¶

Generate a Python script computing b’s parameters from a’s.

The script is generated from the python code snippets of this pair’s map.json. The resulting script takes the path to a’s parameters.json and the path to write b’s as positional arguments.

Examples

Generate the parameter-map script for the a to b pair of p1 | Amusement Park Ticket Machines, whose parameters are a renaming:

>>> from formulation_bench import Dataset
>>> ds = Dataset("dataset")
>>> reform = ds.reformulations[0]  # corresponds to p1.a -> p1.b
>>> script = reform.gen_map_py()
>>> print(script)
import argparse
import json


def main(params_path: str, output_path: str) -> None:
    with open(params_path, "r") as f:
        data = json.load(f)

    # Source Parameters
    CashMachineProcessingRate = data["CashMachineProcessingRate"]
    ...
    # Parameter Map
    A = CashMachineProcessingRate
    ...

run_map(input_path=None, output_path=None)[source]¶

Write this pair’s map.py and run it.

The script generated by gen_map_py() is written to map.py in the pair’s directory, then applied to a’s parameters to produce b’s.

Parameters:

input_pathstr or pathlib.Path, optional: Path to a parameters.json holding formulation a’s parameters. Defaults to parameters.json in a’s formulation directory.
output_pathstr or pathlib.Path, optional: Path to write the mapped parameters. Defaults to parameters.json in this pair’s directory.

Examples

Map formulation a’s parameters to formulation b’s for p1 | Amusement Park Ticket Machines:

>>> import json
>>> from formulation_bench import Dataset
>>> ds = Dataset("dataset")
>>> reform = ds.reformulations[0]  # corresponds to p1.a -> p1.b

>>> reform.a.run_gen_params()
>>> params = json.load(open(reform.a.path / "parameters.json"))
>>> params["CashMachineProcessingRate"]  # a's parameter
20

>>> reform.run_map()
>>> params = json.load(open(reform.path / "parameters.json"))
>>> params["A"]  # b's name for "CashMachineProcessingRate"
20

class formulation_bench.models.ParameterMap(parameters, definitions, metadata)[source]¶

A mapping from one formulation’s parameters to another’s.

Loaded from the map.json of a reformulation pair. See map.json for the file schema.

Attributes:

parametersdict[str, Expression]: One entry per parameter of the target formulation, computing it from the source formulation’s parameters: An entry may reference any parameter defined before it.
definitionsdict[str, Expression]: Optional intermediate quantities computed before the parameters. Used when several parameters share a derivation.
metadatadict[str, Any]: Free-form metadata about the map. Typically a notes field.

render_markdown()[source]¶

Render this parameter map in Markdown.

The output is produced by rendering the following Jinja template. The notes passed to this template are the metadata.notes of the map.

# Parameter Map

{% for note in notes %}
{{ note }}

{% endfor %}
{% if definitions %}
## Definitions

{% for name, d in definitions.items() %}
- **{{ name }}**
$${{ d.formulation }}$$
{% endfor %}

{% endif %}
## Parameters

{% for name, d in parameters.items() %}
- **{{ name }}**
$${{ d.formulation }}$$
{% endfor %}

Returns:

markdownstr: The rendered Markdown string.

Examples

Render the map carrying formulation a of p12 | Traveling Salesman Problem (TSP) to formulation b:

>>> from formulation_bench import Dataset
>>> ds = Dataset("dataset")
>>> pmap = ds.reformulations[73].parameter_map
>>> print(pmap.render_markdown())
# Parameter Map

Formulation `b` has the same parameters as formulation `a`; the map is the identity.

## Parameters

- **n**
$$n = n$$
- **c**
$$c_{ij} = c_{ij}$$

Reformulation¶

`Reformulation`¶