Quantitative bounds for the paired-port compiler

The actual output fits the unchanged 240-macrocell grid, with linear grid sides and quadratic clause, literal, route, segment, and Manhattan-wire costs. Bounds concern the emitted lists and all their integer points; geometric separation is proved separately.

Main results

• drawing_fits, gridWidth_le, gridHeight_le: the actual drawing fits a linear grid.
• length_routes, drawingSegmentCount_eq, drawingWireLength_eq: exact output costs.
• routes_length_le, drawingSegmentCount_le, drawingWireLength_le: quadratic bounds.

References

The unchanged path and grid estimates are reused from Planar.Size and Planar.Bounds.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.gridWidth (φ : Logic.PL.CNF ℕ) : ℕ

The unchanged horizontal side of the 240-macrocell drawing.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.gridHeight (φ : Logic.PL.CNF ℕ) : ℕ

The unchanged vertical side of the 240-macrocell drawing.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.drawing_fits (φ : Logic.PL.CNF ℕ) : Graph.drawingFits (positions φ, routes φ) (gridWidth φ) (gridHeight φ)

Every actual vertex and route point lies in the explicit nonnegative grid rectangle. This quantitative statement does not assert geometric separation.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.gridWidth_le (φ : Logic.PL.CNF ℕ) : gridWidth φ ≤ 1920 * (φ.numVars + List.length φ + φ.vars.length + 1)

The horizontal grid side is linear in source incidence size.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.gridHeight_le (φ : Logic.PL.CNF ℕ) : gridHeight φ ≤ 1920 * (φ.numVars + List.length φ + φ.vars.length + 1)

The vertical grid side is linear in source incidence size.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_positions (φ : Logic.PL.CNF ℕ) : (positions φ).length = (rawFormula φ).numVars + List.length (formula φ)

The position list contains the distinct structured variables followed by all output clauses.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.positions_length_le (φ : Logic.PL.CNF ℕ) : (positions φ).length ≤ 15000 * (φ.numVars + List.length φ + φ.vars.length + 1) ^ 2

The total number of output vertex positions is explicitly quadratic.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_routes (φ : Logic.PL.CNF ℕ) : (routes φ).length = φ.vars.length + 16 * (ordinaryCells φ).length + 162 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ

Exact route count, one per output literal position.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.drawingSegmentCount_eq (φ : Logic.PL.CNF ℕ) : Graph.drawingSegmentCount (positions φ, routes φ) = 3 * φ.vars.length + 16 * (ordinaryCells φ).length + 407 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ

Exact number of listed incidence-route segments: three per source literal, sixteen per ordinary ring, 407 per paired crossover, and four per retained path gap.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.drawingWireLength_eq (φ : Logic.PL.CNF ℕ) : Graph.drawingWireLength (positions φ, routes φ) = 150 * φ.vars.length + 800 * (ordinaryCells φ).length + 2192 * (crossingSites φ).length + 80 * PlanarCompile.linkCount φ

Exact Manhattan wire length of the actual drawing data.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.routes_length_le (φ : Logic.PL.CNF ℕ) : (routes φ).length ≤ 10000 * (φ.numVars + List.length φ + φ.vars.length + 1) ^ 2

The actual route count is quadratically bounded in source incidence size.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.drawingSegmentCount_le (φ : Logic.PL.CNF ℕ) : Graph.drawingSegmentCount (positions φ, routes φ) ≤ 12000 * (φ.numVars + List.length φ + φ.vars.length + 1) ^ 2

The actual segment count is quadratically bounded in source incidence size.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.drawingWireLength_le (φ : Logic.PL.CNF ℕ) : Graph.drawingWireLength (positions φ, routes φ) ≤ 400000 * (φ.numVars + List.length φ + φ.vars.length + 1) ^ 2

The actual Manhattan wire length is quadratically bounded in source incidence size.