diff --git a/Complexity.lean b/Complexity.lean index 56d0bd1da..8f0059f02 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -812,13 +812,17 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverL public import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry public import Complexity.Computability.Complexity.Problems.SAT.Planar.Occurrence public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRing +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedBounds public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCorrectness public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCounting public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayout public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutChecks public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutData +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedOccurrence +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedPolyTime public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedSemantics +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedSize public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedBounds.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedBounds.lean new file mode 100644 index 000000000..3bda2d423 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedBounds.lean @@ -0,0 +1,541 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedSize +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds +public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing +import Complexity.Computability.Complexity.Problems.SAT.Planar.PathGeometry +import Complexity.Computability.Complexity.Problems.Graph.OrthogonalPath +import Mathlib.Data.List.GetD +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.SplitIfs + +/-! +# 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`. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- The unchanged horizontal side of the 240-macrocell drawing. -/ +abbrev gridWidth := PlanarCompile.gridWidth + +/-- The unchanged vertical side of the 240-macrocell drawing. -/ +abbrev gridHeight := PlanarCompile.gridHeight + +private def CellBound (φ : CNF ℕ) (p : Point) : Prop := + 0 ≤ p.1 ∧ p.1 ≤ 8 * ((SAT.incidenceGraph φ).1.length : ℤ) ∧ + 0 ≤ p.2 ∧ p.2 ≤ 8 * ((SAT.incidenceGraph φ).1.length : ℤ) + + 2 * (SAT.incidenceGraph φ).2.length + +private def OutputBound (φ : CNF ℕ) (p : Point) : Prop := + 0 ≤ p.1 ∧ p.1 ≤ gridWidth φ ∧ 0 ≤ p.2 ∧ p.2 ≤ gridHeight φ + +private theorem outputBound_add {φ : CNF ℕ} {p a : Point} (hp : CellBound φ p) + (ha : 0 ≤ a.1 ∧ a.1 ≤ 240 ∧ 0 ≤ a.2 ∧ a.2 ≤ 240) : + OutputBound φ (cellOrigin 120 p + a) := by + simp only [OutputBound, gridWidth, gridHeight, PlanarCompile.gridWidth, PlanarCompile.gridHeight, + Prod.fst_add, Prod.snd_add, cellOrigin, Nat.cast_mul, Nat.cast_add, Nat.cast_ofNat] + dsimp only [CellBound] at hp + norm_num at * + constructor + · nlinarith [hp.1, ha.1] + constructor + · nlinarith [hp.2.1, ha.2.1] + constructor <;> nlinarith [hp.2.2.1, hp.2.2.2, ha.2.2.1, ha.2.2.2] + +private theorem cellBound_path {φ : CNF ℕ} {r : Route} (hr : r ∈ paths φ) + {p : Point} (hp : p ∈ r) : CellBound φ p := by + change r ∈ (SAT.incidenceGraph φ).unitPaths at hr + obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr + have hi' : i < (SAT.incidenceGraph φ).2.length := by simpa using hi + have hp' : p ∈ (SAT.incidenceGraph φ).unitPath i := by + simpa only [Graph.unitPath, List.getD_eq_getElem _ _ hi] using hp + exact Graph.unitPath_bounds _ (fun _ he => SAT.incidenceGraph_endpoints he) + (fun _ he => SAT.incidenceGraph_loopless he) hi' hp' + +private theorem cellBound_occurrencePath {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∈ occurrencePath φ o) : + CellBound φ p := by + have hi : (Cslib.Logic.PL.occurrences φ).idxOf o < (paths φ).length := by + rw [PlanarCompile.paths_length, ← Cslib.Logic.PL.length_occurrences] + exact List.idxOf_lt_length_of_mem ho + apply cellBound_path (r := occurrencePath φ o) _ hp + change (paths φ).getD ((Cslib.Logic.PL.occurrences φ).idxOf o) [] ∈ paths φ + rw [List.getD_eq_getElem _ _ hi] + exact List.getElem_mem hi + +private theorem cellBound_crossing {φ : CNF ℕ} {p : Point} (hp : p ∈ crossingSites φ) : + CellBound φ p := by + have hlen := (PlanarCompile.mem_crossingSites φ p).mp hp |>.2.2 + have hnonempty : ((paths φ).filter fun r => r.contains p) ≠ [] := by + intro he + rw [he] at hlen + simp at hlen + obtain ⟨r, hr⟩ := List.exists_mem_of_ne_nil _ hnonempty + obtain ⟨hr, hp⟩ := List.mem_filter.mp hr + exact cellBound_path hr (List.contains_iff_mem.mp hp) + +private theorem cellBound_clause {φ : CNF ℕ} {i : ℕ} (hi : i < φ.length) : + CellBound φ (Layout.center (φ.distinctVars.length + i)) := by + have hn : φ.distinctVars.length + i < (SAT.incidenceGraph φ).1.length := by + simp only [SAT.length_vertices_incidenceGraph, CNF.length_distinctVars] + omega + simp only [CellBound, Layout.center, Nat.cast_add] + omega + +private theorem crossover_variable_bounds : ∀ v, + 20 ≤ (PairedCrossover.variablePosition v).1 ∧ (PairedCrossover.variablePosition v).1 ≤ 220 ∧ + 20 ≤ (PairedCrossover.variablePosition v).2 ∧ (PairedCrossover.variablePosition v).2 ≤ 220 := + by decide +kernel + +private theorem crossover_clause_bounds : ∀ p ∈ PairedCrossover.clausePositions, + 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel + +private theorem crossover_core_bounds : ∀ e ∈ PairedCrossover.incidenceRoutes, ∀ p ∈ e.2.2, + 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel + +private theorem outputBound_variable {φ : CNF ℕ} {v : Variable} (hv : CellBound φ v.1) : + OutputBound φ (variablePosition v) := by + apply outputBound_add hv + cases h : v.2 with + | inl w => + have hw := PairedPorts.variable_bounds w.1 w.2 + simp only [Sum.elim_inl] + omega + | inr w => + have hw := crossover_variable_bounds w + simp only [Sum.elim_inr] + omega + +private theorem outputBound_center {φ : CNF ℕ} {p : Point} (hp : CellBound φ p) : + OutputBound φ (center p) := outputBound_add hp (by norm_num) + +private theorem outputBound_boundary {φ : CNF ℕ} {p : Point} (hp : CellBound φ p) + (s : Fin 4) (lane : Fin 2) : OutputBound φ (boundary p s lane) := by + unfold boundary + apply outputBound_add hp + fin_cases s <;> fin_cases lane <;> decide + +private theorem outputBound_access {φ : CNF ℕ} (sites : List Point) {p q a : Point} + (hp : CellBound φ p) (lane : Fin 2) (ha : a ∈ access sites p q lane) : + OutputBound φ a := by + simp only [access, List.mem_cons, List.not_mem_nil, or_false] at ha + rcases ha with rfl | rfl + · exact outputBound_boundary hp _ _ + · exact outputBound_variable hp + +private theorem lastLiteral_bounds {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) (sites : List Point) : + OutputBound φ (variablePosition (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1) ∧ + ∀ a ∈ (lastLiteral sites (occurrencePath φ o) o.2.2.2).2, OutputBound φ a := by + let r := occurrencePath φ o + have hlen : 2 ≤ r.length := PlanarCompile.occurrencePath_length_ge_two ho + have hp : CellBound φ (r.getD (r.length - 2) (0, 0)) := by + apply cellBound_occurrencePath ho + rw [List.getD_eq_getElem _ _ (show r.length - 2 < r.length by omega)] + exact List.getElem_mem _ + have hq : CellBound φ (r.getLastD (0, 0)) := by + rw [List.getLastD_eq_getLast?, (PlanarCompile.occurrencePath_endpoints ho).2, + Option.getD_some] + exact cellBound_clause (Cslib.Logic.PL.mem_occurrences.mp ho).1 + constructor + · exact outputBound_variable hp + · intro a ha + simp only [lastLiteral, List.mem_cons, List.not_mem_nil, or_false] at ha + rcases ha with rfl | rfl | rfl | rfl + · exact outputBound_center hq + · apply outputBound_add hq + generalize side (r.getLastD (0, 0)) (r.getD (r.length - 2) (0, 0)) = s + fin_cases s <;> decide + · exact outputBound_boundary hq _ _ + · exact outputBound_variable hp + +private def ClauseBound (φ : CNF ℕ) (pc : PlacedClause) : Prop := + OutputBound φ pc.2.1 ∧ + (∀ l ∈ pc.1, OutputBound φ (variablePosition l.1)) ∧ + ∀ r ∈ pc.2.2, ∀ a ∈ r, OutputBound φ a + + +private theorem originalClauses_bounds (φ : CNF ℕ) (sites : List Point) : + ∀ pc ∈ originalClauses φ sites, ClauseBound φ pc := by + intro pc hpc + obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc + refine ⟨outputBound_center (cellBound_clause (List.mem_zipIdx' hci).1), ?_, ?_⟩ + · intro l hl + obtain ⟨lr, hlr, rfl⟩ := List.mem_map.mp hl + obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr + have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := + List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ + exact (lastLiteral_bounds ho sites).1 + · intro r hr a ha + obtain ⟨lr, hlr, rfl⟩ := List.mem_map.mp hr + obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr + have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := + List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ + exact (lastLiteral_bounds ho sites).2 a ha + +private theorem ordinaryClauses_bounds {φ : CNF ℕ} {p : Point} (hp : CellBound φ p) : + ∀ pc ∈ ordinaryClauses p, ClauseBound φ pc := by + intro pc hpc + obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc + refine ⟨?_, ?_, ?_⟩ + · apply outputBound_add hp + have hi : ci.2 < OrdinaryRing.clausePositions.length := by + rw [OrdinaryRing.drawing_sizes.1] + exact (OrdinaryRing.formula_sizes.1 ▸ (List.mem_zipIdx' hci).1) + have hb := OrdinaryRing.clause_bounds _ (List.getElem_mem hi) + rw [List.getD_eq_getElem _ _ hi] + omega + · intro l hl + obtain ⟨v, _, rfl⟩ := List.mem_map.mp hl + exact outputBound_variable hp + · intro r hr a ha + obtain ⟨e, he, rfl⟩ := List.mem_map.mp hr + obtain ⟨b, hb, rfl⟩ := List.mem_map.mp ha + rw [add_comm] + apply outputBound_add hp + have h := OrdinaryRing.core_bounds e (List.mem_filter.mp he).1 b hb + omega + +private theorem crossingClauses_bounds {φ : CNF ℕ} {p : Point} (hp : CellBound φ p) : + ∀ pc ∈ crossingClauses p, ClauseBound φ pc := by + intro pc hpc + obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc + refine ⟨?_, ?_, ?_⟩ + · apply outputBound_add hp + have hi : ci.2 < PairedCrossover.clausePositions.length := by + rw [show PairedCrossover.clausePositions.length = 78 by decide +kernel] + exact (PairedCrossover.length_formula ▸ (List.mem_zipIdx' hci).1) + have hb := crossover_clause_bounds _ (List.getElem_mem hi) + rw [List.getD_eq_getElem _ _ hi] + omega + · intro l hl + obtain ⟨v, _, rfl⟩ := List.mem_map.mp hl + exact outputBound_variable hp + · intro r hr a ha + obtain ⟨e, he, rfl⟩ := List.mem_map.mp hr + obtain ⟨b, hb, rfl⟩ := List.mem_map.mp ha + rw [add_comm] + apply outputBound_add hp + have h := crossover_core_bounds e (List.mem_filter.mp he).1 b hb + omega + + +private theorem link_bounds {φ : CNF ℕ} (sites : List Point) (lane : Fin 2) {p q : Point} + (hp : CellBound φ p) (hq : CellBound φ q) : ClauseBound φ (link sites p q lane) := by + have hvp := outputBound_variable (v := signal sites p q lane) hp + have hvq := outputBound_variable (v := signal sites q p lane) hq + refine ⟨outputBound_boundary hp _ _, ?_, ?_⟩ + · intro l hl + by_cases h : lane = 0 <;> + simp only [link, h, ite_true, ite_false, List.mem_cons, + List.not_mem_nil, or_false] at hl hvp hvq <;> + rcases hl with rfl | rfl <;> assumption + · intro r hr a ha + by_cases h : lane = 0 <;> + simp only [link, h, ite_true, ite_false, List.mem_cons, + List.not_mem_nil, or_false] at hr <;> + rcases hr with rfl | rfl + all_goals + first + | exact outputBound_access sites hp _ ha + | exact outputBound_access sites hq _ ha + +private theorem cellBound_ordinary {φ : CNF ℕ} {p : Point} (hp : p ∈ ordinaryCells φ) : + CellBound φ p := by + have hmem : p ∈ (paths φ).flatMap List.dropLast ∧ p ∉ crossingSites φ := by + simpa [ordinaryCells, mem_selectDistinct_replicate] using hp + obtain ⟨r, hr, hp⟩ := List.mem_flatMap.mp hmem.1 + exact cellBound_path hr ((List.dropLast_subset _) hp) + +private theorem placedClauses_bounds (φ : CNF ℕ) : + ∀ pc ∈ placedClauses φ, ClauseBound φ pc := by + intro pc hpc + simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc + rcases hpc with ((hpc | ⟨p, hp, hpc⟩) | ⟨p, hp, hpc⟩) | ⟨o, ho, hpc⟩ + · exact originalClauses_bounds φ _ pc hpc + · exact ordinaryClauses_bounds (cellBound_ordinary hp) pc hpc + · exact crossingClauses_bounds (cellBound_crossing hp) pc hpc + · obtain ⟨e, he, hpc⟩ := List.mem_flatMap.mp hpc + have he' := List.of_mem_zip he + have hp := cellBound_occurrencePath ho ((List.dropLast_subset _) he'.1) + have hq := cellBound_occurrencePath ho + ((List.dropLast_subset _) (List.mem_of_mem_tail he'.2)) + simp only [List.mem_cons, List.not_mem_nil, or_false] at hpc + rcases hpc with rfl | rfl <;> exact link_bounds _ _ hp hq + +/-- Every actual vertex and route point lies in the explicit nonnegative grid rectangle. +This quantitative statement does not assert geometric separation. -/ +theorem drawing_fits (φ : CNF ℕ) : + Graph.drawingFits (positions φ, routes φ) (gridWidth φ) (gridHeight φ) := by + constructor + · intro p hp + rcases List.mem_append.mp hp with hp | hp + · obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hp + obtain ⟨c, hc, b, hv⟩ := CNF.mem_vars.mp (CNF.mem_distinctVars.mp hv) + obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hc + exact (placedClauses_bounds φ pc hpc).2.1 (v, b) hv + · obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hp + exact (placedClauses_bounds φ pc hpc).1 + · intro r hr p hp + obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr + exact (placedClauses_bounds φ pc hpc).2.2 r hr p hp + +/-- The horizontal grid side is linear in source incidence size. -/ +theorem gridWidth_le (φ : CNF ℕ) : + gridWidth φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := + PlanarCompile.gridWidth_le φ + +/-- The vertical grid side is linear in source incidence size. -/ +theorem gridHeight_le (φ : CNF ℕ) : + gridHeight φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := + PlanarCompile.gridHeight_le φ + +/-- The position list contains the distinct structured variables followed by all output clauses. -/ +theorem length_positions (φ : CNF ℕ) : + (positions φ).length = (rawFormula φ).numVars + (formula φ).length := by + simp [positions, CNF.length_distinctVars, formula, rawFormula] + +/-- The total number of output vertex positions is explicitly quadratic. -/ +theorem positions_length_le (φ : CNF ℕ) : + (positions φ).length ≤ 15000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by + have hv := (rawFormula φ).numVars_le_length_vars + have hf := length_formula_le φ + have hl := length_vars_formula_le φ + rw [length_positions] + rw [length_vars_rawFormula, ← length_vars_formula] at hv + omega + +private theorem cost_signal_position (sites : List Point) (p q : Point) (l : Fin 2) : + variablePosition (signal sites p q l) = + cellOrigin 120 p + PairedPorts.variablePosition (side p q) l := by + simp only [signal, port, variablePosition] + split_ifs <;> rfl + +/-- Actual accesses are translations of the fixed paired-port accesses. -/ +private theorem cost_access_eq_translate (sites : List Point) (p q : Point) (l : Fin 2) : + access sites p q l = translate (cellOrigin 120 p) (PairedPorts.accessRoute (side p q) l) := by + rw [access, cost_signal_position] + simp only [boundary, PairedPorts.accessRoute, translate, List.map_cons, List.map_nil] + simp only [add_comm] + +private def finalLocalRoute (s : Fin 4) : Route := + [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s), + cellOrigin 120 (PairedPorts.neighbor s) + + PairedPorts.variablePosition (PairedPorts.oppositeSide s) (PairedPorts.spokeLane s)] + +private theorem finalRoute_eq_translate (sites : List Point) {p q : Point} + (h : Orthogonal.length p q = 1) : + [center q, cellOrigin 120 q + PairedPorts.spokeElbow (side q p), + boundary q (side q p) (PairedPorts.spokeLane (side q p)), + variablePosition (signal sites p q (PairedPorts.spokeLane (side q p)))] = + translate (cellOrigin 120 q) (finalLocalRoute (side q p)) := by + rw [cost_signal_position] + have hrev : Orthogonal.length q p = 1 := by + simp only [Orthogonal.length] at h ⊢ + omega + rcases q with ⟨x, y⟩ + rcases PlanarCompile.unit_neighbor_cases hrev with rfl | rfl | rfl | rfl <;> + simp [translate, finalLocalRoute, side, PlanarCompile.side, center, PlanarCompile.center, + boundary, cellOrigin, PairedPorts.neighbor, PairedPorts.oppositeSide, + PairedPorts.variablePosition, PairedPorts.boundaryPort, PairedPorts.spokeLane, + PairedPorts.spokeElbow, PairedPorts.offset, Prod.ext_iff] <;> omega + +private theorem original_route_count (φ : CNF ℕ) (sites : List Point) : + ((originalClauses φ sites).map fun c => c.2.2.length).sum = φ.vars.length := by + rw [CNF.length_vars] + simp only [originalClauses, List.map_map, Function.comp_def, List.length_map, + List.length_zipIdx] + change ((φ.zipIdx).map (List.length ∘ Prod.fst)).sum = (φ.map List.length).sum + rw [← List.map_map, List.zipIdx_map_fst] + +private theorem original_route_cost (φ : CNF ℕ) (sites : List Point) (cost : Route → ℕ) + (k : ℕ) (h : ∀ o ∈ Cslib.Logic.PL.occurrences φ, + cost (lastLiteral sites (occurrencePath φ o) o.2.2.2).2 = k) : + ((originalClauses φ sites).map fun c => (c.2.2.map cost).sum).sum = k * φ.vars.length := by + have hm : (originalClauses φ sites).map (fun c => (c.2.2.map cost).sum) = + (originalClauses φ sites).map (fun c => k * c.2.2.length) := by + apply List.map_congr_left + intro c hc + have he : c.2.2.map cost = c.2.2.map (fun _ => k) := by + apply List.map_congr_left + intro r hr + obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hc + obtain ⟨lr, hlr, rfl⟩ := List.mem_map.mp hr + obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr + exact h (ci.2, lj.2, lj.1) + (List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩) + rw [he] + simp [Nat.mul_comm] + rw [hm, List.sum_map_mul_left, original_route_count] + +private theorem total_route_cost (φ : CNF ℕ) (cost : Route → ℕ) + (source ordinary crossing seam : ℕ) + (hs : ((originalClauses φ (crossingSites φ)).map fun c => (c.2.2.map cost).sum).sum = + source * φ.vars.length) + (ho : ∀ p, ((ordinaryClauses p).map fun c => (c.2.2.map cost).sum).sum = ordinary) + (hc : ∀ p, ((crossingClauses p).map fun c => (c.2.2.map cost).sum).sum = crossing) + (hl : ∀ r, ((links (crossingSites φ) r).map fun c => (c.2.2.map cost).sum).sum = + seam * (r.length - 2)) : + ((routes φ).map cost).sum = source * φ.vars.length + + ordinary * (ordinaryCells φ).length + crossing * (crossingSites φ).length + + seam * PlanarCompile.linkCount φ := by + simp only [routes, List.flatMap, List.map_flatten, List.sum_flatten, List.map_map, + Function.comp_def] + simp only [placedClauses, List.map_append, List.sum_append, List.flatMap, + List.map_flatten, List.sum_flatten, List.map_map, Function.comp_def] + simp_rw [hs, ho, hc, hl] + simp [PlanarCompile.linkCount, List.sum_map_mul_left, Nat.mul_comm, Nat.add_assoc] + +private theorem links_stat (sites : List Point) (r : Route) (cost : PlacedClause → ℕ) + (k : ℕ) (h : ∀ p q lane, cost (link sites p q lane) = k) : + ((links sites r).map cost).sum = (2 * k) * (r.length - 2) := by + have hm : (links sites r).map cost = (links sites r).map (fun _ => k) := by + apply List.map_congr_left + intro c hc + obtain ⟨e, _, hc⟩ := List.mem_flatMap.mp hc + simp only [List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl <;> exact h _ _ _ + rw [hm] + have he : ((links sites r).map fun _ => k).sum = k * (links sites r).length := by + simp [Nat.mul_comm] + rw [he, length_links, ← Nat.mul_assoc, Nat.mul_comm k 2] + +private theorem segments_translate (p : Point) (r : Route) : + (translate p r).consecutivePairs.length = r.consecutivePairs.length := by + simp [translate, List.consecutivePairs] + +private theorem ordinary_route_costs (p : Point) : + ((ordinaryClauses p).map fun c => c.2.2.length).sum = 16 ∧ + ((ordinaryClauses p).map fun c => + (c.2.2.map fun r => r.consecutivePairs.length).sum).sum = 16 ∧ + ((ordinaryClauses p).map fun c => (c.2.2.map wireLength).sum).sum = 800 := by + simp only [ordinaryClauses, List.map_map, Function.comp_def, List.length_map, + segments_translate, wireLength_translate] + decide +kernel + +private theorem crossing_route_costs (p : Point) : + ((crossingClauses p).map fun c => c.2.2.length).sum = 162 ∧ + ((crossingClauses p).map fun c => + (c.2.2.map fun r => r.consecutivePairs.length).sum).sum = 407 ∧ + ((crossingClauses p).map fun c => (c.2.2.map wireLength).sum).sum = 2192 := by + simp only [crossingClauses, List.map_map, Function.comp_def, List.length_map, + segments_translate, wireLength_translate] + decide +kernel + +private theorem access_wire_cost (sites : List Point) (p q : Point) (lane : Fin 2) : + wireLength (access sites p q lane) = 20 := by + rw [cost_access_eq_translate, wireLength_translate] + exact (PairedPorts.access_route_sizes _ _).2 + +private theorem lastLiteral_wire_cost (sites : List Point) (r : Route) (b : Bool) + (h : Orthogonal.length (r.getD (r.length - 2) (0, 0)) (r.getLastD (0, 0)) = 1) : + wireLength (lastLiteral sites r b).2 = 150 := by + dsimp only [lastLiteral] + rw [finalRoute_eq_translate sites h, wireLength_translate] + generalize side (r.getLastD (0, 0)) (r.getD (r.length - 2) (0, 0)) = s + fin_cases s <;> decide + +/-- Exact route count, one per output literal position. -/ +theorem length_routes (φ : CNF ℕ) : + (routes φ).length = φ.vars.length + 16 * (ordinaryCells φ).length + + 162 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ := by + have hs := original_route_cost φ (crossingSites φ) (fun _ => 1) 1 (fun _ _ => rfl) + have ho (p : Point) := (ordinary_route_costs p).1 + have hc (p : Point) := (crossing_route_costs p).1 + have hl (r : Route) := links_stat (crossingSites φ) r (fun c => c.2.2.length) 2 + (by intro p q lane; by_cases h : lane = 0 <;> simp [link, h]) + have h := total_route_cost φ (fun _ => 1) 1 16 162 4 (by simpa using hs) + (fun p => by simpa using ho p) (fun p => by simpa using hc p) + (fun r => by simpa using hl r) + simpa using h + +/-- 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 drawingSegmentCount_eq (φ : CNF ℕ) : + Graph.drawingSegmentCount (positions φ, routes φ) = + 3 * φ.vars.length + 16 * (ordinaryCells φ).length + + 407 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ := by + have hs := original_route_cost φ (crossingSites φ) (fun r => r.consecutivePairs.length) 3 + (fun _ _ => rfl) + have ho (p : Point) := (ordinary_route_costs p).2.1 + have hc (p : Point) := (crossing_route_costs p).2.1 + have hl (r : Route) := links_stat (crossingSites φ) r + (fun c => (c.2.2.map fun r => r.consecutivePairs.length).sum) 2 + (by intro p q lane; by_cases h : lane = 0 <;> simp [link, h, access, List.consecutivePairs]) + exact total_route_cost φ _ 3 16 407 4 hs ho hc hl + +/-- Exact Manhattan wire length of the actual drawing data. -/ +theorem drawingWireLength_eq (φ : CNF ℕ) : + Graph.drawingWireLength (positions φ, routes φ) = + 150 * φ.vars.length + 800 * (ordinaryCells φ).length + + 2192 * (crossingSites φ).length + 80 * PlanarCompile.linkCount φ := by + have hs := original_route_cost φ (crossingSites φ) wireLength 150 + (fun o ho => lastLiteral_wire_cost _ _ _ (PlanarCompile.occurrencePath_last_unit ho)) + have ho (p : Point) := (ordinary_route_costs p).2.2 + have hc (p : Point) := (crossing_route_costs p).2.2 + have hl (r : Route) := links_stat (crossingSites φ) r + (fun c => (c.2.2.map wireLength).sum) 40 + (by intro p q lane; by_cases h : lane = 0 <;> simp [link, h, access_wire_cost]) + exact total_route_cost φ _ 150 800 2192 80 hs ho hc hl + +/-- The actual route count is quadratically bounded in source incidence size. -/ +theorem routes_length_le (φ : CNF ℕ) : + (routes φ).length ≤ 10000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by + rw [length_routes, ← length_vars_formula] + exact length_vars_formula_le φ + +/-- The actual segment count is quadratically bounded in source incidence size. -/ +theorem drawingSegmentCount_le (φ : CNF ℕ) : + Graph.drawingSegmentCount (positions φ, routes φ) ≤ + 12000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by + have ho := ordinaryCells_length_le φ + have hc := crossingSites_length_le φ + have hl := PlanarCompile.linkCount_le φ + rw [drawingSegmentCount_eq] + have hb : PlanarCompile.budget φ = 80 * (φ.numVars + φ.length) + 10 * φ.vars.length := by + simp [PlanarCompile.budget, SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] + rw [hb] at ho hl + nlinarith + +/-- The actual Manhattan wire length is quadratically bounded in source incidence size. -/ +theorem drawingWireLength_le (φ : CNF ℕ) : + Graph.drawingWireLength (positions φ, routes φ) ≤ + 400000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by + have ho := ordinaryCells_length_le φ + have hc := crossingSites_length_le φ + have hl := PlanarCompile.linkCount_le φ + rw [drawingWireLength_eq] + have hb : PlanarCompile.budget φ = 80 * (φ.numVars + φ.length) + 10 * φ.vars.length := by + simp [PlanarCompile.budget, SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] + rw [hb] at ho hl + nlinarith + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedOccurrence.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedOccurrence.lean new file mode 100644 index 000000000..d29dbf33f --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedOccurrence.lean @@ -0,0 +1,331 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathGeometry +public import Complexity.Logics.Propositional.CNF.Compact.Relabel +import Mathlib.Data.List.Nodup +import Mathlib.Algebra.BigOperators.Ring.List +import Mathlib.Tactic.FinCases + +/-! +# Literal occurrences in the paired-port compiler + +Each directed path half has its own port on each lane. These keys are distinct across all +canonical source paths. The emitted external literals form a submultiset of those keys, so a +port receives at most one external occurrence. Each emitted ring contributes two internal +occurrences per port; the paired crossover contributes two at its ports and at most three at +its internal variables. + +## Main results + +* `count_vars_rawFormula_le_three`: the actual structured output respects the occurrence bound. +* `count_vars_formula_le_three`: injective compaction preserves that bound. + +## References + +This literal-position accounting for the paired compiler is original. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- The directed side used by each half of every unit step. -/ +def pathPortKeys (r : Route) : List (Point × Fin 4) := + r.consecutivePairs.flatMap fun e => [(e.1, side e.1 e.2), (e.2, side e.2 e.1)] + +/-- The signal attached to one directed half on one lane. -/ +def portKeySignal (sites : List Point) (k : (Point × Fin 4) × Fin 2) : Variable := + port sites k.1.1 k.1.2 k.2 + +/-- Both lanes of each directed path half, including the unused halves at the final clause. -/ +def pathPortSignals (sites : List Point) (r : Route) : List Variable := + ((pathPortKeys r).product [0, 1]).map (portKeySignal sites) + +private theorem portKeySignal_injective (sites : List Point) : + Function.Injective (portKeySignal sites) := by + rintro ⟨⟨p, s⟩, l⟩ ⟨⟨q, t⟩, k⟩ h + have hcell : p = q := congrArg Prod.fst h + subst q + by_cases hp : p ∈ sites + · have he : s = t ∧ l = k := by + simpa [portKeySignal, port, hp, PairedCrossover.terminal] using h + rcases he with ⟨rfl, rfl⟩ + rfl + · have he : s = t ∧ l = k := by + simpa [portKeySignal, port, hp] using h + rcases he with ⟨rfl, rfl⟩ + rfl + +private theorem pathPortSignals_cons_cons (sites : List Point) (a b : Point) (r : Route) : + pathPortSignals sites (a :: b :: r) = + [signal sites a b 0, signal sites a b 1, signal sites b a 0, signal sites b a 1] ++ + pathPortSignals sites (b :: r) := rfl + +private theorem links_cons_cons_cons (sites : List Point) (a b c : Point) (r : Route) : + links sites (a :: b :: c :: r) = + [link sites a b 0, link sites a b 1] ++ links sites (b :: c :: r) := rfl + +private theorem lastLiteral_cons_cons_cons (sites : List Point) (positive : Bool) + (a b c : Point) (r : Route) : + lastLiteral sites (a :: b :: c :: r) positive = + lastLiteral sites (b :: c :: r) positive := by + simp [lastLiteral] + +private theorem count_vars_append (φ ψ : CNF Variable) (v : Variable) : + (φ ++ ψ).vars.count v = φ.vars.count v + ψ.vars.count v := by + simp [CNF.vars] + +private theorem count_two_links (sites : List Point) (a b : Point) (v : Variable) : + (CNF.vars [(link sites a b 0).1, (link sites a b 1).1]).count v = + [signal sites a b 0, signal sites a b 1, signal sites b a 0, signal sites b a 1].count v := by + simp [link, CNF.vars, List.count_cons, Nat.add_comm, Nat.add_left_comm] + +private theorem count_last_pair_le (sites : List Point) (a b : Point) (l : Fin 2) (v : Variable) : + [signal sites a b l].count v ≤ (pathPortSignals sites [a, b]).count v := by + have hp : pathPortSignals sites [a, b] = + [signal sites a b 0, signal sites a b 1, signal sites b a 0, signal sites b a 1] := rfl + rw [hp] + have hl : l = 0 ∨ l = 1 := by fin_cases l <;> simp + rcases hl with rfl | rfl <;> simp only [List.count_cons, List.count_nil] <;> omega + +/-- External literals use only their actual path-half ports; unused clause halves overcount. -/ +theorem count_links_lastLiteral_le (sites : List Point) (positive : Bool) (r : Route) + (hlen : 2 ≤ r.length) (v : Variable) : + (CNF.vars ((links sites r).map Prod.fst)).count v + + [(lastLiteral sites r positive).1.1].count v ≤ (pathPortSignals sites r).count v := by + induction r with + | nil => simp at hlen + | cons a r ih => + cases r with + | nil => simp at hlen + | cons b r => + cases r with + | nil => + simpa [links, lastLiteral, List.consecutivePairs, CNF.vars] using + count_last_pair_le sites a b (PairedPorts.spokeLane (side b a)) v + | cons c r => + have ht := ih (by simp : 2 ≤ (b :: c :: r).length) + rw [links_cons_cons_cons, List.map_append, List.map_cons, List.map_cons, List.map_nil, + count_vars_append, lastLiteral_cons_cons_cons, + pathPortSignals_cons_cons, List.count_append, count_two_links] + omega + +/-- Both lanes of every directed port in all actual canonical paths. -/ +def allPathPortSignals (φ : CNF ℕ) : List Variable := + (paths φ).flatMap (pathPortSignals (crossingSites φ)) + +/-- Across all canonical paths each presented side/lane variable is distinct. -/ +theorem allPathPortSignals_nodup {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + (allPathPortSignals φ).Nodup := by + have hn : ((paths φ).flatMap pathPortKeys).Nodup := PlanarCompile.pathPorts_nodup hw hv + have heq : allPathPortSignals φ = + (((paths φ).flatMap pathPortKeys).product [0, 1]).map + (portKeySignal (crossingSites φ)) := by + change ((paths φ).flatMap fun r => + ((pathPortKeys r).product [0, 1]).map (portKeySignal (crossingSites φ))) = _ + simp [List.product, List.map_flatMap, List.flatMap_assoc] + rw [heq] + exact (hn.product (by decide)).map (portKeySignal_injective _) + +private theorem vars_originalClauses (φ : CNF ℕ) (sites : List Point) : + CNF.vars ((originalClauses φ sites).map Prod.fst) = + (Cslib.Logic.PL.occurrences φ).map + (fun o => (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1) := by + simp [originalClauses, Cslib.Logic.PL.occurrences, CNF.vars, List.map_flatten, + List.map_map, Function.comp_def, List.flatMap_def] + +private theorem count_external_blocks_le {φ : CNF ℕ} (sites : List Point) + (os : List (Occurrence ℕ)) + (hpaths : ∀ o ∈ os, 2 ≤ (occurrencePath φ o).length) (v : Variable) : + (CNF.vars ((os.flatMap fun o => links sites (occurrencePath φ o)).map Prod.fst)).count v + + (os.map (fun o => (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1)).count v ≤ + (os.flatMap fun o => pathPortSignals sites (occurrencePath φ o)).count v := by + induction os with + | nil => simp [CNF.vars] + | cons o os ih => + have ht := ih (fun a ha => hpaths a (List.mem_cons_of_mem _ ha)) + have ho := count_links_lastLiteral_le sites o.2.2.2 (occurrencePath φ o) + (hpaths o List.mem_cons_self) v + rw [List.flatMap_cons, List.map_append, count_vars_append, List.map_cons, + List.count_cons, List.flatMap_cons, List.count_append] + have hc : [(lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1].count v = + if (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1 == v then 1 else 0 := by + simp [List.count_cons] + rw [hc] at ho + omega + +private theorem vars_append (φ ψ : CNF Variable) : (φ ++ ψ).vars = φ.vars ++ ψ.vars := by + simp [CNF.vars] + +private theorem vars_flatMap (ps : List Point) (f : Point → List PlacedClause) : + CNF.vars ((ps.flatMap f).map Prod.fst) = + ps.flatMap fun p => CNF.vars ((f p).map Prod.fst) := by + induction ps with + | nil => rfl + | cons p ps ih => rw [List.flatMap_cons, List.map_append, vars_append, ih]; rfl + +private theorem vars_ordinaryBlock (p : Point) : + CNF.vars ((ordinaryClauses p).map Prod.fst) = + OrdinaryRing.formula.vars.map (fun v => ((p, Sum.inl v) : Variable)) := by + have h : (ordinaryClauses p).map Prod.fst = + OrdinaryRing.formula.relabel (fun v => ((p, Sum.inl v) : Variable)) := by + simpa only [ordinaryClauses, CNF.relabel, List.map_map, Function.comp_def] using + congrArg (List.map (fun c : Clause OrdinaryRing.Variable => + c.relabel (fun v => ((p, Sum.inl v) : Variable)))) + (List.zipIdx_map_fst (l := OrdinaryRing.formula) 0) + rw [h, CNF.vars_relabel] + +private theorem vars_crossingBlock (p : Point) : + CNF.vars ((crossingClauses p).map Prod.fst) = + PairedCrossover.formula.vars.map (fun v => ((p, Sum.inr v) : Variable)) := by + have h : (crossingClauses p).map Prod.fst = + PairedCrossover.formula.relabel (fun v => ((p, Sum.inr v) : Variable)) := by + simpa only [crossingClauses, CNF.relabel, List.map_map, Function.comp_def] using + congrArg (List.map (fun c : Clause PairedCrossover.Variable => + c.relabel (fun v => ((p, Sum.inr v) : Variable)))) + (List.zipIdx_map_fst (l := PairedCrossover.formula) 0) + rw [h, CNF.vars_relabel] + +/-- Literal positions supplied by all emitted ordinary rings. -/ +def ordinarySignals (φ : CNF ℕ) : List Variable := + (ordinaryCells φ).flatMap fun p => + OrdinaryRing.formula.vars.map (fun v => ((p, Sum.inl v) : Variable)) + +/-- Literal positions supplied by all emitted paired crossovers. -/ +def crossingSignals (φ : CNF ℕ) : List Variable := + (crossingSites φ).flatMap fun p => + PairedCrossover.formula.vars.map (fun v => ((p, Sum.inr v) : Variable)) + +private theorem count_tagged {W : Type*} [DecidableEq W] (ls : List W) + (tag : W → ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) + (hinj : Function.Injective tag) (ps : List Point) (p : Point) (v : W) : + (ps.flatMap fun q => ls.map (fun w => ((q, tag w) : Variable))).count (p, tag v) = + ps.count p * ls.count v := by + have hone (q : Point) : + (ls.map (fun w => ((q, tag w) : Variable))).count (p, tag v) = + if q = p then ls.count v else 0 := by + by_cases h : q = p + · subst q + rw [ite_eq_left rfl] + exact List.count_map_of_injective ls (fun w => ((p, tag w) : Variable)) + (fun _ _ he => hinj (congrArg Prod.snd he)) v + · rw [ite_eq_right h, List.count_eq_zero] + rintro hm + obtain ⟨w, _, he⟩ := List.mem_map.mp hm + exact h (congrArg Prod.fst he) + induction ps with + | nil => simp + | cons q ps ih => + rw [List.flatMap_cons, List.count_append, hone, List.count_cons, ih] + by_cases h : q = p <;> simp [h, beq_iff_eq, Nat.add_mul, Nat.add_comm] + +private theorem count_ordinary_inl (φ : CNF ℕ) (p : Point) (v : Fin 4 × Fin 2) : + (ordinarySignals φ).count (p, Sum.inl v) = (ordinaryCells φ).count p * 2 := by + rw [ordinarySignals, count_tagged _ Sum.inl Sum.inl_injective, + OrdinaryRing.internal_occurrences] + +private theorem count_crossing_inr (φ : CNF ℕ) (p : Point) (v : PairedCrossover.Variable) : + (crossingSignals φ).count (p, Sum.inr v) = + (crossingSites φ).count p * PairedCrossover.formula.vars.count v := + count_tagged _ Sum.inr Sum.inr_injective _ _ _ + +private theorem count_ordinary_inr (φ : CNF ℕ) (p : Point) (v : PairedCrossover.Variable) : + (ordinarySignals φ).count (p, Sum.inr v) = 0 := by + rw [List.count_eq_zero] + simp [ordinarySignals] + +private theorem count_crossing_inl (φ : CNF ℕ) (p : Point) (v : Fin 4 × Fin 2) : + (crossingSignals φ).count (p, Sum.inl v) = 0 := by + rw [List.count_eq_zero] + simp [crossingSignals] + +/-- Count actual emitted literals by internal template literals and actual path-half ports. -/ +theorem count_vars_rawFormula_le (φ : CNF ℕ) (v : Variable) : + (rawFormula φ).vars.count v ≤ (ordinarySignals φ).count v + + (crossingSignals φ).count v + (allPathPortSignals φ).count v := by + have he := count_external_blocks_le (φ := φ) (crossingSites φ) + (Cslib.Logic.PL.occurrences φ) (fun _ => PlanarCompile.occurrencePath_length_ge_two) v + have heq : ((Cslib.Logic.PL.occurrences φ).flatMap fun o => + pathPortSignals (crossingSites φ) (occurrencePath φ o)) = allPathPortSignals φ := by + rw [allPathPortSignals, paths, ← PlanarCompile.occurrencePaths_eq_paths, List.flatMap_map] + rw [heq] at he + have ho : CNF.vars (((ordinaryCells φ).flatMap ordinaryClauses).map Prod.fst) = + ordinarySignals φ := by + rw [vars_flatMap] + simp_rw [vars_ordinaryBlock] + rfl + have hc : CNF.vars (((crossingSites φ).flatMap crossingClauses).map Prod.fst) = + crossingSignals φ := by + rw [vars_flatMap] + simp_rw [vars_crossingBlock] + rfl + simp only [rawFormula, placedClauses, List.map_append, count_vars_append, + vars_originalClauses, ho, hc] + omega + +private theorem count_allPathPortSignals_nonterminal {φ : CNF ℕ} (p : Point) + (v : PairedCrossover.Variable) (hv : ¬ ∃ s l, PairedCrossover.terminal s l = v) : + (allPathPortSignals φ).count (p, Sum.inr v) = 0 := by + rw [List.count_eq_zero] + intro hm + obtain ⟨r, _, hm⟩ := List.mem_flatMap.mp hm + obtain ⟨k, _, hk⟩ := List.mem_map.mp hm + have hs := congrArg Prod.snd hk + by_cases hp : k.1.1 ∈ crossingSites φ + · have ht : PairedCrossover.terminal k.1.2 k.2 = v := by + simpa [portKeySignal, port, hp] using hs + exact hv ⟨_, _, ht⟩ + · simp [portKeySignal, port, hp] at hs + +private theorem count_vars_pairedFormula : ∀ v, PairedCrossover.formula.vars.count v ≤ 3 := by + decide +kernel + +private theorem count_vars_pairedTerminal : + ∀ s l, PairedCrossover.formula.vars.count (PairedCrossover.terminal s l) = 2 := by + decide +kernel + +/-- Every actual output variable has at most three literal occurrences, including repetitions +inside a clause. No occurrence certificate is assumed for the output. -/ +theorem count_vars_rawFormula_le_three {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + ∀ v, (rawFormula φ).vars.count v ≤ 3 := by + rintro ⟨p, v⟩ + have hcompare := count_vars_rawFormula_le φ (p, v) + have hext := List.nodup_iff_count_le_one.mp (allPathPortSignals_nodup hw hv) (p, v) + cases v with + | inl v => + have hn : (ordinaryCells φ).count p ≤ 1 := List.nodup_iff_count_le_one.mp + (nodup_selectDistinct _ _ : (ordinaryCells φ).Nodup) p + rw [count_ordinary_inl, count_crossing_inl] at hcompare + omega + | inr v => + have hn : (crossingSites φ).count p ≤ 1 := + List.nodup_iff_count_le_one.mp (PlanarCompile.crossingSites_nodup φ) p + rw [count_ordinary_inr, count_crossing_inr] at hcompare + by_cases ht : ∃ s l, PairedCrossover.terminal s l = v + · obtain ⟨s, l, rfl⟩ := ht + rw [count_vars_pairedTerminal] at hcompare + omega + · rw [count_allPathPortSignals_nonterminal p v ht] at hcompare + have hlocal := count_vars_pairedFormula v + have hmul := Nat.mul_le_mul hn hlocal + omega + +/-- Injective compaction preserves the actual literal-occurrence bound. -/ +theorem count_vars_formula_le_three {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + ∀ v, (formula φ).vars.count v ≤ 3 := + CNF.count_vars_compact_le (rawFormula φ) (count_vars_rawFormula_le_three hw hv) + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedPolyTime.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedPolyTime.lean new file mode 100644 index 000000000..f56c89a95 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedPolyTime.lean @@ -0,0 +1,375 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathPolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Finite +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# Native polynomial-time computation of the paired-port compiler + +Original variable names and all integer coordinates use binary encodings. List positions and +compact ranks use unary counters. The paths, crossing-site selection, and occurrence lookup reuse +the original compiler's native polynomial-time implementations. Ordinary cells are selected from +the retained path points by filtering and first-occurrence selection. + +Only the local port tag has a fixed finite encoding: an ordinary side/lane pair or a paired +crossover variable. Template tables and all finite dispatches are fixed independently of the +input formula. Neither the input formulas nor their coordinate or variable domains are finite. + +## Main definitions + +* `encVariable`: binary cell coordinates and a fixed finite local tag. +* `encPlacedClause`: the emitted clause, position, and literal incidence routes. + +## Main results + +* `computableInPolyTime_ordinaryCells`: polynomial-time selection of occupied ordinary cells. +* `computableInPolyTime_placedClauses`, `computableInPolyTime_rawFormula`: actual compiler records. +* `computableInPolyTime_formula`: the compact formula under binary CNF encodings. +* `computableInPolyTime_positions`, `computableInPolyTime_routes`: its binary geometric data. + +## References + +The compiler is the construction defined in `PairedCompile`. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal Turing.MultiTapeTM + +/-- Binary cell coordinates together with a fixed finite ordinary-port or crossover tag. -/ +noncomputable def encVariable : Variable ↪ List Bool := + encPair encPoint (encFinite ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) + +/-- A clause and its binary position and incidence-route data. -/ +noncomputable def encPlacedClause : PlacedClause ↪ List Bool := + encPair (encList (encPair encVariable encBool)) (encPair encPoint (encList encRoute)) + +private theorem computable_natCast : + ComputableInPolyTime (fun n : ℕ => (n : ℤ)) encUnary encIntBin := + .of_tidy (ComputableTidilyInPolyTime.intBin_natCast.comp + ComputableTidilyInPolyTime.unary_to_binary) + +attribute [local fun_prop] computable_natCast ComputableInPolyTime.tidy + +private theorem computable_layoutCenter : + ComputableInPolyTime Layout.center encUnary encPoint := by + refine .of_tidy ?_ + unfold Layout.center encPoint + fun_prop + +private theorem computable_side : + ComputableInPolyTime (fun p : Point × Point => side p.1 p.2) + (encPair encPoint encPoint) (encFinite (Fin 4)) := by + refine .of_tidy ?_ + unfold side PlanarCompile.side encPoint + fun_prop + +private theorem computable_cellOrigin : + ComputableInPolyTime (cellOrigin 120) encPoint encPoint := by + refine .of_tidy ?_ + unfold cellOrigin encPoint + fun_prop + +private theorem computable_center : ComputableInPolyTime center encPoint encPoint := by + refine .of_tidy ?_ + change ComputableTidilyInPolyTime (fun p : Point => + (240 * p.1 + 120, 240 * p.2 + 120)) encPoint encPoint + unfold encPoint + fun_prop + +private theorem computable_translate : + ComputableInPolyTime (fun p : Point × Route => translate p.1 p.2) + (encPair encPoint encRoute) encRoute := by + refine .of_tidy ?_ + change ComputableTidilyInPolyTime (fun p : Point × Route => + p.2.map fun q => (q.1 + p.1.1, q.2 + p.1.2)) _ _ + unfold encPoint encRoute + fun_prop + +private theorem computable_pointAdd : + ComputableInPolyTime (fun p : Point × Point => p.1 + p.2) + (encPair encPoint encPoint) encPoint := by + refine .of_tidy ?_ + change ComputableTidilyInPolyTime (fun p : Point × Point => + (p.1.1 + p.2.1, p.1.2 + p.2.2)) _ _ + unfold encPoint + fun_prop + +private theorem computable_dropLast : + ComputableInPolyTime (List.dropLast (α := Point)) encRoute encRoute := by + refine .of_tidy ?_ + change ComputableTidilyInPolyTime (fun r : Route => r.dropLast) encRoute encRoute + simp only [List.dropLast_eq_take] + unfold encRoute + fun_prop + +attribute [local fun_prop] computable_layoutCenter computable_side computable_cellOrigin + computable_center computable_translate computable_pointAdd computable_dropLast + +private theorem computable_distinctPoints : + ComputableInPolyTime (fun l : Route => selectDistinct l (List.replicate l.length true)) + encRoute encRoute := by + have hrep : ComputableTidilyInPolyTime (fun n => List.replicate n true) encUnary encBits := + ComputableTidilyInPolyTime.of_linear (.of_eq fun _ => rfl) + refine .of_tidy ?_ + unfold selectDistinct encRoute + fun_prop + +/-- Ordinary cells are selected from polynomial-size retained paths, without enumerating a +coordinate box or a domain depending on the numeric magnitude of an input label. -/ +@[fun_prop] +theorem computableInPolyTime_ordinaryCells : + ComputableInPolyTime ordinaryCells encCNF encRoute := by + have hp := PlanarCompile.computableInPolyTime_paths.tidy + have hs := PlanarCompile.computableInPolyTime_crossingSites.tidy + have hd := computable_dropLast.tidy.comp + (ComputableTidilyInPolyTime.snd encCNF encRoute) + have hl := ComputableTidilyInPolyTime.flatMapWithInput + (f := fun (_ : CNF ℕ) (r : Route) => r.dropLast) (encB := encPoint) hp hd + have ht : ComputableTidilyInPolyTime (fun p : CNF ℕ × Point => + decide (p.2 ∉ crossingSites p.1)) (encPair encCNF encPoint) encBool := + .decide_not (.decide_mem (hs.comp (.fst _ _)) (.snd _ _)) + have ho : ComputableTidilyInPolyTime (fun φ : CNF ℕ => + ((paths φ).flatMap List.dropLast).filter fun p => decide (p ∉ crossingSites φ)) + encCNF encRoute := .filterWithInput hl ht + change ComputableInPolyTime (fun φ => ordinaryCells φ) _ _ + simpa only [ordinaryCells, Function.comp_def] using + computable_distinctPoints.comp (.of_tidy ho) + +private theorem computable_port : + ComputableInPolyTime (fun p : List Point × Point × Fin 4 × Fin 2 => + port p.1 p.2.1 p.2.2.1 p.2.2.2) + (encPair encRoute (encPair encPoint + (encPair (encFinite (Fin 4)) (encFinite (Fin 2))))) encVariable := by + have hi : ComputableTidilyInPolyTime + (fun p : Fin 4 × Fin 2 => (Sum.inl p : (Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) + (encPair (encFinite (Fin 4)) (encFinite (Fin 2))) + (encFinite ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) := .of_finite _ + have ht : ComputableTidilyInPolyTime + (fun p : Fin 4 × Fin 2 => + (Sum.inr (PairedCrossover.terminal p.1 p.2) : (Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) + (encPair (encFinite (Fin 4)) (encFinite (Fin 2))) + (encFinite ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) := .of_finite _ + let input := encPair encRoute (encPair encPoint + (encPair (encFinite (Fin 4)) (encFinite (Fin 2)))) + have hs : ComputableTidilyInPolyTime + (fun p : List Point × Point × Fin 4 × Fin 2 => p.1) input encRoute := .fst _ _ + have hp : ComputableTidilyInPolyTime + (fun p : List Point × Point × Fin 4 × Fin 2 => p.2.1) input encPoint := by + unfold input + fun_prop + have ha : ComputableTidilyInPolyTime + (fun p : List Point × Point × Fin 4 × Fin 2 => (p.2.2.1, p.2.2.2)) input + (encPair (encFinite (Fin 4)) (encFinite (Fin 2))) := by + unfold input + fun_prop + have hm := ComputableTidilyInPolyTime.decide_mem hs hp + refine .of_tidy ?_ + exact hp.prod (hm.ite_decide (ht.comp ha) (hi.comp ha)) + +attribute [local fun_prop] computable_port + +private theorem computable_signal : + ComputableInPolyTime (fun p : List Point × Point × Point × Fin 2 => + signal p.1 p.2.1 p.2.2.1 p.2.2.2) + (encPair encRoute (encPair encPoint (encPair encPoint (encFinite (Fin 2))))) + encVariable := by + refine .of_tidy ?_ + unfold signal + fun_prop + +private theorem computable_variablePosition : + ComputableInPolyTime variablePosition encVariable encPoint := by + have hl : ComputableTidilyInPolyTime + (fun v : (Fin 4 × Fin 2) ⊕ PairedCrossover.Variable => + v.elim (fun p => PairedPorts.variablePosition p.1 p.2) PairedCrossover.variablePosition) + (encFinite ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) encPoint := .of_finite _ + refine .of_tidy ?_ + unfold variablePosition encVariable + fun_prop + +private theorem computable_boundary : + ComputableInPolyTime (fun p : Point × Fin 4 × Fin 2 => boundary p.1 p.2.1 p.2.2) + (encPair encPoint (encPair (encFinite (Fin 4)) (encFinite (Fin 2)))) encPoint := by + have hb : ComputableTidilyInPolyTime + (fun p : Fin 4 × Fin 2 => PairedPorts.boundaryPort p.1 p.2) + (encPair (encFinite (Fin 4)) (encFinite (Fin 2))) encPoint := .of_finite _ + refine .of_tidy ?_ + unfold boundary + fun_prop + +attribute [local fun_prop] computable_signal computable_variablePosition computable_boundary + +private theorem computable_access : + ComputableInPolyTime (fun p : List Point × Point × Point × Fin 2 => + access p.1 p.2.1 p.2.2.1 p.2.2.2) + (encPair encRoute (encPair encPoint (encPair encPoint (encFinite (Fin 2))))) encRoute := by + refine .of_tidy ?_ + unfold access encRoute + fun_prop + +attribute [local fun_prop] computable_access + +private theorem computable_link : + ComputableInPolyTime (fun p : List Point × Point × Point × Fin 2 => + link p.1 p.2.1 p.2.2.1 p.2.2.2) + (encPair encRoute (encPair encPoint (encPair encPoint (encFinite (Fin 2))))) + encPlacedClause := by + refine .of_tidy ?_ + dsimp only [link] + unfold encPlacedClause + fun_prop + +attribute [local fun_prop] computable_link + +private theorem computable_links : + ComputableInPolyTime (fun p : List Point × Route => links p.1 p.2) + (encPair encRoute encRoute) (encList encPlacedClause) := by + refine .of_tidy ?_ + unfold links List.consecutivePairs + fun_prop + +private theorem computable_lastLiteral : + ComputableInPolyTime (fun p : List Point × Route × Bool => lastLiteral p.1 p.2.1 p.2.2) + (encPair encRoute (encPair encRoute encBool)) + (encPair (encPair encVariable encBool) encRoute) := by + have hl : ComputableTidilyInPolyTime PairedPorts.spokeLane + (encFinite (Fin 4)) (encFinite (Fin 2)) := .of_finite _ + have he : ComputableTidilyInPolyTime PairedPorts.spokeElbow + (encFinite (Fin 4)) encPoint := .of_finite _ + refine .of_tidy ?_ + dsimp only [lastLiteral] + simp only [List.getLastD_eq_getLast?, List.getLast?_eq_head?_reverse] + unfold encRoute + fun_prop + +attribute [local fun_prop] computable_links computable_lastLiteral + +private theorem computable_originalClauses : + ComputableInPolyTime (fun p : CNF ℕ × List Point => originalClauses p.1 p.2) + (encPair encCNF encRoute) (encList encPlacedClause) := by + have hp := PlanarCompile.computableInPolyTime_occurrencePath.tidy + refine .of_tidy ?_ + dsimp only [originalClauses] + unfold encPlacedClause encCNF + fun_prop + +private theorem computable_templateClauses {A : Type} [Finite A] + (tag : A → (Fin 4 × Fin 2) ⊕ PairedCrossover.Variable) (ψ : CNF A) + (clausePositions : List Point) (incidenceRoutes : List (ℕ × A × Route)) : + ComputableInPolyTime (fun p : Point => ψ.zipIdx.map fun (c, i) => + (c.relabel (fun v => (p, tag v)), + cellOrigin 120 p + clausePositions.getD i (0, 0), + (incidenceRoutes.filter fun e => e.1 == i).map fun e => + translate (cellOrigin 120 p) e.2.2)) encPoint (encList encPlacedClause) := by + classical + let : Fintype A := Fintype.ofFinite A + let rowEncoding := encPair (encList (encPair (encFinite A) encBool)) encUnary + have htag : ComputableTidilyInPolyTime tag (encFinite A) + (encFinite ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)) := .of_finite _ + have hbody : ComputableInPolyTime (fun p : Point × (Clause A × ℕ) => + (p.2.1.relabel (fun v => (p.1, tag v)), + cellOrigin 120 p.1 + clausePositions.getD p.2.2 (0, 0), + (incidenceRoutes.filter fun e => e.1 == p.2.2).map fun e => + translate (cellOrigin 120 p.1) e.2.2)) + (encPair encPoint rowEncoding) encPlacedClause := by + have hpositions : ComputableTidilyInPolyTime + (fun _ : Point × (Clause A × ℕ) => clausePositions) + (encPair encPoint rowEncoding) encRoute := .const _ + have hposition : ComputableTidilyInPolyTime + (fun p : Point × (Clause A × ℕ) => clausePositions.getD p.2.2 (0, 0)) + (encPair encPoint rowEncoding) encPoint := by + unfold rowEncoding encRoute at * + fun_prop + refine .of_tidy ?_ + unfold rowEncoding encPlacedClause Clause.relabel encVariable Prod.map at * + fun_prop + have hlist : ComputableInPolyTime (fun _ : Point => ψ.zipIdx) + encPoint (encList rowEncoding) := .of_tidy (.const _) + simpa only [Function.comp_def] using ComputableInPolyTime.mapWithInput hlist hbody + +private theorem computable_ordinaryClauses : + ComputableInPolyTime ordinaryClauses encPoint (encList encPlacedClause) := by + exact computable_templateClauses Sum.inl OrdinaryRing.formula + OrdinaryRing.clausePositions OrdinaryRing.incidenceRoutes + +private theorem computable_crossingClauses : + ComputableInPolyTime crossingClauses encPoint (encList encPlacedClause) := by + exact computable_templateClauses Sum.inr PairedCrossover.formula + PairedCrossover.clausePositions PairedCrossover.incidenceRoutes + +attribute [local fun_prop] computable_originalClauses computable_ordinaryClauses + computable_crossingClauses + +/-- The complete actual list of emitted clauses and drawing records is native polynomial-time. -/ +@[fun_prop] +theorem computableInPolyTime_placedClauses : + ComputableInPolyTime placedClauses encCNF (encList encPlacedClause) := by + have hs := PlanarCompile.computableInPolyTime_crossingSites.tidy + have hp := PlanarCompile.computableInPolyTime_occurrencePath.tidy + have ho := (Cslib.Logic.PL.computableInPolyTime_occurrences encNat).tidy + refine .of_tidy ?_ + change ComputableTidilyInPolyTime (fun φ => placedClauses φ) _ _ + dsimp only [placedClauses] + unfold encCNF Cslib.Logic.PL.encOccurrence at * + fun_prop + +/-- Projecting the actual records computes the structured output formula. -/ +@[fun_prop] +theorem computableInPolyTime_rawFormula : + ComputableInPolyTime rawFormula encCNF (encList (encList (encPair encVariable encBool))) := by + have hp := computableInPolyTime_placedClauses.tidy + refine .of_tidy ?_ + unfold rawFormula encPlacedClause at * + fun_prop + +/-- The actual compact formula compiler is native polynomial-time under binary CNF encodings. +Compact ranks are computed as unary counters and then encoded in binary. -/ +@[fun_prop] +theorem computableInPolyTime_formula : ComputableInPolyTime formula encCNF encCNF := by + have hu := (CNF.isPolyTime_compact encVariable).comp computableInPolyTime_rawFormula + have hi : ComputableInPolyTime (fun n : ℕ => n) encUnary encNat := + .of_tidy ComputableTidilyInPolyTime.unary_to_binary + have hr := (CNF.computableInPolyTime_relabel hi).comp hu + have he (ψ : CNF ℕ) : ψ.relabel (fun n : ℕ => n) = ψ := CNF.relabel_id ψ + change ComputableInPolyTime (fun φ => (rawFormula φ).compact) _ _ + simpa only [Function.comp_def, he, encCNF] using hr + +/-- All actual output vertex positions are computed in polynomial time with binary coordinates. -/ +@[fun_prop] +theorem computableInPolyTime_positions : ComputableInPolyTime positions encCNF encRoute := by + have hv := (CNF.computableInPolyTime_distinctVars encVariable).comp + computableInPolyTime_rawFormula + have hp := computableInPolyTime_placedClauses.tidy + refine .of_tidy ?_ + change ComputableTidilyInPolyTime (fun φ => positions φ) _ _ + dsimp only [positions] + unfold encPlacedClause encRoute at * + fun_prop + +/-- All actual clause-to-variable incidence routes are computed in polynomial time with binary +coordinates. -/ +@[fun_prop] +theorem computableInPolyTime_routes : + ComputableInPolyTime routes encCNF (encList encRoute) := by + have hp := computableInPolyTime_placedClauses.tidy + refine .of_tidy ?_ + unfold routes encPlacedClause at * + fun_prop + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSize.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSize.lean new file mode 100644 index 000000000..3da7c4fd4 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSize.lean @@ -0,0 +1,225 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds +import Mathlib.Algebra.BigOperators.Ring.List +import Mathlib.Data.List.GetD +import Mathlib.Tactic.Linarith + +/-! +# Exact sizes of the paired-port compiler + +The actual output contains eight clauses and sixteen literal positions per ordinary ring, +78 clauses and 162 literal positions per paired crossover, and two binary clauses per retained +path gap. Source literal repetitions are counted with multiplicity. These bounds apply to all +inputs, without a geometric validity assumption. + +## Main results + +* `ordinaryCells_length_le_retained`, `ordinaryCells_length_le`: occupied ordinary-cell bounds. +* `length_formula`, `length_vars_formula`: exact clause and literal accounting. +* `width_formula`: width-three inputs produce width-three outputs. +* `length_formula_le`, `length_vars_formula_le`: explicit quadratic output bounds. + +## References + +The unchanged path estimates are reused from `Planar.Size`. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- Selected crossings reuse the canonical quadratic cover. -/ +theorem crossingSites_length_le (φ : CNF ℕ) : + (crossingSites φ).length ≤ 2 * φ.vars.length ^ 2 := + PlanarCompile.crossingSites_length_le φ + +/-- Filtering and deduplication do not increase the number of retained path points. -/ +theorem ordinaryCells_length_le_retained (φ : CNF ℕ) : + (ordinaryCells φ).length ≤ ((paths φ).map fun r => r.dropLast.length).sum := by + unfold ordinaryCells + rw [length_selectDistinct_replicate] + exact (List.toFinset_card_le _).trans ((List.length_filter_le _ _).trans_eq + List.length_flatMap) + +/-- The ordinary-cell count is bounded by the canonical total path budget. -/ +theorem ordinaryCells_length_le (φ : CNF ℕ) : + (ordinaryCells φ).length ≤ φ.vars.length * (5 * PlanarCompile.budget φ + 1) := by + calc + _ ≤ ((paths φ).map fun r => r.dropLast.length).sum := ordinaryCells_length_le_retained φ + _ ≤ ((paths φ).map fun _ => 5 * PlanarCompile.budget φ + 1).sum := + List.sum_le_sum fun r hr => (by simp only [List.length_dropLast]; omega : + r.dropLast.length ≤ r.length).trans (PlanarCompile.path_length_le hr) + _ = _ := by simp [PlanarCompile.paths_length, Nat.mul_comm] + +/-- Original clauses keep their count. -/ +theorem length_originalClauses (φ : CNF ℕ) (sites : List Point) : + (originalClauses φ sites).length = φ.length := by simp [originalClauses] + +/-- One ordinary cell contributes eight clauses. -/ +theorem length_ordinaryClauses (p : Point) : (ordinaryClauses p).length = 8 := by + simp [ordinaryClauses, OrdinaryRing.formula_sizes.1] + +/-- One crossing contributes 78 clauses. -/ +theorem length_crossingClauses (p : Point) : (crossingClauses p).length = 78 := by + simp [crossingClauses, PairedCrossover.length_formula] + +/-- Each retained path gap contributes two clauses. -/ +theorem length_links (sites : List Point) (r : Route) : + (links sites r).length = 2 * (r.length - 2) := by + have hsum : (links sites r).length = 2 * r.dropLast.consecutivePairs.length := by + simp [links, List.length_flatMap, Nat.mul_comm] + rw [hsum] + simp only [List.consecutivePairs, List.length_zip, List.length_dropLast, List.length_tail] + omega + +/-- Exact clause count of the emitted structured formula. -/ +theorem length_rawFormula (φ : CNF ℕ) : + (rawFormula φ).length = φ.length + 8 * (ordinaryCells φ).length + + 78 * (crossingSites φ).length + 2 * PlanarCompile.linkCount φ := by + simp [rawFormula, placedClauses, List.length_flatMap, length_originalClauses, + length_ordinaryClauses, length_crossingClauses, length_links, PlanarCompile.linkCount, + List.sum_map_mul_left, Nat.mul_comm, Nat.add_assoc] + +/-- Compaction preserves the exact output clause count. -/ +theorem length_formula (φ : CNF ℕ) : + (formula φ).length = φ.length + 8 * (ordinaryCells φ).length + + 78 * (crossingSites φ).length + 2 * PlanarCompile.linkCount φ := by + simpa only [formula, CNF.length_compact] using length_rawFormula φ + +/-- Original clause records preserve their widths. -/ +theorem width_originalClauses {φ : CNF ℕ} {k : ℕ} + (h : ∀ c ∈ φ, c.length ≤ k) (sites : List Point) : + ∀ c ∈ originalClauses φ sites, c.1.length ≤ k := by + intro c hc + obtain ⟨⟨d, i⟩, hd, rfl⟩ := List.mem_map.mp hc + simpa using h d (List.fst_mem_of_mem_zipIdx hd) + +/-- Every ordinary ring clause is binary. -/ +theorem width_ordinaryClauses (p : Point) : + ∀ c ∈ ordinaryClauses p, c.1.length = 2 := by + intro c hc + obtain ⟨⟨d, i⟩, hd, rfl⟩ := List.mem_map.mp hc + simpa [Clause.relabel] using OrdinaryRing.formula_sizes.2 d + (List.fst_mem_of_mem_zipIdx hd) + +/-- Every crossover clause has width at most three. -/ +theorem width_crossingClauses (p : Point) : + ∀ c ∈ crossingClauses p, c.1.length ≤ 3 := by + intro c hc + obtain ⟨⟨d, i⟩, hd, rfl⟩ := List.mem_map.mp hc + simpa [Clause.relabel] using PairedCrossover.width_formula d + (List.fst_mem_of_mem_zipIdx hd) + +/-- Every seam clause is binary. -/ +theorem width_links (sites : List Point) (r : Route) : + ∀ c ∈ links sites r, c.1.length = 2 := by + intro c hc + obtain ⟨e, _, hc⟩ := List.mem_flatMap.mp hc + simp only [List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl <;> rfl + +/-- Width-three inputs produce structured formulas of width at most three. -/ +theorem width_rawFormula {φ : CNF ℕ} (h : ∀ c ∈ φ, c.length ≤ 3) : + ∀ c ∈ rawFormula φ, c.length ≤ 3 := by + intro c hc + obtain ⟨d, hd, rfl⟩ := List.mem_map.mp hc + simp only [placedClauses, List.mem_append, List.mem_flatMap] at hd + rcases hd with ((hd | ⟨p, _, hd⟩) | ⟨p, _, hd⟩) | ⟨o, _, hd⟩ + · exact width_originalClauses h _ d hd + · exact (width_ordinaryClauses p d hd).le.trans (by decide) + · exact width_crossingClauses p d hd + · exact (width_links _ _ d hd).le.trans (by decide) + +/-- Compaction preserves the width-three guarantee. -/ +theorem width_formula {φ : CNF ℕ} (h : ∀ c ∈ φ, c.length ≤ 3) : + ∀ c ∈ formula φ, c.length ≤ 3 := by + intro c hc + have hm : c.length ∈ (formula φ).map List.length := List.mem_map_of_mem hc + rw [formula, CNF.map_length_compact] at hm + obtain ⟨d, hd, he⟩ := List.mem_map.mp hm + rw [← he] + exact width_rawFormula h d hd + +private theorem original_literal_count (φ : CNF ℕ) (sites : List Point) : + ((originalClauses φ sites).map fun c => c.1.length).sum = φ.vars.length := by + rw [CNF.length_vars] + simp only [originalClauses, List.map_map, Function.comp_def, List.length_map, + List.length_zipIdx] + change ((φ.zipIdx).map (List.length ∘ Prod.fst)).sum = (φ.map List.length).sum + rw [← List.map_map, List.zipIdx_map_fst] + +private theorem ordinary_literal_count (p : Point) : + ((ordinaryClauses p).map fun c => c.1.length).sum = 16 := by + simp only [ordinaryClauses, List.map_map, Function.comp_def, Clause.relabel, List.length_map] + decide +kernel + +private theorem crossing_literal_count (p : Point) : + ((crossingClauses p).map fun c => c.1.length).sum = 162 := by + simp only [crossingClauses, List.map_map, Function.comp_def, Clause.relabel, List.length_map] + decide +kernel + +private theorem links_literal_count (sites : List Point) (r : Route) : + ((links sites r).map fun c => c.1.length).sum = 4 * (r.length - 2) := by + have hmap : (links sites r).map (fun c => c.1.length) = (links sites r).map (fun _ => 2) := + List.map_congr_left fun c hc => width_links sites r c hc + rw [hmap] + have hsum : ((links sites r).map fun _ => 2).sum = 2 * (links sites r).length := by + simp [Nat.mul_comm] + rw [hsum, length_links] + omega + +/-- Exact literal count, including repetitions and all ordinary ring ports. -/ +theorem length_vars_rawFormula (φ : CNF ℕ) : + (rawFormula φ).vars.length = φ.vars.length + 16 * (ordinaryCells φ).length + + 162 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ := by + rw [CNF.length_vars] + simp only [rawFormula, List.map_map] + change ((placedClauses φ).map fun c => c.1.length).sum = _ + simp only [placedClauses, List.map_append, List.sum_append, List.flatMap, + List.map_flatten, List.sum_flatten, List.map_map, Function.comp_def] + simp_rw [original_literal_count, ordinary_literal_count, crossing_literal_count, + links_literal_count] + simp [PlanarCompile.linkCount, List.sum_map_mul_left, Nat.mul_comm, Nat.add_assoc] + +/-- Compaction preserves the exact number of output literal occurrences. -/ +theorem length_vars_formula (φ : CNF ℕ) : + (formula φ).vars.length = φ.vars.length + 16 * (ordinaryCells φ).length + + 162 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ := by + simpa only [formula, CNF.length_vars, CNF.map_length_compact] using length_vars_rawFormula φ + +/-- A generous explicit quadratic clause bound in the source incidence size. -/ +theorem length_formula_le (φ : CNF ℕ) : + (formula φ).length ≤ 5000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by + have ho := ordinaryCells_length_le φ + have hc := crossingSites_length_le φ + have hl := PlanarCompile.linkCount_le φ + rw [length_formula] + have hb : PlanarCompile.budget φ = 80 * (φ.numVars + φ.length) + 10 * φ.vars.length := by + simp [PlanarCompile.budget, SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] + rw [hb] at ho hl + nlinarith + +/-- A generous explicit quadratic bound on output literal occurrences. -/ +theorem length_vars_formula_le (φ : CNF ℕ) : + (formula φ).vars.length ≤ 10000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by + have ho := ordinaryCells_length_le φ + have hc := crossingSites_length_le φ + have hl := PlanarCompile.linkCount_le φ + rw [length_vars_formula] + have hb : PlanarCompile.budget φ = 80 * (φ.numVars + φ.length) + 10 * φ.vars.length := by + simp [PlanarCompile.budget, SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] + rw [hb] at ho hl + nlinarith + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/ComplexityTests/PairedOccurrence.lean b/ComplexityTests/PairedOccurrence.lean new file mode 100644 index 000000000..ad36a5008 --- /dev/null +++ b/ComplexityTests/PairedOccurrence.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedOccurrence + +/-! Repeated literals consume separate occurrence capacity in the actual paired compiler. -/ + +open Cslib.Logic.PL Cslib.Complexity.SAT.ParsimoniousPlanar + +private def repeated : CNF ℕ := [[(0, true), (0, true), (0, true)]] + +private theorem repeated_counts : ∀ v, repeated.vars.count v ≤ 3 := by + intro v + by_cases h : 0 = v + · subst v + decide + · simp [repeated, CNF.vars, h] + +example : repeated.vars.count 0 = 3 := by decide + +example (v : Variable) : (rawFormula repeated).vars.count v ≤ 3 := + count_vars_rawFormula_le_three (by decide) repeated_counts v + +example (v : ℕ) : (formula repeated).vars.count v ≤ 3 := + count_vars_formula_le_three (by decide) repeated_counts v diff --git a/ComplexityTests/PlanarBounds.lean b/ComplexityTests/PlanarBounds.lean index d16694e29..42c3e1302 100644 --- a/ComplexityTests/PlanarBounds.lean +++ b/ComplexityTests/PlanarBounds.lean @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Erik Demaine -/ -import Complexity.Computability.Complexity.Problems.SAT.Planar.Bounds +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedBounds namespace ComplexityTests.PlanarBounds -open Cslib.Complexity Cslib.Complexity.SAT.PlanarCompile +open Cslib.Complexity Cslib.Complexity.SAT.ParsimoniousPlanar -- The same linear grid bounds apply to an ordinary name and a succinct large binary name. example : gridWidth [[(7, true)]] = 4080 := by decide +kernel @@ -24,13 +24,13 @@ example : Graph.drawingFits (positions [[(7, true)]], routes [[(7, true)]]) 4080 example : positions [[]] = [(1080, 1080)] := by decide +kernel example : Graph.drawingFits (positions [[]], routes [[]]) 2160 2160 := drawing_fits [[]] --- Exact costs for the actual nonempty unit-clause output, including its final two-segment route. -example : (routes [[(7, true)]]).length = 63 := by decide +kernel -example : Graph.drawingSegmentCount (positions [[(7, true)]], routes [[(7, true)]]) = 64 := +-- Exact costs for the actual nonempty unit-clause output, including its final three-segment route. +example : (routes [[(7, true)]]).length = 637 := by decide +kernel +example : Graph.drawingSegmentCount (positions [[(7, true)]], routes [[(7, true)]]) = 639 := by decide +kernel -example : Graph.drawingWireLength (positions [[(7, true)]], routes [[(7, true)]]) = 7680 := +example : Graph.drawingWireLength (positions [[(7, true)]], routes [[(7, true)]]) = 28230 := by decide +kernel -example : Graph.drawingWireLength (positions [[(7, false)]], routes [[(7, false)]]) = 7680 := +example : Graph.drawingWireLength (positions [[(7, false)]], routes [[(7, false)]]) = 28230 := by decide +kernel end ComplexityTests.PlanarBounds diff --git a/ComplexityTests/PlanarOccurrence.lean b/ComplexityTests/PlanarOccurrence.lean index 2fb70bdbf..448691f92 100644 --- a/ComplexityTests/PlanarOccurrence.lean +++ b/ComplexityTests/PlanarOccurrence.lean @@ -4,43 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Erik Demaine -/ -import Complexity.Computability.Complexity.Problems.SAT.Planar.Occurrence +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedOccurrence -/-! Literal-position counting regressions for actual planarization paths. -/ +/-! Literal-position regressions for the paired compiler and its shared canonical paths. -/ -open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Complexity.SAT.PlanarCompile Cslib.Orthogonal +open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Complexity.SAT.ParsimoniousPlanar +open Cslib.Complexity.SAT.PlanarCompile (occurrencePaths_eq_paths) private def repeated : CNF ℕ := [[(0, true), (0, false), (0, true)]] -example : (Cslib.Logic.PL.occurrences repeated).Nodup := Cslib.Logic.PL.occurrences_nodup _ - example : (Cslib.Logic.PL.occurrences repeated).map (occurrencePath repeated) = paths repeated := occurrencePaths_eq_paths _ -example : (pathSignals [] [(0, 0), (1, 0), (2, 0)]).count ((1, 0), none) = 2 := by decide - -example : (pathSignals [] [(0, 0), (1, 0), (2, 0)]).count ((0, 0), none) = 1 := by decide - -example : (pathSignals [(1, 0)] [(0, 0), (1, 0), (2, 0)]).count - ((1, 0), some (Crossover.splitTerminal 0)) = 1 := by decide - -example : (pathSignals [(1, 0)] [(0, 0), (1, 0), (2, 0)]).count - ((1, 0), some (Crossover.splitTerminal 1)) = 1 := by decide - -example : (pathSignals [(1, 0)] [(0, 0), (1, 0), (2, 0)]).count ((1, 0), none) = 0 := by decide - -example (positive : Bool) : - (CNF.vars ((links [] positive [(0, 0), (1, 0), (2, 0)]).map Prod.fst)).count ((1, 0), none) + - [(lastLiteral [] [(0, 0), (1, 0), (2, 0)] positive).1.1].count ((1, 0), none) ≤ 2 := by - simpa only [show (pathSignals [] [(0, 0), (1, 0), (2, 0)]).count ((1, 0), none) = 2 by decide] - using count_links_lastLiteral_le [] positive [(0, 0), (1, 0), (2, 0)] (by decide) ((1, 0), none) - -example (i : Fin 4) : Crossover.splitFormula.vars.count (Crossover.splitTerminal i) = 2 := - count_vars_splitTerminal i - -example (v : Crossover.SplitVariable) : Crossover.splitFormula.vars.count v ≤ 3 := - count_vars_splitFormula v - private theorem repeated_width : ∀ c ∈ repeated, c.length ≤ 3 := by intro c hc simp only [repeated, List.mem_singleton] at hc @@ -77,20 +52,6 @@ private theorem crossed_count : ∀ v, crossed.vars.count v ≤ 3 := by · rw [List.count_eq_zero.mpr hv] decide --- This actual compiler input selects a strict bridge/stem crossing at (10,42). -private theorem crossing_selected : (10, 42) ∈ crossingSites crossed := by decide +kernel - -example (i : Fin 4) : (allPathSignals crossed).count - ((10, 42), some (Crossover.splitTerminal i)) ≤ 1 := - count_allPathSignals_terminal_le_one crossed_width crossed_count _ i crossing_selected - -example (i : Fin 4) : (crossingSignals crossed).count - ((10, 42), some (Crossover.splitTerminal i)) = 2 := by - rw [count_crossingSignals_some, count_vars_splitTerminal] - have hpos := List.count_pos_iff.mpr crossing_selected - have hle := List.nodup_iff_count_le_one.mp (crossingSites_nodup crossed) (10, 42) - omega - example : ∀ v, (rawFormula crossed).vars.count v ≤ 3 := count_vars_rawFormula_le_three crossed_width crossed_count