Sang-il Oum엄상일

Abstract

A connectivity function on a finite set $E$ is a function $f\colon 2^E\to\mathbb Z$ that is submodular and symmetric, with $f(\varnothing)=0$. Given a connectivity function $f$ via a value oracle, terminals $t_1,\ldots,t_r\in E$, and an integer $k$, the Multiway $f$-Cut problem asks whether $E$ has a partition $(P_1,\ldots,P_r)$ with $t_i\in P_i$ for every $i$ and $\sum_{i=1}^r f(P_i)\le k$. We prove that Multiway $f$-Cut is fixed-parameter tractable parameterized by $k$. Cut functions of graphs are connectivity functions, so as a special case we recover the classical result that Edge Multiway Cut in graphs is fixed-parameter tractable. Our proof of correctness is completely elementary, and is arguably the simplest known proof of this fact.

Abstract

Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. The compiler treats the external semidefinite programming output as candidate data rather than trusted input: Lean independently computes the required density and multiplication facts, verifies positive semidefiniteness exactly over $\mathbb{Q}$, and carries out the algebraic normalization steps of flag-algebra proofs. Our case studies yield formal proofs of seven Turán-type upper bounds, including Mantel's theorem and the Erdős pentagon theorem, a $C_4$-density bound for triangle-free graphs, and edge-density bounds for $K_4$-free, $K_5$-free, and $C_5$-free graphs. Independently of the compiler, we formalize the matching constructions that complete the exact Turán densities of Mantel's theorem and the Erdős pentagon theorem, and prove two inequalities of Goodman. Our constrained semantics also prompted a meta-theoretic comparison of two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We state the resulting root-plantability criterion characterizing when the two approaches agree; a forthcoming paper will present the complete account.

Abstract

We determine both the excluded vertex-minors and the excluded pivot-minors for the class of graphs of rank-width at most two. Up to local equivalence and graph isomorphism, there are exactly 25 excluded vertex-minors: 1 graph on 8 vertices, 18 on 9 vertices, and 6 on 10 vertices. Up to pivot equivalence and graph isomorphism, there are exactly 609 excluded pivot-minors: 2 on 8 vertices, 447 on 9 vertices, 146 on 10 vertices, 10 on 11 vertices, and 4 on 12 vertices. No excluded vertex-minor occurs on 11--16 vertices, and no excluded pivot-minor occurs on 13--16 vertices; the author's 16-vertex bound makes both lists complete. The proof is computer-assisted. Instead of enumerating all graphs, we reverse the one-vertex reduction theorem for prime graphs. For each n, we retain exactly the prime n-vertex graphs of rank-width at most two, modulo local equivalence and isomorphism, and extend those graphs by one vertex. Local-equivalence classes are identified by an exact canonical key obtained from the associated isotropic system, the binary row space of [I|A(G)]. A restricted version of the same key classifies pivot equivalence exactly. The vertex-minor and pivot-minor computations examine, respectively, more than 9.0×10^10 and 4.9×10^11 prime extensions in their 16-vertex final layers.