formulation-bench-v0.5.0

NP-hardness. Problems expose whether they are NP-hard, and the default dataset moves
to dataset-v0.4.0, which is now the oldest release the package can read.

API

• Problem.np_hard reports whether the underlying optimization problem is NP-hard
  — a property of the problem itself, not of any one formulation of it. It parallels
  Formulation.valid: a semantic property users filter on belongs at the top level
  rather than in freeform metadata (46646aa).
• The np_hard key is required. The attribute is typed bool and the key is read
  directly, so a dataset release without it fails to load rather than yielding None
  and an "unknown" label downstream (176ff73).
• DEFAULT_DATASET_VERSION is dataset-v0.4.0. Every earlier dataset release
  predates np_hard and no longer loads, so this release requires the new dataset.
  Its p20 a → b pair is positive again, making the pair counts 63 positive and 26
  negative.

Docs

• Per-problem pages and the problems table report NP-hardness, schema.md documents
  the key, and the add-a-problem guide says how to set it (46646aa, 6ec1761).
• The problems table cites sources parenthetically; the author name adds nothing next
  to the problem name in a narrow column, while per-problem pages keep the textual
  form where the name reads as prose (1e52ded).

CI

• The dataset release workflow reads its notes from the tag annotation again.
  actions/checkout writes the pushed tag as a lightweight ref pointing at the
  commit, so %(contents:body) returned the commit message; the tags are re-fetched
  before it is read, mirroring what this workflow already did (e5909e1).

formulation-bench release at 17e603d.

dataset-v0.4.0

NP-hardness. Every problem now records whether its underlying optimization problem
is NP-hard, and the two problems that were not — p13 and p20 — were reworked until
they are. p20's a → b pair, marked negative in the last release, is positive again
with a complete proof.

NP-hardness

• problem.json carries a top-level np_hard boolean, promoted to a first-class
  Problem.np_hard attribute alongside Formulation.valid: a semantic property users
  filter on belongs at the top level rather than in freeform metadata. The six problems
  that are not NP-hard — p1, p4, p5, p7, p13, p20 — plus p2 (strongly) and p3 (only
  weakly) each explain the reasoning in a metadata.notes bullet (46646aa, 5ad8b01).
  The key is required, not optional: the schema check demands a real boolean, and the
  reader reads it directly rather than treating absence as "unclassified" (176ff73).
• p13 gains plane classes. With a single interchangeable fleet the flights aggregate
  into one commodity on a time-expanded flow network with node capacities, so the
  constraint matrix is totally unimodular and the problem is polynomial. The fleet is
  now partitioned into nK classes earning class-dependent rewards but sharing the
  location capacities, which makes it an integral multi-commodity flow problem: a large
  reward at one location in the first period and another in the last forces a class to
  fly between them, so two-commodity integral flow (Even, Itai & Shamir 1976) reduces
  to it. Both formulations gain a class index, b indexes planes within a class (a
  ragged nP[nK] dimension), and the recorded instance has a fractional LP relaxation
  (285.05 vs 284.2) with per-class capacities raising the optimum to 294.3, so the
  coupling binds (f2d1b38, b989c04, 9080c78).
• p20 gains capacitated hubs and integral shipments. The source describes
  transshipment points as capacity-limited but never models it, and lets shipments be
  continuous; without a shared resource the commodities decouple into shortest paths
  per camp plus an LP over the ration. A per-hub throughput capacity cap shared across
  commodities restores the coupling, and integrality makes it hard — the pair contains
  integral multi-commodity flow. b states the capacity over routes, where a path's or
  cycle's in-degree at a hub is its visit indicator, so it needs no new parameter. The
  recorded instance now holds camps of a few hundred people rather than tens of
  thousands, with capacities sized so the hubs jointly suffice but none alone does
  (3dcdf15, 28369d5).
• p20 assumes a directed supply graph: no arcs enter suppliers, none leave camps.
  This removes a's now-redundant source/sink flow constraints and b's
  transshipment-node restrictions on path and cycle validity (12fc189).

Dataset structure

• p20.b indexes simple directed cycles alongside supplier-to-camp paths. bf7bea9
  had marked b invalid because a feasible arc flow in a may circulate on a
  transshipment cycle and the path-based b had no variable to carry its cost. b now
  has a shipment variable y[c,k] per cycle, so the objectives match at every feasible
  point: b is valid again and the pair is positive. The parameter map gains the cycle
  enumeration (nC, cE, cCost) and the path cost c is renamed pCost (38bde8b).
• p20.b's cycle-completeness assumption is a real assertion, enumerating the simple
  directed cycles of (N, E) and checking each one's arc set is indexed by some
  c ∈ C. The graph assumptions make the unfiltered enumeration exactly the valid
  cycles, so no node-class filtering is needed (342bcef).
• formulation_id is used consistently across p13–p20. p15, p16, p18, and p20
  tagged their inefficient formulation's source with variation_id while their
  efficient counterparts used formulation_id (67135f1).
• p13's implicit assumptions are recorded in problem.json, matching p14–p20, and the
  nK, nA, nT ≥ 1 assumptions carried by the Lean Params are declared in both
  formulation JSONs (6d8d163).

20 problems, 109 formulations, 89 pairs — 63 positive, every one proved, and 26
negative. Sixteen of the twenty problems are NP-hard.

Bug fixes

• p13's total unimodularity claim was overstated; it is softened to
  polynomial-time solvability, and the direction of the paramMap doc comment is
  corrected (6d8d163).
• p20's formulation prose was stale: a's note still described F as continuous
  after shipments became integral, and b's note describing the cycle variables was
  garbled (f96df0e).
• Bibliography coverage missed notes. The citation checker only walked
  metadata.source, so a key cited solely by a {cite:t} role in a note was reported
  as uncited. Notes render through MyST like any other page content, so those roles are
  real citations (09daecd).

Proofs

• New: p20 a_b. Every feasible arc flow decomposes into simple supplier-to-camp
  paths plus transshipment cycles — extracted by bottleneck subtraction and strong
  induction on positive-support cardinality, including one-node self-loops — so the
  objectives agree pointwise (e523040, 38bde8b). The decomposition machinery moves from
  R to Z under integral shipments, which the bottleneck argument survives unchanged,
  and the throughput capacity transfers in both directions because the decomposition is
  an exact arc-wise identity (3dcdf15). The proof was then reworked around the reduced
  path/cycle predicates and cleaned up: duplicated degree lemmas consolidated, dead
  inverse-consistency and projection declarations removed, helpers made private
  (12fc189, 342bcef, cb3ec3b).
• p13 a_b runs the layered flow decomposition one class at a time; the helper
  lemmas were already generic in the plane count. The unused round-trip lemma is
  dropped (f2d1b38, 6d8d163).

Testing

• Every problem's np_hard is checked to be present and a real boolean, so the in-repo
  dataset cannot regress to an unclassified problem (46646aa).
• The parameter-map test no longer filters pairs on having a map.json: every pair has
  one, and Reformulation.parameter_map raises rather than returning None, so a
  missing file is a failure instead of a silently skipped pair (b17d9e0).
• Both p13 models now fit the size-limited license bundled with gurobipy, so CI covers
  p13.b as well (f2d1b38).

Docs

• Per-problem pages and the problems table both report NP-hardness; the table cites
  sources parenthetically since the author name adds nothing next to the problem name
  (46646aa, 1e52ded).

Dataset snapshot at eb811f4.

sha256: 44a7640d0dfb692c6d16291f169ec37aa952c0276f794cc949751016b71cb5ac

formulation-bench-v0.4.1

Make Reformulation.parameter_map non-optional. Every reformulation pair has a map.json, so returning None on a missing file only turned a dataset defect into a soft None downstream. Read the file directly and let it raise.

formulation-bench release at 7e2bcf8.

formulation-bench-v0.4.0

Its own repository, parameter maps, and a dataset test suite. The package moved out
of the FLARE monorepo, gained an API for the reformulation parameter maps that ship
with dataset-v0.3.0, and the two ad-hoc validation scripts became a marked pytest
suite that CI runs.

Standalone repository

• The package now lives in henryrobbins/formulation-bench. Extracted from
  packages/formulation_bench/ in the monorepo; download.py's REPO, the docs
  URLs, the Read the Docs config, and the Makefile all repoint here (140786e).
• CI, coverage, and releases run per-package. lefthook pre-commit hooks, a lint /
  format / typecheck / test workflow, Codecov, PyPI publish on formulation-bench-v*
  tags via trusted publishing, and a dataset tarball release on dataset-v* tags
  (e2f4a4b).
• The dataset is committed to this repo, and the docs build reads it directly.

API

• Reformulation exposes its parameter map. parameter_map loads the pair's
  map.json, gen_map_py() generates a script computing b's parameters from
  a's, and run_map() writes it beside the map and runs it. path gives the pair
  directory (c5da3bd, e7130c7).
• ParameterMap.render_markdown() mirrors Formulation.render_markdown(), for
  use in FLARE's prompts (54c3a22).
• Shapes are typed. Parameter.shape and Variable.shape become a Shape of
  Dimension objects classified by DimensionType (fixed, expression, ragged,
  cardinality), with is_scalar, is_ragged, has_cardinality, and resolve().
  Shape parsing lived in two places and now lives in Shape.parse (3ea75ea).
• Definition.description is required; map entries use the new Expression
  (code plus formulation), which has no description to give (ad444bc).
• lean_proof_path resolves to reformulations/pN/a_b/Reformulation.lean, following
  the dataset's move of proofs into the pair directory (bb1a173).
• download_dataset()'s undocumented sha256 argument is gone (53183b3), and it now
  defaults to dataset-v0.3.0.

Code generation

• Continuous and integer variables are free by default. _var_decl emitted only
  vtype=, so every non-binary variable inherited Gurobi's lb=0 and the generated
  solve.py was more constrained than the formulation it encodes. Binary keeps the
  solver default, where ub=1 really does follow from the type (49b9dfc, 6749ee5).
• run_gen_params() no longer sniffs each gen_params.py for an argparse data
  argument; all 109 scripts take the same two positional arguments (3ef810b).

Tests

• tests/dataset/ validates dataset content, tests/ validates the package. The
  two validation scripts became a marked pytest suite, kept out of make test and
  out of coverage; make test-dataset runs it (fbd99b5).
• Recorded solutions are re-solved with every variable pinned. A stored
  assignment can be infeasible while its objective is still optimal, which is how
  p12's MTZ positions went unnoticed. Formulations not stated over the recorded
  variables are filtered at collection rather than skipped (fbd99b5, 2a83fad).
• Schema validation over the dataset JSON, covering the defect classes the audit
  found by hand: declarations disagreeing with recorded data, shapes naming
  dimensions that do not exist, and snippets that never reach the generated
  solve.py (a4f0d3a).
• Structural checks on the Lean files --- namespace matching the path, the five
  declarations a MILPFormulation is built from, variable domains against the JSON,
  and the labelled pair and direction of each proof (53f4907).
• CI treats Gurobi's size-limit error as a skip, so the bundled license covers 14 of
  20 problems instead of gating the job (c5dae47). _codegen.py reaches 100% line
  coverage (b033b49).

Docs

• Installation, user guide, schema, and definitions pages rewritten: FLARE-specific
  guides now point at FLARE's docs, code examples are included by literalinclude,
  and the Lean pages are consolidated into a single definitions page (45d0330,
  3691b21, 45ecd0a).
• Citations are managed by sphinxcontrib-bibtex against docs/ref.bib (4de70bd).
• Every problem page gains a reformulations section: each pair's label, links to both
  formulations, and a table giving each parameter's definition in terms of the source
  formulation's (24ba113, f2d7982). ParameterMap and map.json are documented
  (f32ac16).

formulation-bench release at d20223c.

dataset-v0.3.0

Parameter maps and an audit. Every reformulation pair now states how one
formulation's parameters are computed from the other's, and the audit behind this
release corrected content in all 20 problems.

Dataset structure

• Every pair carries a parameter map. map.json gives each parameter of b as a
  function of a's, in LaTeX and Python. The two parametrizations were previously
  related only through the problem's data.json (a66e8e6).
• Proofs live in the pair directory. reformulations/pN/a_b.lean becomes
  reformulations/pN/a_b/Reformulation.lean, beside map.json (bb1a173).
• Sources cite a dataset-owned ref.bib. Every metadata.source names a citekey;
  an optional origin credits the work that first proposed a formulation reproduced
  from a survey (4006a09).
• Continuous variables are free unless the formulation bounds them. Generated
  solvers no longer inherit Gurobi's lb=0; p11 and p17.a now state the domains they
  had been relying on it for (49b9dfc).
• p11 collapsed from nine formulations to two. Every EvoCut extension was vacuous:
  each bounded a free variable in one direction and referenced it nowhere else, so all
  eight projected onto a's feasible region (c7e09e1, 028d40e).
• Mathematical symbols in descriptions are wrapped in inline LaTeX, and \cdot is
  \times throughout (8beb68f, 33b9a47).
• The dataset gains LICENSE.md, AGENTS.md, and a thin README.md.

20 problems, 109 formulations, 89 pairs — 62 positive, every one proved, and 27
negative.

Bug fixes

• p7 strips ranged over reversed intervals. The JSON declares strips over
  I = {(a,b) : a ≤ b} but Lean quantified over all of Fin N × Fin N. b and c's cut
  sums therefore ranged over degenerate strips, weakening them below spec; the unused
  coordinates also made the feasible sets infinite, breaking the cardinality argument
  behind the negative labels. Constraints and variables are now indexed by I
  (3fce062, 3724544).
• p17.a was unbounded. gen_data.py drew grades from [0.5, 3.0], but the
  formulation's partition into g < 1 and g = 1 is only a partition for g ≤ 1, so
  most blocks had free extraction variables. Grades are now drawn as ore fractions and
  g ≤ 1 is recorded as an assumption (df64573).
• p20.a solved a relaxation. Its acyclicity constraint carried only a Python
  comment, so codegen dropped it. Removed from the model; without it, b cannot match
  the objective on cycling flows, so b is invalid and the pair is now negative
  (bf7bea9).
• Lean formulations disagreed with their JSON. Realigned in p2–p5 and p6 c/d/i;
  unused flow-bound hypotheses and orphan private lemmas removed (a914bd7, bc80af8,
  274ced9, 677583f).
• Missing assumptions. p10 time-window ordering, p12 n ≥ 2 and the MTZ bound on
  all vertices, p13 city count, p14 n ≤ |S|, p15 positive floor count, p18 m ≥ 0,
  p6/p9 dimension nonemptiness.
• Parameter declarations disagreed with the data. p9 node indices typed integer,
  p11 types and n_L shape, p13 r shape, p15 area and ragged apartment dimension,
  p16 D a scalar, p20 dem indexed by camp; p15–p20 data.json regenerated to match.
• Recorded solutions. p12's MTZ positions were infeasible, p16's was misplaced,
  p14's was missing, p11's regenerated, and p10/p11/p13/p14's unwrapped.
• p15.b's apartment bound disagreed with its map. A nonzero assumption on the
  apartment dimension made the all-zero-capacity case unrepresentable; the bound is now
  the exact finite maximum of configuration capacities that map.json computes
  (0187f20).
• p13 encoded maximization as minimization. Objectives negated (648d564); the
  formulation ordering was also swapped so a is the aggregate model, with a new a_b
  proof (1a23d44).
• Also: p10's big-M widened to cover the time-window spread, p10.d's conflict-graph
  cuts enumerate all cliques, p19's unmodeled storage/deadline requirements and
  duplicate data keys dropped, p18's coverage indicator derived from distances, p8's
  EvoCut cuts moved to the end of the constraint lists.

Proofs

• New: p13 a_b, p15 a_b (replacing a b_a proof that ran the wrong direction).
• Removed: p11 a_c–a_i with their formulations, p20 a_b now that the pair is negative.

Testing

• Schema validation over the dataset JSON: parameter declarations against the recorded
  data, shapes against declared dimensions, code blocks against their kind (a4f0d3a).
• Structural checks that each Lean file is the declaration its path claims —
  namespacing, the five MILPFormulation declarations, variable domains, and the pair
  and direction a proof constructs (53f4907).
• Parameter maps are pinned to the formulations by composing the two descriptions of
  the same data: a's gen_params.py followed by the map must agree with b's (c5da3bd).

Dataset snapshot at 22e39ff.

sha256: 7964ec4803b98e35806bfe083a1bb22ef85b7954bc240ce19eaf166edec5bc69

formulation-bench-v0.3.0

Packaging and docs polish; no breaking API changes.

• Add README, AGENTS.md, and package-local Makefile to formulation-bench
• Flesh out PyPI metadata (readme, authors, license, keywords,
  classifiers, project URLs) so the published PyPI page renders correctly
• Replace the heavyweight dataset/README.md with a thin pointer to the
  documentation site; add dataset/AGENTS.md pointing to the schema docs
• Add pytest-cov coverage with Codecov uploads under the
  formulation_bench flag; new make cov / cov-open / cov-clean targets
• Fix badges in the package README

formulation-bench release at e6d295c.

formulation-bench-v0.2.0

API changes

• Rename Pair → Reformulation throughout
• Rename Formulation.gurobipy_code → gen_solve_py(); gen_params → run_gen_params
• Add Formulation.lean_formulation_path / lean_proof_path properties
• Add from_dict classmethods to model dataclasses
• Build Dataset.reformulations eagerly in init
• Take typed Formulation in codegen; drop Formulation.solve
• Make codegen module private; drop runtime ruff formatting
• Simplify Formulation.with_constraint via copy.copy

Dataset

• Fold pairs.json into dataset.json as reformulations
• Bump DEFAULT_DATASET_VERSION to dataset-v0.2.0
• Add download helper and dataset release workflow

Docs

• New user guide and Lean sections
• Generate per-problem pages from dataset JSON; flatten layout
• API reference refresh; sync citations with paper/ref.bib
• Run doctests via pytest (--doctest-modules)

formulation-bench release at 97ce5b4.

formulation-bench-v0.1.0

formulation-bench release at b8da66e.

dataset-v0.2.0

Switch to semantic versioning for the dataset.

Changes since dataset-v0.1:

• Make dataset/ the source of truth for the Lean project: it now owns
  Common.lean, lakefile.toml, lean-toolchain, and lake-manifest.json
  (package name FormulationBench), so the dataset is self-buildable
  with cd dataset && lake build. Reformulation imports drop the
  dataset. module prefix.
• Fold pairs.json into dataset.json as a reformulations field.
• Migrate hand-written notes into structured metadata.notes on each
  problem and formulation; split formulation-specific notes out of
  problem-level metadata.
• Generate per-problem docs pages from dataset JSON via a Sphinx
  extension that sources LaTeX from formulation.json.
• Remove HuggingFace-specific content from the dataset.

Dataset snapshot at d88f9c6.

sha256: 43ab0ad8d68fffc526abc59407548524f9318479f115bb111adbde9ad1171e60

dataset-v0.1

Publishes dataset/ as a GitHub release tarball on dataset-v* tags
(.github/workflows/release-dataset.yml), and adds
formulation_bench.download_dataset() + Dataset.load() so consumers can
fetch and cache a pinned dataset version. DEFAULT_DATASET_VERSION ties
each package release to the dataset snapshot it was built against.

Co-Authored-By: Claude Opus 4.7 noreply@anthropic.com

Dataset snapshot at 08c305e.

sha256: 5e8c87afb8460ddcf3b78d0b8db9a34825ee741df8e9c0b2212575fc8110c791