Theoretical Computer Science

Motivation

Given a $k$-connected graph, many connectivity algorithms run in time that grows with the number of edges $|E|$. A sparse certificate is a spanning subgraph with only $O(k|V|)$ edges that is still $k$-connected; computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the bound. Finding a $k$-connected spanning subgraph with the minimum number of edges is NP-complete for every fixed $k \ge 2$ (Garey and Johnson, problem GT31), so the question is how cheaply a sparse, not necessarily minimum, certificate can be found.

Nagamochi and Ibaraki (Algorithmica 7 (1992) 583–596) answered this with a single linear-time scanning procedure, FOREST, which partitions the edges into classes $E_1, E_2, \dots, E_{|E|}$. They showed that the prefix unions $E_1 \cup \dots \cup E_k$ are certificates for edge-connectivity and, for simple graphs, for node-connectivity. The node-connectivity result is the subject of this mission; the edge-connectivity result is the preceding mission of this series.

Timeline:

• 1980: Galil gives an algorithm testing $\kappa(G) \ge k$ whose running time depends on $|E|$ (SIAM J. Comput. 9).
• Before 1992 (as cited on p. 583): Suzuki et al. give $O(|E|)$-time algorithms for sparse 2- and 3-node-connected spanning subgraphs; Nishizeki and Poljak find, for general $k$, a $k$-node-connected spanning subgraph with at most $k(|V|-1)$ edges in $O(|V|^{1/2}|E|^2)$ time.
• 1992: Nagamochi and Ibaraki prove that FOREST, which runs in $O(|V| + |E|)$ time, yields a $k$-node-connected spanning subgraph $G_k$ of every simple $k$-node-connected graph, with $|E(G_k)| \le k|V| - k(k+1)/2$. Their Theorem 3.1 states a stronger, local form.
• 1993: Cheriyan, Kao and Thurimella isolate "scan-first search" as the general principle behind such certificates (SIAM J. Comput. 22 (1993)).

Setting

A graph $G = (V, E)$ has a finite node set $V$ with $|V| \ge 2$ and a finite edge set $E$; each edge has an unordered pair of two distinct end nodes. In this mission the graph is simple: no two edges have the same end nodes. For $F \subseteq E$, $(V, F)$ is the spanning subgraph with edge set $F$.

The local node-connectivity $\kappa(x, y; H)$ of nodes $x, y$ in a graph $H$ on $V$ is $|V| - 1$ if $x$ and $y$ are adjacent in $H$, and otherwise the minimum size of a node set $W \subseteq V - \{x, y\}$ whose deletion leaves no $x$–$y$ path. The node connectivity is $\kappa(G) = \min_{x, y} \kappa(x, y; G)$.

Procedure FOREST keeps a label $r(v) \ge 0$ on each node, initially $0$. While some node is unscanned, it chooses an unscanned node $x$ of largest label; for each unscanned edge $e = (x, y)$ it puts $e$ into the class $E_{r(y)+1}$, increases $r(x)$ by one if $r(x) = r(y)$, and increases $r(y)$ by one; then it marks $x$ scanned. Ties are broken arbitrarily. The time instants are the states between these elementary operations; $E^*_i$ denotes the class $i$ at an instant, and $E_i$ its final value. Put

$$G_i = (V,\ E_1 \cup E_2 \cup \dots \cup E_i).$$

Formalization targets

Goal: Theorem 3.1

For a simple graph $G$ and the classes of any completed run of FOREST, for $1 \le i \le |E|$,

$$\kappa(x, y; G_i) \ \ge\ \min\{\kappa(x, y; G),\ i\} \qquad \text{for any } x, y \in V. \tag{3.1}$$

The statement is local: it holds pair by pair, not only for the global minimum, and for every tie-breaking of the procedure.

Milestones, in the order the proof uses them

1. Lemma 2.2: at every instant, a node $v$ meets $E_i$ exactly for $i = 1, \dots, r(v)$.
2. Lemma 2.4(b): at every instant, a $u$–$v$ path in $E^*_j$ yields $u$–$v$ paths in every $E^*_i$, $i < j$.
3. In-degree at most one (§2, p. 588): orienting each edge from the earlier-scanned to the later-scanned end, every node has at most one entering arc in each class.
4. Lemma 3.1: if an $x$–$y$ path of $E^*_j$ has the form $x, u_1, \dots, u_k = w, y$ with $k = 1$ or $u_1$ scanned before $w$, then any $w$–$x$ and $w$–$y$ paths in $E^*_i$ ($i < j$) share a node other than $w$.
5. Lemma 3.2: for a node cut set $W = \{w_1, \dots, w_i\}$ of $G_{i+1}$ (in scan order) separating a component $X$ from the rest $Y$, immediately after $w_t$ is scanned every $X$–$Y$ path of $E^*_t$ passes through $w_t$, and $E^*_j$ has no $X$–$Y$ path for $t + 1 \le j \le i + 1$.

A companion item states the paper's announcement in §3: $G_k$ is $k$-node-connected for every $1 \le k \le \kappa(G)$.

Significance

Theorem 3.1 at $i = k$ shows that the first $k$ classes of FOREST form a $k$-node-connected spanning subgraph whenever $G$ is, and the edge-count analysis of the companion mission bounds its size by $k|V| - k(k+1)/2$. Since FOREST runs in linear time, any algorithm testing $\kappa(G) \ge k$ can be run on $G_k$ instead of $G$; the paper uses this to improve the bound for testing $\kappa(G) \ge k$ from $O(\max\{k^2|V|^{1/2}, k|V|\}|E|)$ to $O(\max\{k^3|V|^{3/2}, k^2|V|^2\})$, and similar gains for computing the number of node-disjoint paths between two nodes. The local form (3.1) is what makes the $s$–$t$ applications possible.

The result is proved on paper. As far as a search of the platform shows, neither FOREST nor local node-connectivity has a machine-checked treatment there; Mathlib has no notion of vertex connectivity of a pair of nodes. This mission produces a formal model of FOREST as a nondeterministic transition system and the statements needed to verify the paper's proof step by step.

Difficulty

For edge-connectivity the analogous statement follows from a general principle: any sequence of maximal spanning forests, each taken in what remains of the graph, preserves local edge-connectivity up to its length. The obvious attempt is to prove (3.1) the same way, from the fact that each $E_i$ is a maximal spanning forest of what the earlier classes leave. The paper gives no such argument for node-connectivity: its proof uses the specific scan order of FOREST in an essential way, through the orientation of edges from earlier- to later-scanned nodes and the in-degree bound of that orientation (Lemmas 3.1 and 3.2). The argument tracks, for a hypothetical node cut $W$ of size $i$ in $G_{i+1}$, the classes at the moments the nodes of $W$ are scanned, which requires reasoning about intermediate states of the algorithm and about paths in several classes at once. None of this reduces to a static property of the output partition.

Formalization scope

• Graphs. A node type V and an edge type E, both finite, with ends : E → Sym2 V; loop-freeness is ∀ e, ¬ (ends e).IsDiag and simplicity is Function.Injective ends. The standing assumptions of p. 583 and p. 589 ($|V| \ge 2$, no self-loop, a simple graph when node-connectivity is discussed) appear as hypotheses; §2 items are stated for loopless graphs, as on the page.
• Connectivity. $\kappa(x, y; (V, F))$ is valued in $\mathbb N_\infty$: $|V| - 1$ on adjacent pairs, the minimum node cut otherwise, and $\top$ when $x = y$, where (3.1) holds trivially.
• FOREST. A nondeterministic step relation with three steps (select, scan, finish), a run of length $K$ from the initial state, and completion when every node is scanned. Every tie-breaking is allowed, so the theorems quantify over all completed runs. A time instant is a state of a run; "scanned before" compares positions in the run's selection order; "immediately after $w_t$ has been scanned" is the state right after the finish step of $w_t$.
• Excluded. The running time "$O(|V| + |E|)$" and everything in §4 (the connectivity-testing algorithms and their bounds) are not stated: the paper fixes no machine model. The edge bounds on $|E_i|$ belong to the edge-connectivity mission.
• Ruled out. Stating (3.1) for an arbitrary partition into maximal spanning forests, or reading the classes $E^*_j$ of Lemmas 3.1–3.2 off the final state, would state a different theorem from the one the paper proves; the classes are those of a run of FOREST at the instant the page specifies.
• Infrastructure. Reachability avoiding a node set, walks and paths in SimpleGraph, and invariants of the FOREST transition system. The definitions duplicate those of the edge-connectivity mission by design and are candidates for a shared layer. Contributions of general lemmas about the run (label invariants, monotonicity of classes along a run) are welcome.

Selected references

• H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$-connected spanning subgraph of a $k$-connected graph, Algorithmica 7 (1992), 583–596. https://doi.org/10.1007/BF01758778
• Z. Galil, Finding the vertex connectivity of graphs, SIAM J. Comput. 9 (1980), 197–199. https://doi.org/10.1137/0209016
• J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$-vertex connectivity, SIAM J. Comput. 22 (1993), 157–174. https://doi.org/10.1137/0222013
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.

Motivation

Many graph algorithms for connectivity questions run in time proportional to the number of edges. When the question is only whether a graph is $k$-edge-connected, or what its local edge-connectivities are up to a threshold $k$, most edges are irrelevant: a spanning subgraph with $O(k|V|)$ edges already carries the answer. Such a subgraph is called a sparse certificate. Computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the running time of connectivity testing, of Matula-type edge-connectivity algorithms, and of $s$–$t$ flow computations used as connectivity oracles.

Nagamochi and Ibaraki (Algorithmica 7, 1992) gave a procedure, FOREST, that computes such a certificate for edge-connectivity and, on simple graphs, for node-connectivity, with a single graph search. The same partition of the edges into forests is the engine of their deterministic minimum-cut algorithm for multigraphs (SIAM J. Discrete Math. 5, 1992), which later became the maximum-adjacency ordering of the Stoer–Wagner minimum-cut algorithm (J. ACM 44, 1997).

Timeline:

• 1927: Menger identifies the minimum number of edges separating two nodes with the maximum number of edge-disjoint paths between them.
• 1992: Nagamochi and Ibaraki publish Procedure FOREST and prove that its $i$-th prefix preserves local edge-connectivity up to $i$ in multigraphs, and local node-connectivity up to $i$ in simple graphs.
• 1993: Cheriyan, Kao and Thurimella (SIAM J. Comput. 22) obtain sparse certificates by scan-first search; Frank, Ibaraki and Nagamochi (J. Graph Theory 17) give a shorter proof for the node-connectivity case.
• 1994: Nishizeki and Poljak (Discrete Appl. Math. 55) publish the forest-decomposition lemma (Lemma 2.1 below), found independently.

Setting

A graph $G = (V, E)$ is finite and undirected, has $|V| \ge 2$ nodes, may have multiple edges (several edges with the same pair of end nodes), and has no self-loop. It is simple if no two edges have the same end nodes. For $F \subseteq E$, $(V, F)$ is the spanning subgraph with edge set $F$. It is a forest if it has no cycle; two parallel edges form a cycle. It is a maximal spanning forest in $(V, H)$, for $F \subseteq H$, if adding any edge of $H \setminus F$ to $F$ creates a cycle.

The local edge-connectivity $\lambda(x, y; H)$ is the minimum number of edges of $H$ whose removal leaves no path from $x$ to $y$; parallel edges count separately. It is $\infty$ when $x = y$.

Procedure FOREST keeps a label $r(v) \in \mathbb{N}$ on every node, initially $0$, and classes $E_1, E_2, \dots, E_{|E|}$, initially empty. While an unscanned node exists, it picks an unscanned node $x$ of largest label; for every unscanned edge $e$ from $x$ to a node $y$, it puts $e$ into $E_{r(y)+1}$, increases $r(x)$ by one if $r(x) = r(y)$, increases $r(y)$ by one, and marks $e$ scanned; then it marks $x$ scanned. Ties among nodes and the order of edges are free. On termination, $G_i = (V, E_1 \cup \cdots \cup E_i)$.

Formalization targets

Goal: Theorem 2.1 (pp. 588–589), without the running time

For every graph $G$ and every completed execution of FOREST on $G$:

1. every edge lies in exactly one class $E_i$, $1 \le i \le |E|$;
2. for $i = 1, \dots, |E|$,

$$\lambda(x, y; G_i) \ge \min\{\lambda(x, y; G),\ i\} \qquad \text{for all } x, y \in V; \tag{2.1}$$

3. $|E_i| \le |V| - 1$ for all $i$;
4. if $G$ is simple, $|E_i| \le |V| - i$ for $i \le |V| - 1$ and $E_i = \emptyset$ for $i \ge |V|$.

Milestones

• Lemma 2.2 (p. 587): during the execution, a node $v$ has incident edges in exactly the classes $E_1, \dots, E_{r(v)}$.
• Lemma 2.3 (p. 587): each $(V, E_i)$ is a forest at every instant.
• Lemma 2.4 (p. 588): (a) an edge $(u, v)$ added to $E_i$ has its end nodes joined by a path in $E_{i-1}$; (b) a path in $E_j$ between $u$ and $v$ yields a path in every $E_i$, $i < j$.
• Lemma 2.5 (p. 588): each output $(V, E_i)$ is a maximal spanning forest in $G - E_1 \cup \cdots \cup E_{i-1}$.
• Lemma 2.1 (p. 584): any sequence of successive maximal spanning forests satisfies (2.1).

Companions

• the sparse certificate (p. 589): if $\lambda(x, y; G) \ge k$ for all $x, y$, then $G_k$ is $k$-edge-connected with $|E(G_k)| \le k(|V| - 1)$, and $|E(G_k)| \le k|V| - k(k+1)/2$ for simple $G$;
• Lemma 2.6 (p. 589): for $k \le \delta(G)$, $G_k$ has a node of degree exactly $k$.

Significance

(2.1) says that one search produces, for every threshold $k$ at once, a subgraph with at most $k(|V|-1)$ edges that keeps every local edge-connectivity up to $k$. Any algorithm whose running time grows with $|E|$ can then be run on $G_k$ in place of $G$; §4 of the paper uses this to speed up $k$-connectivity tests and the computation of local connectivities. The same forest partition is the structural fact behind the Nagamochi–Ibaraki and Stoer–Wagner minimum-cut algorithms. Lemma 2.6 shows that the certificate is tight: its edge-connectivity is exactly $k$ when $\lambda(G) \ge k$.

The results are proved in the paper. No machine-checked proof of them is known. Formalizing them means formalizing a graph search with free tie-breaking as a transition system, reasoning about invariants of all its executions, and proving a cut-counting statement for multigraphs. Mathlib's connectivity notions, such as SimpleGraph.IsEdgeReachable, do not see parallel edges, so the multigraph cut theory here is new.

Difficulty

Lemma 2.1 is a short cut argument once maximality is available. The difficulty is showing that FOREST, which assigns each edge to a class by looking only at the label of one end node, produces maximal forests in the successive residual graphs (Lemma 2.5). The obvious invariant, that the class of an edge is the first forest it does not close a cycle in, is not what line 7 computes. The label $r(y)$ records only which classes touch $y$, not which component of each class contains $y$. The paper's argument needs Lemma 2.4(a): at the moment an edge is added to $E_i$ its ends already lie in one tree of $E_{i-1}$. That relies on the choice of the unscanned node of largest label, on the order of lines 8 and 9, and on an argument about the scan order of tree roots.

Formalization scope

• Graphs. A graph is a finite node type V with $|V| \ge 2$, a finite edge type E, and ends : E → Sym2 V with no diagonal value (no self-loops). Parallel edges are distinct elements of E. Simplicity is injectivity of ends, and edge subsets are Finset E. A forest is an edge set in which every edge is a bridge, a condition that sees parallel edges.
• Connectivity. $\lambda$ is an infimum in ℕ∞ over separating edge sets, $\infty$ at $x = y$. (2.1) is kept "for all $x, y$", as printed.
• FOREST. FOREST is a nondeterministic step relation (select, scan, finish) on explicit states: labels, class index per edge ($0$ = unscanned), scanned nodes, current node and selection order. The theorems quantify over every run from the initial state, so no tie-breaking rule is fixed. "At some time instant" is a state of the run; "upon completion" is a run whose last state has every node scanned. Lemma 2.2 is stated at every state, not only after a scan block (the other steps change neither labels nor classes). Lemma 2.4(a) assumes $i \ge 2$, since $E_0$ does not exist.
• Exclusions. Theorem 2.1's clause "is found in $O(|V| + |E|)$ time", the bucket implementation, and the time bound of the certificate are not formalized: the paper fixes no machine model. The goal consists of the structural conclusions only. The bound printed "if $G$ is multiple" is stated for every loopless graph.
• Non-triviality. The goal is about the classes of a run of FOREST. An arbitrary partition of $E$ into maximal spanning forests is Lemma 2.1's hypothesis, not a formalization of Theorem 2.1. A statement in which the classes are unconstrained variables, or in which the run hypotheses cannot be met, would be trivial. A separate sanity file checks that a complete run on the triangle $K_3$ exists and attains $|E_1| = |V| - 1$, $|E_2| = |V| - 2$.
• Welcome contributions. Useful reusable infrastructure includes:
  • a cut and Menger layer for finite multigraphs;
  • forest and bridge lemmas for edge-indexed graphs;
  • invariant-style reasoning over runs.

Selected references

• H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$-connected spanning subgraph of a $k$-connected graph, Algorithmica 7 (1992) 583–596. https://doi.org/10.1007/BF01758778
• H. Nagamochi, T. Ibaraki, Computing edge-connectivity in multigraphs and capacitated graphs, SIAM J. Discrete Math. 5 (1992) 54–66. https://doi.org/10.1137/0405004
• T. Nishizeki, S. Poljak, $k$-connectivity and decomposition of graphs into forests, Discrete Appl. Math. 55 (1994) 295–301. https://doi.org/10.1016/0166-218X(94)90014-0
• J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$-vertex connectivity, SIAM J. Comput. 22 (1993) 157–174. https://doi.org/10.1137/0222013
• A. Frank, T. Ibaraki, H. Nagamochi, On sparse subgraphs preserving connectivity properties, J. Graph Theory 17 (1993) 275–281. https://doi.org/10.1002/jgt.3190170302
• M. Stoer, F. Wagner, A simple min-cut algorithm, J. ACM 44 (1997) 585–591. https://doi.org/10.1145/263867.263872

Motivation

Manufacturing cells, communication protocols, traffic systems and database transaction managers are naturally described not by differential equations but by sequences of discrete events: a machine starts, a part arrives, a message is lost. Ramadge and Wonham's 1987 paper (SIAM J. Control Optim. 25(1)) set up a control theory for such systems in which the plant is an automaton, the controller is another automaton that may disable some events, and specifications are formal languages. The framework, now called supervisory control theory or the Ramadge–Wonham framework, is the standard model for the logical control of discrete event systems and underlies the textbook treatment in Cassandras and Lafortune (Introduction to Discrete Event Systems, 2008) and Wonham and Cai (Supervisory Control of Discrete-Event Systems, 2019).

The question the paper answers is the basic synthesis question of the theory: given a plant, a set of legal behaviours and a set of minimally acceptable behaviours, when does a controller exist that keeps the plant legal, achieves at least the acceptable behaviour, and never deadlocks, and what is the least restrictive such controller?

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$ with a state set $Q$, a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$, an initial state $q_0$ and marker states $Q_m \subseteq Q$. Extending $\delta$ to strings, the generated language $L(\mathcal G)$ is the set of strings $w$ for which $\delta(w, q_0)$ is defined, and the marked language $L_m(\mathcal G)$ is the subset of those that end in $Q_m$. The closure $\bar K$ of a language $K$ is its set of prefixes; $K$ is closed if $K = \bar K$. Throughout, $\mathcal G$ is assumed trim in the sense $L(\mathcal G) = \bar L_m(\mathcal G)$: every generated string can be completed to a marked one.

The alphabet is split into controllable events $\Sigma_c$ and uncontrollable events $\Sigma_u = \Sigma - \Sigma_c$. A supervisor $\mathcal S = (S, \phi)$ consists of a deterministic, accessible automaton $S = (X, \Sigma, \xi, x_0, X_m)$, whose state set $X$ may be infinite, and a map $\phi$ assigning to each state $x$ the set of controllable events it enables; uncontrollable events are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep: an event occurs when the plant can execute it, the supervisor enables it, and the supervisor's automaton can follow it. This defines the languages $L(\mathcal S/\mathcal G)$, $L_m(\mathcal S/\mathcal G)$ and the controlled language $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$.

$\mathcal S$ is complete if its automaton never refuses an event that the plant can execute and $\phi$ enables; it is proper if it is complete and

$$\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G),$$

that is, every closed-loop string can be completed to a marked task. A language $K$ is controllable if $K \subseteq L(\mathcal G)$ and $\bar K \Sigma_u \cap L(\mathcal G) \subseteq \bar K$. For $L \subseteq L(\mathcal G)$, $\mathbf C_{\mathcal G}(L)$ is the class of controllable sublanguages of $L$ and $\mathbf F_{\mathcal G}(L)$ the class of sublanguages $K$ of $L$ with $K = \bar K \cap L_m(\mathcal G)$.

Given $\emptyset \neq L_a \subseteq L_g \subseteq L_m(\mathcal G)$, the Supervisory Marking Problem (SMP) asks for a proper $\mathcal S$ with $L_a \subseteq L_m(\mathcal S/\mathcal G) \subseteq L_g$, and the Supervisory Control Problem (SCP) for a proper $\mathcal S$ with $L_a \subseteq L_c(\mathcal S/\mathcal G) \subseteq L_g$.

Formalization targets

Goal: Theorem 7.1 (pp. 218–219)

$$\text{SMP solvable} \iff \sup \mathbf C_{\mathcal G}(L_g) \supseteq L_a, \qquad \text{SCP solvable} \iff \sup\{\mathbf C_{\mathcal G}(L_g) \cap \mathbf F_{\mathcal G}(L_g)\} \supseteq L_a,$$

and in each case the solving supervisor can be taken minimally restrictive: its marked (respectively controlled) language equals the supremal element and contains that of every proper supervisor whose language lies in $L_g$.

Milestones

1. Proposition 4.1 (i), (ii): marking is independent of control; every $K \subseteq L_m(\mathcal G)$, or $K \subseteq L \cap L_m(\mathcal G)$ for an achievable closed $L$, is the marked language of a complete supervisor.
2. Proposition 5.1: a complete supervisor realizes $(L_m, L_c, L) = (K_1, K_2, K_3)$ iff $K_1 \subseteq K_2$, $K_2 = K_3 \cap L_m(\mathcal G)$ and $K_3$ is closed and controllable.
3. Theorem 6.1 (i), (ii): a proper supervisor with $L_m(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable; one with $L_c(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable and $L_m(\mathcal G)$-closed.
4. Proposition 7.1: $\mathbf C_{\mathcal G}(L)$ and $\mathbf F_{\mathcal G}(L)$ contain $\emptyset$ and are closed under arbitrary unions.
5. The supremal elements (p. 218): $\sup \mathbf C_{\mathcal G}(L)$, $\sup \mathbf F_{\mathcal G}(L)$ and $\sup\{\mathbf C_{\mathcal G}(L) \cap \mathbf F_{\mathcal G}(L)\}$ belong to their classes.

Significance

Theorem 7.1 reduces the existence of a correct, non-blocking controller to a single language inclusion, and identifies the supremal controllable sublanguage as the behaviour of the least restrictive solution. That object is the backbone of the later theory: modular and decentralized control, control under partial observation, and the computational results that $\sup \mathbf C_{\mathcal G}(L)$ is regular and computable when $\mathcal G$ is finite and $L$ regular all start from it.

The result is proved in the paper and has been taught for decades; it is not open. Mathlib has no model of generators with partial transitions, supervisors or controllability (its DFA has a total transition function and a single accepted language), and no formalization of this theory exists on the platform. This mission provides one: a reusable Lean model of generators with partial transitions, supervisors with possibly infinite state, closed loops and controllability, together with the paper's existence theorems stated against it. A second mission on the same paper (quotients of supervisors, Theorem 10.1) builds on the same objects.

Difficulty

The combinatorial core of Proposition 7.1 is a short prefix-closure computation. The work lies in the constructions: to show existence, a supervisor must be built for an arbitrary controllable language, which in general is not regular, so the supervisor needs an infinite state set (for example strings of the target language) together with a proof that the closed loop generates exactly the intended language, is complete, and is proper. The converse directions require relating the closed-loop run to separate runs of the plant and of the supervisor's automaton. The naive shortcut of reading the "sup" as an arbitrary member of $\mathbf C_{\mathcal G}(L_g)$ containing $L_a$ skips the content of the supremal-element milestone; the goal is stated with the actual union.

Formalization scope

• The alphabet is a type α with [Fintype α]; strings are List α, the empty string is [], and $s\sigma$ is s ++ [σ]. Languages are Set (List α); the closure is pre K = {s | ∃ t, s ++ t ∈ K}.
• A generator is a structure with a state type Q : Type, a partial transition δ : α → Q → Option Q, an initial state and a marker set. No finiteness is assumed on states, of the plant or of the supervisor. Supervisors and generators live in Type 1.
• $\phi$ maps states to Ec → Bool; an event outside $\Sigma_c$ is enabled by definition, so uncontrollable events cannot be disabled.
• The closed loop is the product run from $(x_0, q_0)$; the accessible part in the paper's display (2.1) changes no language and is not built.
• Standing assumptions carried by every theorem: $\Sigma$ finite, $L(\mathcal G) = \bar L_m(\mathcal G)$, supervisor automata accessible (as a hypothesis on every input supervisor and a conjunct of every "there exists a supervisor").
• $\sup$ is sSup in the complete lattice Set (List α).
• A formalization in which the closed loop ignores $\phi$ or the plant, in which completeness is dropped from properness, or in which the supervisor is restricted to finitely many states, is not the paper's theorem and is ruled out by the definitions above.

Welcome contributions: the basic run lemmas (closed-loop runs project to plant and supervisor runs), the string-state supervisor construction, and proofs of the milestones in the given order.

Selected references

• P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
• W. M. Wonham and P. J. Ramadge, On the Supremal Controllable Sublanguage of a Given Language, SIAM J. Control Optim. 25(3):637–659, 1987. https://doi.org/10.1137/0325036
• C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
• W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

Motivation

Clique-width is a graph parameter introduced by Courcelle and Olariu (Discrete Appl. Math. 101 (2000)) that measures how far a graph is from being built by a few labelled operations. Every problem expressible in monadic second-order logic with quantification over vertices and vertex sets (MSO$_1$) can be solved in linear time on graphs given together with a decomposition of bounded clique-width (Courcelle, Makowsky and Rotics, Theory Comput. Syst. 33 (2000)). Bounded clique-width is more general than bounded tree-width: complete graphs have unbounded tree-width but clique-width $2$.

For fixed $k$ there was, before this paper, no polynomial-time algorithm that either decides that a graph has clique-width at least $k+1$ or outputs a decomposition of clique-width bounded by a function of $k$; the best known algorithm, by Johansson (2001), gave width $2k\log n$. Oum and Seymour (J. Combin. Theory Ser. B 96 (2006)) closed this gap with approximation $2^{3k+2}-1$, through rank-width and a factor-3 approximation for the branch-width of symmetric submodular functions.

Timeline:

• 1991: Robertson and Seymour introduce branch-width of graphs and hypergraphs (J. Combin. Theory Ser. B 52).
• 2000: Courcelle and Olariu define clique-width; Courcelle, Makowsky and Rotics solve MSO$_1$ problems on graphs given with a $k$-expression.
• 2001: Johansson gives a $2k\log n$ approximation.
• 2006: Oum and Seymour define rank-width, prove $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$, and give an $O(n^9 \log n)$ algorithm that outputs a $(2^{3k+2}-1)$-expression or certifies clique-width above $k$.

Setting

All graphs are finite and simple. For a finite set $V$, a function $f : 2^V \to \mathbb{Z}$ is submodular if $f(X)+f(Y) \ge f(X\cap Y)+f(X\cup Y)$ and symmetric if $f(X) = f(V\setminus X)$.

A branch-decomposition of $f$ is a pair $(T, L)$ where $T$ is a tree with at least two vertices and all degrees at most $3$, and $L$ is a bijection from $V$ onto the leaves of $T$. Removing an edge $e$ of $T$ splits the leaves in two; the width of $e$ is $f$ of the set of elements of $V$ on one side. The width of $(T, L)$ is the largest edge width, and the branch-width $\mathrm{bw}(f)$ is the least width of a branch-decomposition, with $\mathrm{bw}(f) = f(\emptyset)$ when $|V| \le 1$.

A set $W \subseteq V$ is well-linked with respect to $f$ if for every partition $(X, Y)$ of $W$ and every $Z$ with $X \subseteq Z \subseteq V\setminus Y$, $f(Z) \ge \min(|X|, |Y|)$.

Let $A(G)$ be the adjacency matrix of $G$ over $\mathrm{GF}(2)$. For disjoint $X, Y \subseteq V(G)$, $\mathrm{cutrk}^*_G(X, Y)$ is the rank of the submatrix of $A(G)$ with rows $X$ and columns $Y$, and the cut-rank function is $\mathrm{cutrk}_G(X) = \mathrm{cutrk}^*_G(X, V(G)\setminus X)$. The rank-width $\mathrm{rwd}(G)$ is $\mathrm{bw}(\mathrm{cutrk}_G)$.

A $k$-expression is a term built from constants $\cdot_i$ (a vertex with label $i \in \{1,\dots,k\}$), the operators $\eta_{i,j}$ ($i \ne j$; add all edges between labels $i$ and $j$), $\rho_{i\to j}$ (relabel $i$ into $j$) and disjoint union $\oplus$. Its value is the labelled graph it produces; $G$ has clique-width $\mathrm{cwd}(G) \le k$ if some $k$-expression has value isomorphic to $G$.

An interpolation of $f$ is a function $f^*$ on disjoint pairs $(X, Y)$ that agrees with $f$ on $(X, V\setminus X)$, is monotone, submodular in the sense $f^*(A,B)+f^*(C,D) \ge f^*(A\cap C, B\cup D) + f^*(A\cup C, B\cap D)$, and has $f^*(\emptyset,\emptyset)=f(\emptyset)$.

Formalization targets

Goal: Theorem 1.1, certificate form

For a graph $G$ with at least one vertex and an integer $k \ge 1$:

$$\exists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \ge k+1,$$ $$\nexists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \le 2^{3k+2}-1.$$

The same explicit condition decides which side of the approximation holds; this is what the paper's algorithm certifies.

Milestones

1. Proposition 4.1: properties of an interpolation, including that $X \mapsto f^*(X, B) - f(\emptyset)$ is a matroid rank function on $V\setminus B$ when $f(\{v\}) - f(\emptyset) \le 1$.
2. Proposition 4.2: $f_{\min}(X,Y) = \min_{X\subseteq Z\subseteq V\setminus Y} f(Z)$ is an interpolation.
3. Theorem 5.1: a well-linked set of size $k$ forces $\mathrm{bw}(f) \ge k/3$ (for $k \ne 1$).
4. Theorem 5.2: no well-linked set of size $k$ implies $\mathrm{bw}(f) \le k$, when $f(\{v\}) \le 1$.
5. Proposition 6.1: $\mathrm{rk}\,M[X_1,Y_1] + \mathrm{rk}\,M[X_2,Y_2] \ge \mathrm{rk}\,M[X_1\cup X_2, Y_1\cap Y_2] + \mathrm{rk}\,M[X_1\cap X_2, Y_1\cup Y_2]$.
6. Corollary 6.2: submodularity of $\mathrm{cutrk}^*_G$ and $\mathrm{cutrk}_G$.
7. Section 6 claim: $\mathrm{cutrk}_G$ is symmetric submodular and $\mathrm{cutrk}^*_G$ interpolates it.
8. Proposition 6.3: $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$.

Significance

The dichotomy turns clique-width, for which no exact polynomial algorithm is known even for fixed $k$, into a parameter that can be approximated with an explicit witness in each direction. Downstream, every algorithm for graphs of bounded clique-width that needs a $k$-expression as input becomes applicable to graphs given without one, at the cost of an exponential blow-up of the width.

The result is proved in the literature; this mission formalizes it. To our knowledge none of the objects involved — branch-width of set functions, rank-width, cut-rank, $k$-expressions, clique-width — has been formalized in Mathlib, and the submodularity of submatrix rank (Proposition 6.1) is absent from Mathlib's Matrix.rank API. The formal development would give reusable definitions of branch-decompositions of arbitrary integer set functions, of cut-rank, and of clique-width, and a machine-checked link between the combinatorial and the linear-algebraic width parameters.

Difficulty

The upper bound in Theorem 5.2 is the core. The natural approach, growing a branch-decomposition one leaf split at a time while keeping the width at most $k$, gets stuck at a leaf carrying a set $B$ with $f(B) = k$: a split of $B$ into two parts of $f$-value below $k$ has to be found, and it must be found from the failure of well-linkedness of a set that is not obviously related to $B$. The paper's device is the interpolation $f^*$, which attaches a matroid to $B$ whose base has exactly $f(B)$ elements. Formalizing this requires handling partial branch-decompositions, their extensions, and a maximality argument over trees, none of which exists in Mathlib.

Proposition 6.3's upper bound is a second, independent difficulty: a rank-decomposition must be converted into a $k$-expression by an induction over a rooted binary tree, with a relabelling argument bounding the number of labels by the number of distinct nonzero rows of a $\mathrm{GF}(2)$ matrix of rank $k$. Its lower bound needs the tree structure of a $k$-expression to be read as a branch-decomposition.

Formalization scope

The ground set is a Fintype V with DecidableEq V; subsets are Finset V; set functions are Finset V → ℤ, as in the paper. A branch-decomposition is a tree T : SimpleGraph (Fin n) with $n \ge 2$, all neighbour sets of size at most $3$, and an injective map $L$ from $V$ onto the vertices of degree $1$; the side of an edge $uw$ is found by reachability from $u$ after deleting $uw$. Branch-width, rank-width and clique-width are never computed as minima: "$\mathrm{bw}(f) \le k$" is the predicate "$|V| \le 1$ and $f(\emptyset) \le k$, or a branch-decomposition of width at most $k$ exists", lower bounds say that every branch-decomposition has a wide edge, and "$\mathrm{cwd}(G) \le k$" is "$G$ has a $k$-expression". Labels $\{1,\dots,k\}$ are Fin k. The value of a $k$-expression has as vertex type the occurrences of constants (a nested sum type), and $\eta_{i,j}$ requires $i \ne j$. Cut-rank uses Matrix.rank over ZMod 2 of submatrices of SimpleGraph.adjMatrix. An interpolation is a function on all pairs of subsets whose axioms are imposed on disjoint pairs only.

Running time is not formalized. The paper's Theorem 1.1 asserts an $O(n^9\log n)$ algorithm; there is no cost model on the page, and the goal states the certificate the algorithm returns instead. Without the running time, "$\mathrm{cwd}(G) \ge k+1$ or $\mathrm{cwd}(G) \le 2^{3k+2}-1$" holds for every graph, so that reading is ruled out as a formalization of the goal; so are well-linkedness with respect to anything other than $\mathrm{cutrk}_G$, widths defined by an unguarded infimum (which is $0$ on an empty family), $k$-expressions whose value is not the graph up to isomorphism or whose $\eta$ may join equal labels, and Theorem 5.1 stated for $k = 1$.

Correction of Theorem 5.1. As printed, Theorem 5.1 fails for $k = 1$: a singleton is always well-linked, but the edgeless graph on two vertices has cut-rank identically $0$ and branch-width $0 < 1/3$. The milestone carries the hypothesis $k \ne 1$; the goal uses the theorem only at size $3k+1 \ge 4$.

The graph with no vertex is excluded from the goal and from the upper bound of Proposition 6.3, since it has no $k$-expression for any $k$. Contributions welcome: proofs of the milestones, lemmas on branch-decompositions (suppressing degree-2 vertices, extending partial decompositions), and submatrix-rank submodularity, which is reusable beyond this mission.

Selected references

• S. Oum and P. Seymour, Approximating clique-width and branch-width, J. Combin. Theory Ser. B 96 (2006) 514–528. https://doi.org/10.1016/j.jctb.2005.10.006
• B. Courcelle and S. Olariu, Upper bounds to the clique width of graphs, Discrete Appl. Math. 101 (2000) 77–114. https://doi.org/10.1016/S0166-218X(99)00184-5
• B. Courcelle, J. A. Makowsky and U. Rotics, Linear time solvable optimization problems on graphs of bounded clique-width, Theory Comput. Syst. 33 (2000) 125–150. https://doi.org/10.1007/s002249910009
• N. Robertson and P. D. Seymour, Graph minors. X. Obstructions to tree-decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-N

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) was one of the first systematic worst-case analyses of polynomial-time heuristics for NP-complete optimization problems. Its Section 5 proves the harmonic bound $\sum_{j=1}^k 1/j$ for the greedy algorithm on minimum-cardinality set cover, a result that still underlies the standard $\ln n$ approximation guarantee.

Section 6, the subject of this mission, asks what happens when the cost of a cover is its total size rather than its number of sets. This problem, SET COVERING II (EC), is the optimization version of the EXACT COVER recognition problem of Karp's list (Karp 1972): a family has a disjoint subcover exactly when the optimum equals the number of covered points. Johnson shows that the change of measure breaks the cardinality greedy but that a greedy rule based on an overlap ratio recovers essentially the same guarantee. The same accounting (paying for each newly covered point) later became the standard analysis of greedy weighted set cover (Chvátal 1979).

Setting

An input is a finite family $F = \{S_1, \dots, S_p\}$ of finite sets. Its covered set is $T = \bigcup_{S \in F} S$. A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S\in F'} S = T$, and its measure is

$$m_{EC}(F') = \sum_{S \in F'} |S|.$$

The optimum $F^*$ is the least measure of a subcover; since every subcover has measure at least $|T|$, an optimal subcover is one with the least possible overlapping. The subproblem EC$(k)$ admits only families in which every set has at most $k$ points.

Algorithm C2 keeps a subfamily SUB (initially empty), the unused sets LEFT (initially $F$) and the uncovered points UNCOV (initially $T$). While UNCOV is nonempty it chooses $S' \in$ LEFT minimizing

$$\mathrm{Ratio}(S) = \frac{|S - \mathrm{UNCOV}|}{|S \cap \mathrm{UNCOV}|},$$

the number of already-covered points of $S$ per newly covered point, and moves $S'$ from LEFT to SUB, removing its points from UNCOV. When several sets tie, any of them may be chosen; a subcover is choosable by C2 if some sequence of admissible choices returns it.

The overlap of a chosen set is $|S' - \mathrm{UNCOV}|$ at the moment it is chosen, and the cumulative overlap $\mathrm{OV}(F_1)$ of a run returning $F_1$ is the sum of these overlaps.

Formalization targets

Goal: Theorem 6 (p. 271)

For all $k \ge 1$ and $n > 0$,

$$R[C2, EC(k)](n) \le 1 + \ln(k) \le \sum_{j=1}^k \frac1j + \frac12,$$

and for all sufficiently large $n$, $R[C2, EC(k)](n) \ge \sum_{j=1}^k (1/j)$. In the size-free form used here, for every $k \ge 1$:

1. every subcover $M$ choosable by C2 on an input of EC$(k)$ satisfies $m_{EC}(M) \le (1 + \ln k)\,F^*$;
2. $1 + \ln k \le \sum_{j=1}^k 1/j + 1/2$;
3. some input of EC$(k)$ with $F^* > 0$ has a choosable subcover with $m_{EC}(M) \ge \big(\sum_{j=1}^k 1/j\big) F^*$.

Milestones (proof of Theorem 6, pp. 271–272)

• the measure of the output is $|T| + \mathrm{OV}(F_1)$;
• if C2 may choose a set with $\mathrm{Ratio}(S') \ge y$, then $(y+1)\,|\mathrm{UNCOV}| \le F^*$;
• with $a = F^*/|T|$ and $x = |T - \mathrm{UNCOV}|/|T|$, the next chosen set has $\mathrm{Ratio}(S') \le a/(1-x) - 1$;
• on EC$(k)$, $\mathrm{OV}(F_1) \le |T|\,(a[\ln(k) + 1] - 1)$;
• the analytic inequality $1 + \ln(k) \le \sum_{j=1}^k 1/j + 1/2$;
• the lower-bound input (Fig. 1 of the paper with every set of $F_1$ filled out to exactly $k$ points) on which C2 may pay $\sum_{j=1}^k 1/j$ times the optimum.

Significance

The result. The measure $\sum|S|$ penalizes overlap, and the paper notes (without proof, p. 270) that an algorithm returning an optimal cover for the cardinality measure can be a factor $k$ from optimal for this one. Theorem 6 shows that the ratio rule C2 is within $1 + \ln k$ of the least-overlap cover, and the lower bound shows that no analysis of C2 can beat $\sum_{j=1}^k 1/j$. The two bounds differ by less than $1/2$ for every $k$. The theorem was an early instance of a logarithmic guarantee for a weighted covering problem, where each set's cost is its size.

Formalizing it. The theorem has been proved since 1974; no machine-checked proof is known to exist. The mission produces a formal model of the EC problem and of C2 as a nondeterministic process, the overlap identity, and the discrete form of the paper's area-under-a-curve estimate. The last is the part the paper argues informally, through a step function and an integral.

Difficulty

The cardinality argument for C1 counts the sets chosen; here the sets have different sizes, so it does not apply. The overlap C2 pays per newly covered point is not bounded by a constant: early choices can be free and late ones cost up to $k-1$ per point, and the bound on the cumulative overlap must hold against the whole run, for every sequence of tie-breaks.

In a formal proof the integral must be replaced by a sum. Covered points arrive in blocks (one block per chosen set), the charge is constant on a block but the bound depends on the covered fraction at the start of the block, and the sum has to be compared with a logarithm. The terms $a\ln a$ and $a/k$ that the paper drops using $1 \le a \le k$ must be controlled as well, and the relation $1 \le a \le k$ must itself be proved from optimality. The lower bound needs an explicit run of C2 through ties on an input with $k \cdot k!$ points, checking at every stage that the intended set is a ratio minimizer.

Formalization scope

• Inputs. A family is p : ℕ with S : Fin p → Finset α (0-based, repetitions allowed; a repeated set counts twice in the measure if both copies are chosen, which C2 never does). Subcovers and SUB, LEFT are index sets. $F^*$ is a minimum over the finite, nonempty set of subcovers (Finset.inf'), never a junk value.
• Algorithm. C2 is a step relation on states (SUB, LEFT, UNCOV). The choice at Step 3 is existential over all minimizers, so every result quantifies over every choosable output (the paper's WORST). $\mathrm{Ratio}(S)$ is $+\infty$ when $S \cap \mathrm{UNCOV} = \emptyset$; the formal rule requires the chosen set to meet UNCOV and compares ratios by cross-multiplication, with no division.
• Overlap. The cumulative overlap depends on the run, not on the output alone, so it is carried by an inductive run relation RunOV.
• No problem size. The paper's $R[A, P](n)$ maximizes over inputs of size at most $n$ in an unspecified encoding. Upper bounds are stated for every input and every choosable output; the lower bound exhibits one input and one choosable output. Given monotonicity of $R$ in $n$, these are equivalent to the paper's claims. Ratios are stated multiplicatively, so $F^* = 0$ does not create a vacuous bound.
• Numbers. Measures are natural numbers cast to $\mathbb R$; $\ln$ is Real.log; $\sum_{j=1}^k 1/j$ is Mathlib's harmonic k.
• Ruled out. A deterministic tie-break would prove a weaker upper bound and could not realize the lower-bound run, and a ratio with $x/0 = 0$ would make disjoint-from-UNCOV sets the most attractive choice. The formalization uses neither.

The overlap identity and the discrete integral comparison are reusable for any greedy covering analysis that charges cost per newly covered point. Contributions welcome include proofs of the milestones, the invariants of the C2 run relation (SUB and LEFT partition the indices; UNCOV $= T - \bigcup$ SUB), and the explicit lower-bound run.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233

Motivation

Many problems in signal processing, statistics and function interpolation ask for a solution of a linear system $Ax\approx b$ that uses as few columns of $A$ as possible: a sparse approximate solution. Natarajan's 1995 paper Sparse Approximate Solutions to Linear Systems (SIAM J. Comput. 24(2):227–234) was motivated by radial basis interpolation, where each column corresponds to a basis function and fewer columns mean a cheaper interpolant. The paper does two things. It proves that finding the sparsest approximate solution is computationally hard (§2, Theorem 1), and it analyses a greedy column-selection algorithm whose number of chosen columns is within a factor, depending on the conditioning of $A$, of the optimum (§3, Theorem 2; a separate mission of this series).

The hardness theorem is the reason the second half of the paper exists: once exact minimization is ruled out, one settles for approximation guarantees. It is cited throughout the compressed-sensing literature as the canonical statement that $\ell_0$-minimization under an $\ell_2$ error constraint is NP-hard, and is the starting point for the later theory of when convex relaxations recover sparse solutions.

The argument follows the classical reduction from Exact Cover by 3-sets (X3C) to minimum-weight solutions of linear systems in Garey and Johnson (1979), pp. 221 and 246, adapted to an approximate right-hand side.

Setting

Sparse approximate solution (SAS). Given a matrix $A\in\mathbb R^{m\times n}$, a vector $b\in\mathbb R^m$ and a tolerance $\varepsilon>0$, find a vector $x\in\mathbb R^n$ with $\|Ax-b\|_2\le\varepsilon$ whose number of nonzero entries, written $\|x\|_0=|\{j : x_j\neq0\}|$, is as small as possible. Here $\|\cdot\|_2$ is the Euclidean norm.

Exact Cover by 3-sets (X3C). An instance is a ground set $S=\{s_1,\dots,s_m\}$ and a list $C=c_1,\dots,c_n$ of subsets of $S$, each with exactly three elements. An exact cover is a sub-collection $\hat C=\{c_j : j\in J\}$, $J\subseteq\{1,\dots,n\}$, such that every element of $S$ occurs in exactly one set of $\hat C$.

The transformation. From an X3C instance build the SAS instance with

• the incidence matrix $A\in\mathbb R^{m\times n}$: $A_{ij}=1$ if $s_i\in c_j$ and $A_{ij}=0$ otherwise, so column $j$ is the characteristic vector of $c_j$;
• the all-ones vector $b=(1,1,\dots,1)\in\mathbb R^m$;
• the tolerance $\varepsilon=\tfrac12$.

In Lean, $S$ is Fin m, the collection is C : Fin n → Finset (Fin m) with hC : ∀ j, (C j).card = 3, an exact cover is an index set J with IsExactCover C J, the matrix is incidence C, the vector $b$ is onesVec m, $Ax$ is Matrix.toEuclideanLin (incidence C) x, and $\|x\|_0$ is nnz x.

Formalization targets

Goal: correctness of the reduction

For every X3C instance $(S,C)$ as above,

$$\bigl(\exists J,\ \{c_j\}_{j\in J}\text{ is an exact cover of }S\bigr)\iff\bigl(\exists x\in\mathbb R^n,\ \|Ax-b\|_2\le\tfrac12\ \text{and}\ 3\,\|x\|_0\le m\bigr).$$

This is the sentence the proof of Theorem 1 (p. 228) establishes: "the constructed instance of SAS has a solution with $m/3$ or fewer entries if and only if the given instance of X3C has a solution."

Milestones

1. Forward direction. If $\{c_j\}_{j\in J}$ is an exact cover, the indicator vector $x=\mathbf 1_J$ satisfies $Ax=b$ and $3\|x\|_0=m$.
2. Entry bounds. For every $x$ with $\|Ax-b\|_2\le\frac12$, each entry of $Ax$ lies in $[\frac12,\frac32]$.
3. Lower bound on sparsity. For every such $x$, $m\le3\|x\|_0$.
4. Exact cover from a sparse solution. If moreover $3\|x\|_0\le m$, the sets $c_j$ with $x_j\neq0$ form an exact cover.

Significance

The result. The equivalence shows that deciding whether a sparse approximate solution with a prescribed number of nonzeros exists is at least as hard as X3C, which is NP-complete. Consequently no polynomial-time algorithm computes the optimum of SAS unless P = NP, and approximation algorithms such as the greedy method of §3 are the natural object of study. The same instance shows hardness persists for 0/1 matrices, a right-hand side of all ones and a constant tolerance, so the difficulty does not come from ill-conditioned data or from vanishing precision.

Formalizing it. The reduction is proved in the paper; this mission produces a machine-checked proof of its correctness, the combinatorial core of every NP-hardness claim for $\ell_0$-constrained least squares. No prior machine-checked version is known to exist, on the platform or elsewhere. The complexity-theoretic wrapper is out of scope (see below).

Difficulty

The forward direction is a direct computation. The converse contains the only real step, which the paper passes over with "it is clear". From $\|Ax-b\|_2\le\frac12$ one gets only that every entry of $Ax$ is in $[\frac12,\frac32]$; the entries of $x$ themselves are arbitrary reals, possibly negative or not equal to $1$, so $x$ need not be an indicator vector and $Ax=b$ need not hold. The exact-cover property must therefore be extracted from support sizes alone: every element is covered by some column in the support, the support has at most $m/3$ columns of three elements each, and a counting argument forces the chosen sets to be pairwise disjoint. Reading off a cover from the values of $x$ (for instance, taking the $j$ with $x_j=1$) does not work.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin m) and EuclideanSpace ℝ (Fin n), so ‖·‖ is the paper's $\|\cdot\|_2$. Using the sup norm of Fin m → ℝ would give a different statement.
• The tolerance is exactly $\varepsilon=\frac12$, as printed.
• The collection is indexed, C : Fin n → Finset (Fin m): repeated sets are allowed and are distinct indices; an exact cover is a set of indices, and on the SAS side one nonzero entry is counted per index, so both sides treat duplicates consistently.
• "$m/3$ or fewer" is written $3\|x\|_0\le m$, never with natural-number division. With this form the equivalence holds for every $m$ (both sides are false when $3\nmid m$), which absorbs the paper's "without loss of generality $m$ is a multiple of 3"; no divisibility hypothesis is assumed. For $m=0$ both sides are true.
• The hypothesis that every set has exactly three elements is essential for the converse (with $m=9$, $O=\{s_3,\dots,s_9\}$, $c_1=\{s_1\}\cup O$, $c_2=\{s_2\}\cup O$, $c_3=O$, the vector $x=(1,1,-1)$ solves $Ax=b$ with $3\|x\|_0=m$, yet $C$ has no exact cover since $c_1$ and $c_2$ must both be chosen) and is kept as hC.
• Not formalized: the infinite-precision RAM machine model, polynomial-time many-one reductions, polynomial-time computability of the transformation (evident: an $m\times n$ 0/1 matrix), and the NP-completeness of X3C (cited by the paper from Garey–Johnson). The goal is therefore the correctness of the transformation, not a statement titled "SAS is NP-hard". A statement that only records the forward direction, or that fixes $x$ to be a 0/1 vector on the SAS side, would trivialize the converse and is not the target.
• Tools a solver will need are in Mathlib: coordinate bounds for the Euclidean norm (PiLp.norm_apply_le), Finset.card_biUnion_le, and Finset.card_biUnion for disjoint unions. Contributions of a reusable exact-cover API, or of a polynomial-time reduction framework that could later wrap this equivalence into an NP-hardness theorem, are welcome.

Selected references

• B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM Journal on Computing 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (X3C: problem [SP2], p. 221; minimum weight solution to linear equations: [MP5], p. 246).
• F. P. Preparata and M. I. Shamos, Computational Geometry: An Introduction, Springer, 1985 (the real RAM model). https://doi.org/10.1007/978-1-4612-1098-6