Definitions

FormulationBench includes machine-checkable Lean 4 definitions of MILP formulation and reformulation as defined in the FLARE Paper. Both definitions are defined in Common.lean.

MILP Formulation

We make a clear distinction between a formulation and the parameter (or data) values that define a particular instance of the problem. Take the traveling salesman problem (TSP) as an example. A TSP formulation is defined on an abstract set of cities. A TSP instance is one such city set. Instantiating the formulation with an instance yields a concrete MILP to be solved.

Definition

A MILP formulation \(\mathcal{M}\) is a tuple \(\mathcal{M} = (\mathcal{P}, \mathcal{F}, f_0)\) with parameter space \(\mathcal{P}\), feasible region \(\mathcal{F}(p) \subseteq \mathbb{R}^{n(p)}\), and objective function \(f_0\). For instance \(p \in \mathcal{P}\), the feasible region \(\mathcal{F}(p)\) is defined by \(m(p)\) linear constraints, \(f_i(\cdot ; p) : \mathbb{R}^{n(p)} \to \mathbb{R}\) for all \(i \in [m(p)]\). The first \(k(p) \leq n(p)\) variables are integers. The feasible region is

\[\mathcal{F}(p) = \{x \in \mathbb{Z}^{k(p)} \times \mathbb{R}^{n(p)-k(p)}~|~f_i(x;p) \leq 0 \; \forall i\in[m(p)]\}.\]

The objective is to minimize the linear function \(f_0(\cdot ; p) : \mathbb{R}^{n(p)} \to \mathbb{R}\). A formulation \(\mathcal{M}\) is instantiated with an instance \(p \in \mathcal{P}\). We denote an instantiated formulation as \(\mathcal{M}(p) = (\mathcal{F}(p), f_0(p))\).

Lean Encoding

The MILPFormulation structure in Common.lean encodes the tuple above. Params is the parameter space \(\mathcal{P}\), Vars p is the variable space for instance \(p\), feasible p x is the indicator of \(x \in \mathcal{F}(p)\), and obj p x is \(f_0(x; p)\).

structure MILPFormulation where
  Params   : Type
  Vars     : Params → Type
  feasible : (p : Params) → Vars p → Prop
  obj      : (p : Params) → Vars p → ℝ

Warning

MILPFormulation does not restrict Vars to \(\mathbb{R}^n\) nor does it assert linearity conditions on either feasible or obj. See the FLARE Paper for a further discussion.

Reformulation

Reformulation has an intuitive operational meaning: \(\mathcal{M}'\) is a reformulation of \(\mathcal{M}\) if one can map an instance \(\mathcal{M}(p)\) to an instance \(\mathcal{M}'(p')\), solve \(\mathcal{M}'(p')\), and efficiently recover an optimal solution to \(\mathcal{M}(p)\). Importantly, this is a formulation-level claim that holds across all problem instances \(p \in \mathcal{P}\). FormulationBench adopts a constructive definition of reformulation that is amenable to formalization and tractable for automated formal-proof systems.

Definition

Let \(\mathcal{M} = (\mathcal{P}, \mathcal{F}, f_0)\) and \(\mathcal{M}' = (\mathcal{P}', \mathcal{F}', f'_0)\) be formulations. A reformulation construction from \(\mathcal{M}\) to \(\mathcal{M}'\) is a tuple \(\Phi(\mathcal{M}, \mathcal{M}') = (\Phi_{\mathrm{p}},\, \Phi_{\text{fwd}},\, \Phi_{\text{bwd}},\, \Phi_{\text{obj}})\) consisting of:

• Parameter mapping. \(\Phi_{\mathrm{p}} : \mathcal{P} \to \mathcal{P}'\).

• Forward mapping. \(\Phi_{\text{fwd}}(\cdot;p) : \mathbb{R}^{n(p)} \to \mathbb{R}^{n'(\Phi_{\mathrm{p}}(p))}\).

• Backward mapping. \(\Phi_{\text{bwd}}(\cdot;p) : \mathbb{R}^{n'(\Phi_{\mathrm{p}}(p))} \to \mathbb{R}^{n(p)}\) computable in polynomial time.

• Objective mapping. \(\Phi_{\text{obj}} : \mathbb{R} \to \mathbb{R}\).

\(\mathcal{M}'\) is a constructive reformulation of \(\mathcal{M}\) if there exists a reformulation construction satisfying the following conditions for every instance \(p \in \mathcal{P}\), with \(p' = \Phi_{\mathrm{p}}(p)\):

• Forward feasibility. For all \(x \in \mathcal{F}(p)\): \(\Phi_{\text{fwd}}(x;p) \in \mathcal{F}'(p')\).

• Backward feasibility. For all \(x' \in \mathcal{F}'(p')\): \(\Phi_{\text{bwd}}(x';p) \in \mathcal{F}(p)\).

• Strictly monotone objective mapping. \(\Phi_{\text{obj}}\) is strictly monotonically increasing.

• Objective preservation. For all \(x \in \mathcal{F}(p)\), \(f_0'(\Phi_{\text{fwd}}(x;p);p') = \Phi_{\text{obj}}(f_0(x;p))\), and for all \(x' \in \mathcal{F}'(p')\), \(f_0'(x';p') = \Phi_{\text{obj}}(f_0(\Phi_{\text{bwd}}(x';p);p))\).

Lean Encoding

MILPReformulation F G in Common.lean encodes a reformulation construction from F to G. The fields correspond directly to the components above: paramMap is \(\Phi_{\mathrm{p}}\), fwd and bwd are the forward and backward mappings, objMap is \(\Phi_{\text{obj}}\) with monotonicity witnessed by objMap_mono. Lastly, fwd_feas, bwd_feas, fwd_obj, and bwd_obj discharge the four conditions.

structure MILPReformulation (F G : MILPFormulation) where
  paramMap    : F.Params → G.Params
  fwd         : (p : F.Params) → F.Vars p → G.Vars (paramMap p)
  bwd         : (p : F.Params) → G.Vars (paramMap p) → F.Vars p
  fwd_feas    : ∀ p x, F.feasible p x → G.feasible (paramMap p) (fwd p x)
  bwd_feas    : ∀ p x', G.feasible (paramMap p) x' → F.feasible p (bwd p x')
  objMap      : ℝ → ℝ
  objMap_mono : StrictMono objMap
  fwd_obj     : ∀ p x, F.feasible p x →
                  G.obj (paramMap p) (fwd p x) = objMap (F.obj p x)
  bwd_obj     : ∀ p x', G.feasible (paramMap p) x' →
                  G.obj (paramMap p) x' = objMap (F.obj p (bwd p x'))

Warning

MILPReformulation omits the restriction that the backward mapping \(\Phi_{\text{bwd}}\) is computable in polynomial time. See the FLARE Paper for a further discussion.