diff --git a/Complexity.lean b/Complexity.lean index 538c50259..67d75ddc7 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -815,6 +815,11 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRi 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.PathAssignments +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathGeometry +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathPolyTime public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy public import Complexity.Computability.Complexity.Problems.SAT.Planar.PolyTime diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean index 2aa32de78..53f6ab0f9 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry @@ -50,12 +51,6 @@ These bounds concern the original finite compiler in `Compile` and its 240-squar namespace Cslib.Complexity.SAT.PlanarCompile open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal -/-- Horizontal side of the actual tiled drawing, including its last square. -/ -def gridWidth (φ : CNF ℕ) : ℕ := 240 * (8 * (SAT.incidenceGraph φ).1.length + 1) -/-- Vertical side of the actual tiled drawing, including its last square. -/ -def gridHeight (φ : CNF ℕ) : ℕ := - 240 * (8 * (SAT.incidenceGraph φ).1.length + 2 * (SAT.incidenceGraph φ).2.length + 1) - 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 : ℤ) + @@ -279,20 +274,6 @@ theorem drawing_fits (φ : CNF ℕ) : 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 at most 1920 times the source incidence size plus one. -/ -theorem gridWidth_le (φ : CNF ℕ) : - gridWidth φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := by - unfold gridWidth - rw [SAT.length_vertices_incidenceGraph] - nlinarith - -/-- The vertical grid side is at most 1920 times the source incidence size plus one. -/ -theorem gridHeight_le (φ : CNF ℕ) : - gridHeight φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := by - unfold gridHeight - rw [SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] - nlinarith - private theorem access_cost (sites : List Point) (p q : Point) : wireLength (access sites p q) ≤ 240 ∧ (access sites p q).consecutivePairs.length ≤ 19 := by diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean index a14da4cc3..5b4c8d96e 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean @@ -7,6 +7,8 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments public import Complexity.Computability.Complexity.Problems.SAT.Incidence public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalLayout public import Complexity.Foundations.Geometry.Orthogonal.Subdivision @@ -44,57 +46,9 @@ namespace Cslib.Complexity.SAT.PlanarCompile open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal -/-- A cell's ordinary signal, or a local variable of its crossover. -/ -abbrev Variable := Point × Option Crossover.SplitVariable - /-- A clause, its position, and one route per literal in literal order. -/ abbrev PlacedClause := Clause Variable × Point × List Route -/-- The explicit linear per-route expansion budget. -/ -def budget (φ : CNF ℕ) : ℕ := - 80 * (SAT.incidenceGraph φ).1.length + 10 * (SAT.incidenceGraph φ).2.length - -/-- Unit paths in the order of the original literal occurrences. -/ -def paths (φ : CNF ℕ) : List Route := - let G := SAT.incidenceGraph φ - (G.orthogonalRoutes G.canonicalPorts).map (subdivideWithin (budget φ)) - -/-- The path of a particular original literal occurrence. -/ -def occurrencePath (φ : CNF ℕ) (o : Occurrence ℕ) : Route := - (paths φ).getD ((Cslib.Logic.PL.occurrences φ).idxOf o) [] - -/-- Actual occupied crossing candidates, excluding every declared graph vertex center. -First-occurrence selection ensures exactly one local gadget per selected square. -/ -def crossingSites (φ : CNF ℕ) : List Point := - let G := SAT.incidenceGraph φ - let occupied := (G.crossingCandidates G.canonicalPorts).filter fun p => - !(G.orthogonalPositions.contains p) && - decide (2 ≤ ((paths φ).filter fun r => r.contains p).length) - Cslib.Complexity.selectDistinct occupied (List.replicate occupied.length true) - -/-- The selected cells are exactly occupied nonvertex candidates. -/ -theorem mem_crossingSites (φ : CNF ℕ) (p : Point) : - p ∈ crossingSites φ ↔ - p ∈ (SAT.incidenceGraph φ).crossingCandidates (SAT.incidenceGraph φ).canonicalPorts ∧ - p ∉ (SAT.incidenceGraph φ).orthogonalPositions ∧ - 2 ≤ ((paths φ).filter fun r => r.contains p).length := by - simp [crossingSites, mem_selectDistinct_replicate, Bool.and_eq_true] - -/-- Every selected square receives exactly one template. -/ -theorem crossingSites_nodup (φ : CNF ℕ) : (crossingSites φ).Nodup := nodup_selectDistinct _ _ - -/-- Side facing a neighboring square, in left/right/bottom/top order. -Only unit neighbors are used by the correctness theorem. -/ -def side (p q : Point) : Fin 4 := - if q.1 < p.1 then 0 else if p.1 < q.1 then 1 else if q.2 < p.2 then 2 else 3 - -/-- The center of a square of side 240 indexed by an integer grid point. -/ -def center (p : Point) : Point := cellOrigin 120 p + (120, 120) - -/-- The signal presented by a cell toward a neighboring cell. -/ -def signal (sites : List Point) (p q : Point) : Variable := - (p, if p ∈ sites then some (Crossover.splitTerminal (side p q)) else none) - /-- Geometric position of a structured output variable. -/ def variablePosition (v : Variable) : Point := cellOrigin 120 v.1 + v.2.elim (120, 120) Crossover.variablePosition @@ -104,12 +58,6 @@ def access (sites : List Point) (p q : Point) : Route := if p ∈ sites then translate (cellOrigin 120 p) (Crossover.accessRoute (side p q)) else [cellPort 120 p (side p q), center p] -/-- Every cell before the original clause vertex contributes an entry/exit signal pair. -At the source endpoint the unused entry defaults to the source's own ordinary signal. -/ -def wire (sites : List Point) (r : Route) : List (Variable × Variable) := - r.dropLast.zipIdx.map fun (p, i) => - (signal sites p (r.getD (i - 1) p), signal sites p (r.getD (i + 1) p)) - /-- One implication at the common side midpoint of adjacent occupied cells. Positive literals propagate toward the source, negative literals toward the clause. -/ def link (sites : List Point) (positive : Bool) (p q : Point) : PlacedClause := diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean index c61a182cb..3056a8b93 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments public import Complexity.Computability.Complexity.Problems.SAT.Planar.Correctness import Mathlib.Data.List.GetD import Mathlib.Tactic.SplitIfs @@ -39,283 +40,6 @@ namespace Cslib.Complexity.SAT.PlanarCompile open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal -private theorem two_paths_filter_length (rs : List Route) (p : Point) {i j : ℕ} - (hi : i < rs.length) (hj : j < rs.length) (hij : i ≠ j) - (hpi : p ∈ rs[i]) (hpj : p ∈ rs[j]) : - 2 ≤ (rs.filter fun r => r.contains p).length := by - induction rs generalizing i j with - | nil => simp at hi - | cons r rs ih => - cases i with - | zero => - cases j with - | zero => exact False.elim (hij rfl) - | succ j => - have hj' : j < rs.length := by simpa using hj - have hm : rs[j] ∈ rs.filter (fun r => r.contains p) := - List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hj), - List.contains_iff_mem.mpr hpj⟩ - obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm - have hphead : p ∈ r := hpi - simp only [List.filter_cons, List.contains_iff_mem.mpr hphead, - ite_true, List.length_cons] - omega - | succ i => - cases j with - | zero => - have hi' : i < rs.length := by simpa using hi - have hm : rs[i] ∈ rs.filter (fun r => r.contains p) := - List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hi), - List.contains_iff_mem.mpr hpi⟩ - obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm - have hphead : p ∈ r := hpj - simp only [List.filter_cons, List.contains_iff_mem.mpr hphead, - ite_true, List.length_cons] - omega - | succ j => - have ht := ih (by simpa using hi) (by simpa using hj) (by omega) hpi hpj - rw [List.filter_cons] - split_ifs - · simp only [List.length_cons] - omega - · exact ht - -private theorem path_mem_paths_get {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∈ occurrencePath φ o) : - p ∈ (paths φ)[(Cslib.Logic.PL.occurrences φ).idxOf o]'(by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho) := by - unfold occurrencePath at hp - rwa [List.getD_eq_getElem _ _ (by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho)] at hp - -/-- Two different occurrence paths sharing an ordinary cell meet at a declared vertex center. -/ -theorem shared_ordinary_cell_center {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) - (ht : t ∈ Cslib.Logic.PL.occurrences φ) (hot : o ≠ t) {p : Point} - (hp : p ∉ crossingSites φ) (hpo : p ∈ occurrencePath φ o) - (hpt : p ∈ occurrencePath φ t) : p ∈ (SAT.incidenceGraph φ).orthogonalPositions := by - by_contra hc - have hij : (Cslib.Logic.PL.occurrences φ).idxOf o ≠ - (Cslib.Logic.PL.occurrences φ).idxOf t := fun he => hot ((List.idxOf_inj ho).1 he) - have hcandidate := Graph.unitPath_shared_mem_crossingCandidates (SAT.incidenceGraph φ) - (fun _ he => SAT.incidenceGraph_endpoints he) - (fun _ he => SAT.incidenceGraph_loopless he) (SAT.incidenceGraph_degree_le hw hv) - (occurrence_index_lt ho) (occurrence_index_lt ht) hij hc - (by simpa only [occurrencePath_eq_unitPath] using hpo) - (by simpa only [occurrencePath_eq_unitPath] using hpt) - apply hp - apply (mem_crossingSites φ p).2 - refine ⟨hcandidate, hc, ?_⟩ - exact two_paths_filter_length (paths φ) p - (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho) - (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ht) - hij (path_mem_paths_get ho hpo) (path_mem_paths_get ht hpt) - -/-- No retained wire cell is the clause-center endpoint removed by `dropLast`. -/ -theorem clause_center_not_mem_dropLast {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - Layout.center (φ.distinctVars.length + o.1) ∉ (occurrencePath φ o).dropLast := by - intro hp - obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hp - have hlen := occurrencePath_length_ge_two ho - have hk' : k < (occurrencePath φ o).length := by - simp only [List.length_dropLast] at hk - omega - have hlast := (occurrencePath_endpoints ho).2 - rw [List.getLast?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hlast - have heq' : (occurrencePath φ o)[k] = - (occurrencePath φ o)[(occurrencePath φ o).length - 1] := by - rw [← List.getElem_dropLast hk, heq, Option.some.inj hlast] - have hidx := (occurrencePath_nodup ho).getElem_inj_iff.1 heq' - simp only [List.length_dropLast] at hk - omega - -/-- A retained cell at a declared center is the source-variable center of its occurrence. -/ -theorem dropLast_center_eq_source {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} - (hp : p ∈ (occurrencePath φ o).dropLast) - (hc : p ∈ (SAT.incidenceGraph φ).orthogonalPositions) : - p = Layout.center (φ.distinctVars.idxOf o.2.2.1) := by - obtain ⟨w, hw, rfl⟩ := List.mem_map.mp hc - have hw' := List.mem_range.mp hw - have hwmem : w ∈ (SAT.incidenceGraph φ).1 := by - apply List.mem_range.mpr - simpa only [SAT.incidenceGraph, List.length_range] using hw' - have hi := List.idxOf_lt_length_of_mem hwmem - have hidx : (SAT.incidenceGraph φ).1.idxOf w = w := by - simpa only [SAT.incidenceGraph, List.getElem_range] using List.getElem_idxOf hi - have h := (Graph.unitPath_declared_center_iff (SAT.incidenceGraph φ) - (fun _ he => SAT.incidenceGraph_endpoints he) - (fun _ he => SAT.incidenceGraph_loopless he) (occurrence_index_lt ho) hwmem).1 - (by rw [hidx]; simpa only [occurrencePath_eq_unitPath] using List.dropLast_subset _ hp) - simp only [SAT.incidenceGraph, List.getElem_map, - List.getElem_idxOf (List.idxOf_lt_length_of_mem ho)] at h - rcases h with h | h - · rw [h] - · exact False.elim (clause_center_not_mem_dropLast ho (h ▸ hp)) - -/-- All occurrences using an ordinary retained cell have the same original variable. -/ -theorem ordinary_cell_source_eq {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) - (ht : t ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∉ crossingSites φ) - (hpo : p ∈ (occurrencePath φ o).dropLast) - (hpt : p ∈ (occurrencePath φ t).dropLast) : o.2.2.1 = t.2.2.1 := by - by_cases hot : o = t - · rw [hot] - have hc := shared_ordinary_cell_center hw hv ho ht hot hp - (List.dropLast_subset _ hpo) (List.dropLast_subset _ hpt) - have he := (dropLast_center_eq_source ho hpo hc).symm.trans - (dropLast_center_eq_source ht hpt hc) - have hx := congrArg Prod.fst he - simp only [Layout.center] at hx - have hi : φ.distinctVars.idxOf o.2.2.1 = φ.distinctVars.idxOf t.2.2.1 := by omega - apply (List.idxOf_inj ?_).1 hi - apply CNF.mem_distinctVars.mpr - rw [← Cslib.Logic.PL.map_occurrences] - exact List.mem_map_of_mem ho - -private theorem not_both_straight {r : Route} (hn : r.Nodup) {p : Point} (hp : p ∈ r) - (hh : StraightThrough r p (1, 0)) (hv : StraightThrough r p (0, 1)) : False := by - obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hp - obtain ⟨_, _, hhn⟩ := hh.getD_neighbors hn hk heq - obtain ⟨_, _, hvn⟩ := hv.getD_neighbors hn hk heq - rcases hhn with ⟨hh, _⟩ | ⟨hh, _⟩ <;> rcases hvn with ⟨hv, _⟩ | ⟨hv, _⟩ - all_goals - have hx := congrArg Prod.fst (hh.symm.trans hv) - simp only [Prod.fst_sub, Prod.fst_add] at hx - omega - -/-- The occurrence carrying either coordinate-axis signal at a crossing is unique. -/ -theorem crossing_axis_occurrence_eq {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) - (ht : t ∈ Cslib.Logic.PL.occurrences φ) {p d : Point} - (hp : p ∈ crossingSites φ) (hpo : p ∈ occurrencePath φ o) - (hpt : p ∈ occurrencePath φ t) (hd : d = (1, 0) ∨ d = (0, 1)) - (hs : StraightThrough (occurrencePath φ o) p d) - (hts : StraightThrough (occurrencePath φ t) p d) : o = t := by - by_contra hot - have hij : (Cslib.Logic.PL.occurrences φ).idxOf o ≠ - (Cslib.Logic.PL.occurrences φ).idxOf t := fun he => hot ((List.idxOf_inj ho).1 he) - have hn := Graph.unitPath_crossing_neighbors (SAT.incidenceGraph φ) - (fun _ he => SAT.incidenceGraph_endpoints he) - (fun _ he => SAT.incidenceGraph_loopless he) (SAT.incidenceGraph_degree_le hw hv) - (occurrence_index_lt ho) (occurrence_index_lt ht) hij - ((mem_crossingSites φ p).1 hp).2.1 - (by simpa only [occurrencePath_eq_unitPath] using hpo) - (by simpa only [occurrencePath_eq_unitPath] using hpt) - rw [← occurrencePath_eq_unitPath, ← occurrencePath_eq_unitPath] at hn - rcases hd with rfl | rfl - · rcases hn with ⟨_, htvert⟩ | ⟨hovert, _⟩ - · exact not_both_straight (occurrencePath_nodup ht) hpt hts htvert - · exact not_both_straight (occurrencePath_nodup ho) hpo hs hovert - · rcases hn with ⟨hohor, _⟩ | ⟨_, hthor⟩ - · exact not_both_straight (occurrencePath_nodup ho) hpo hohor hs - · exact not_both_straight (occurrencePath_nodup ht) hpt hthor hts - -open Classical in -private noncomputable def chosenValue (τ : ℕ → Bool) (P : Occurrence ℕ → Prop) : Bool := - if h : ∃ o, P o then τ (Classical.choose h).2.2.1 else false - -private theorem chosenValue_eq (τ : ℕ → Bool) (P : Occurrence ℕ → Prop) - {o : Occurrence ℕ} (ho : P o) (heq : ∀ t, P t → t.2.2.1 = o.2.2.1) : - chosenValue τ P = τ o.2.2.1 := by - classical - have h : ∃ t, P t := ⟨o, ho⟩ - simp only [chosenValue, dite_eq_left h] - rw [heq _ (Classical.choose_spec h)] - -/-- Every source assignment extends compatibly to all actual wire cells and crossover blocks. -The choice of auxiliary values is logical; this theorem makes no computational claim. -/ -theorem exists_compatible_assignment {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) (τ : ℕ → Bool) : - ∃ σ : Variable → Bool, - (∀ o ∈ Cslib.Logic.PL.occurrences φ, - ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), - σ c.1 = τ o.2.2.1 ∧ σ c.2 = τ o.2.2.1) ∧ - (∀ p ∈ crossingSites φ, Crossover.splitFormula.eval (fun v => σ (p, some v)) = true) := by - classical - let ordinary (p : Point) := chosenValue τ (fun o => - o ∈ Cslib.Logic.PL.occurrences φ ∧ p ∈ (occurrencePath φ o).dropLast) - let axis (p d : Point) := chosenValue τ (fun o => - o ∈ Cslib.Logic.PL.occurrences φ ∧ p ∈ occurrencePath φ o ∧ - StraightThrough (occurrencePath φ o) p d) - have hord {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} - (hp : p ∉ crossingSites φ) (hpo : p ∈ (occurrencePath φ o).dropLast) : - ordinary p = τ o.2.2.1 := by - apply chosenValue_eq τ _ ⟨ho, hpo⟩ - intro t ht - exact ordinary_cell_source_eq hw hv ht.1 ho hp ht.2 hpo - have haxis {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p d : Point} - (hp : p ∈ crossingSites φ) (hpo : p ∈ occurrencePath φ o) - (hd : d = (1, 0) ∨ d = (0, 1)) (hs : StraightThrough (occurrencePath φ o) p d) : - axis p d = τ o.2.2.1 := by - apply chosenValue_eq τ _ ⟨ho, hpo, hs⟩ - intro t ht - rw [crossing_axis_occurrence_eq hw hv ht.1 ho hp ht.2.1 hpo hd ht.2.2 hs] - let cross (p : Point) : Crossover.SplitVariable → Bool := - Classical.choose (Crossover.exists_split_holds (axis p (1, 0)) (axis p (0, 1))) - have hcross (p : Point) := - Classical.choose_spec (Crossover.exists_split_holds (axis p (1, 0)) (axis p (0, 1))) - let σ : Variable → Bool := fun v => match v.2 with - | none => ordinary v.1 - | some a => cross v.1 a - refine ⟨σ, ?_, fun p _ => (hcross p).1⟩ - intro o ho c hc - unfold wire at hc - obtain ⟨⟨p, k⟩, hpk, rfl⟩ := List.mem_map.mp hc - have hget := List.mem_zipIdx_iff_getElem?.mp hpk - obtain ⟨hk, heq⟩ := List.getElem?_eq_some_iff.mp hget - have hk' : k < (occurrencePath φ o).length := by - simp only [List.length_dropLast] at hk - omega - have heq' : (occurrencePath φ o)[k] = p := by - rw [← List.getElem_dropLast hk] - exact heq - have hpo : p ∈ occurrencePath φ o := heq' ▸ List.getElem_mem hk' - change (List.dropLast (occurrencePath φ o))[k] = p at heq - have hpod : p ∈ (occurrencePath φ o).dropLast := by - rw [← heq] - exact List.getElem_mem hk - by_cases hp : p ∈ crossingSites φ - · have hl : side p (p - (1, 0)) = 0 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_sub, Prod.snd_sub] - split_ifs <;> first | rfl | omega - have hr : side p (p + (1, 0)) = 1 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_add, Prod.snd_add] - split_ifs <;> first | rfl | omega - have ht : side p (p - (0, 1)) = 2 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_sub, Prod.snd_sub] - split_ifs <;> first | rfl | omega - have hb : side p (p + (0, 1)) = 3 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_add, Prod.snd_add] - split_ifs <;> first | rfl | omega - rcases occurrencePath_crossing_straight hw hv ho hp hpo with hs | hs - · have hav := haxis ho hp hpo (Or.inl rfl) hs - have hports := (hcross p).2 - obtain ⟨_, _, hnb⟩ := hs.getD_neighbors (occurrencePath_nodup ho) hk' heq' - rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ - all_goals - simp only [hprev, hnext, signal, hp, ite_true, hl, hr, Crossover.splitTerminal] - exact ⟨by simpa only [σ, cross, hports.1, hports.2.1] using hav, - by simpa only [σ, cross, hports.1, hports.2.1] using hav⟩ - · have hav := haxis ho hp hpo (Or.inr rfl) hs - have hports := (hcross p).2.2.2 - obtain ⟨_, _, hnb⟩ := hs.getD_neighbors (occurrencePath_nodup ho) hk' heq' - rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ - all_goals - simp only [hprev, hnext, signal, hp, ite_true, ht, hb, Crossover.splitTerminal] - exact ⟨by simpa only [σ, cross, hports.1, hports.2] using hav, - by simpa only [σ, cross, hports.1, hports.2] using hav⟩ - · simpa only [signal, hp, ite_false, σ] using - And.intro (hord ho hp hpod) (hord ho hp hpod) - /-- An actual raw compiler output has a satisfying extension of every source model. -/ theorem satisfiable_rawFormula_of_source {φ : CNF ℕ} (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean index df779538b..dc8fde83a 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments public import Complexity.Computability.Complexity.Problems.SAT.Planar.Semantics public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths @@ -39,51 +40,6 @@ namespace Cslib.Complexity.SAT.PlanarCompile open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal -private theorem occurrence_var_mem {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) : o.2.2.1 ∈ φ.vars := by - rw [← Cslib.Logic.PL.map_occurrences] - exact List.mem_map_of_mem ho - -/-- The actual graph edge has the occurrence's original variable and clause labels. -/ -theorem occurrence_edgeEndpoint {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) (side : Bool) : - (SAT.incidenceGraph φ).edgeEndpoint ((Cslib.Logic.PL.occurrences φ).idxOf o) side = - if side then φ.distinctVars.length + o.1 else φ.distinctVars.idxOf o.2.2.1 := by - unfold Graph.edgeEndpoint - rw [List.getD_eq_getElem _ _ (occurrence_index_lt ho)] - simp only [SAT.incidenceGraph, List.getElem_map, - List.getElem_idxOf (List.idxOf_lt_length_of_mem ho)] - -private theorem other_path_index (rs : List Route) (p : Point) (i : ℕ) (hi : i < rs.length) - (hcount : 2 ≤ (rs.filter fun r => r.contains p).length) : - ∃ j, ∃ hj : j < rs.length, j ≠ i ∧ p ∈ rs[j] := by - induction rs generalizing i with - | nil => simp at hi - | cons r rs ih => - cases i with - | zero => - have hpos : 0 < (rs.filter fun r => r.contains p).length := by - rw [List.filter_cons] at hcount - split_ifs at hcount - · simp only [List.length_cons] at hcount - omega - · omega - obtain ⟨s, hs⟩ := List.exists_mem_of_length_pos hpos - have hm := List.mem_filter.mp hs - obtain ⟨j, hj, hsj⟩ := List.mem_iff_getElem.mp hm.1 - refine ⟨j + 1, by simp only [List.length_cons]; omega, by omega, ?_⟩ - simp only [List.getElem_cons_succ] - rw [hsj] - exact List.contains_iff_mem.mp hm.2 - | succ i => - by_cases hmem : r.contains p = true - · exact ⟨0, by simp, by omega, by simpa using List.contains_iff_mem.mp hmem⟩ - · have ht : 2 ≤ (rs.filter fun r => r.contains p).length := by - have hp : p ∉ r := fun hp => hmem (List.contains_iff_mem.mpr hp) - simpa [List.filter_cons, hp] using hcount - obtain ⟨j, hj, hji, hp⟩ := ih i (by simp only [List.length_cons] at hi; omega) ht - exact ⟨j + 1, by simp only [List.length_cons]; omega, by omega, by simpa using hp⟩ - /-- An actual crossover whose path goes straight through a cell equates the two signals read by the executable neighbor lookups, in either traversal direction. -/ theorem signals_eq_of_straight {φ : CNF ℕ} {σ : Variable → Bool} @@ -106,38 +62,6 @@ theorem signals_eq_of_straight {φ : CNF ℕ} {σ : Variable → Bool} · rw [hprev, hnext] exact (vertical_signal_eq hraw hp).symm -/-- A selected crossing is traversed straight along one coordinate axis by each occupying path. -/ -theorem occurrencePath_crossing_straight {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) - {p : Point} (hp : p ∈ crossingSites φ) (hpi : p ∈ occurrencePath φ o) : - StraightThrough (occurrencePath φ o) p (1, 0) ∨ - StraightThrough (occurrencePath φ o) p (0, 1) := by - have hsite := (mem_crossingSites φ p).1 hp - let G := SAT.incidenceGraph φ - have hG : ∀ e ∈ G.2, e.1 ∈ G.1 ∧ e.2 ∈ G.1 := - fun _ he => SAT.incidenceGraph_endpoints he - have hloop : ∀ e ∈ G.2, e.1 ≠ e.2 := fun _ he => SAT.incidenceGraph_loopless he - have hdeg : ∀ v, G.incidenceVertices.count v ≤ 3 := SAT.incidenceGraph_degree_le hw hv - have hi := occurrence_index_lt ho - obtain ⟨j, hj, hji, hpj⟩ := other_path_index (paths φ) p - ((Cslib.Logic.PL.occurrences φ).idxOf o) - (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi) hsite.2.2 - have hj' : j < G.2.length := by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hj - have hpi' : p ∈ G.unitPath ((Cslib.Logic.PL.occurrences φ).idxOf o) := by - simpa only [occurrencePath_eq_unitPath] using hpi - have hpj' : p ∈ G.unitPath j := by - unfold Graph.unitPath - change p ∈ (SAT.incidenceGraph φ).unitPaths.getD j [] - rw [← paths_eq_unitPaths, List.getD_eq_getElem _ _ hj] - exact hpj - have hnb := Graph.unitPath_crossing_neighbors G hG hloop hdeg hi hj' (Ne.symm hji) - hsite.2.1 hpi' hpj' - rcases hnb with ⟨h, _⟩ | ⟨h, _⟩ - · exact Or.inl (by simpa only [occurrencePath_eq_unitPath] using h) - · exact Or.inr (by simpa only [occurrencePath_eq_unitPath] using h) - /-- Actual cell entry/exit values agree: ordinary cells share one variable, while selected crossings use the certified opposite ports of the fixed crossover. -/ theorem wire_cells_agree {φ : CNF ℕ} @@ -164,42 +88,6 @@ theorem wire_cells_agree {φ : CNF ℕ} (occurrencePath_crossing_straight hw hv ho hp hpi) · simp only [signal, hp, ite_false] -/-- The initial source center is excluded from the actual selected crossing list. -/ -theorem source_center_not_crossing {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - Layout.center (φ.distinctVars.idxOf o.2.2.1) ∉ crossingSites φ := by - intro hp - have hvar := List.idxOf_lt_length_of_mem (CNF.mem_distinctVars.mpr (occurrence_var_mem ho)) - apply ((mem_crossingSites φ _).1 hp).2.1 - apply List.mem_map.mpr - refine ⟨φ.distinctVars.idxOf o.2.2.1, ?_, rfl⟩ - apply List.mem_range.mpr - simp only [SAT.incidenceGraph, List.length_range] - omega - -/-- The executable first entry is the original variable's ordinary cell signal. -/ -theorem wire_first_entry {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) (fallback : Variable) : - ((wire (crossingSites φ) (occurrencePath φ o)).headD (fallback, fallback)).1 = - (Layout.center (φ.distinctVars.idxOf o.2.2.1), none) := by - have hlen := occurrencePath_length_ge_two ho - have hwpos : 0 < (wire (crossingSites φ) (occurrencePath φ o)).length := by - rw [length_wire] - omega - have hhead : (wire (crossingSites φ) (occurrencePath φ o)).headD (fallback, fallback) = - (wire (crossingSites φ) (occurrencePath φ o))[0] := by - generalize hc : wire (crossingSites φ) (occurrencePath φ o) = xs at hwpos ⊢ - cases xs with - | nil => simp at hwpos - | cons a rest => rfl - rw [hhead, getElem_wire _ _ 0 (by omega)] - simp only [Nat.zero_sub] - rw [List.getD_eq_getElem _ _ (by omega)] - have hp := (occurrencePath_endpoints ho).1 - rw [List.head?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hp - rw [Option.some.inj hp] - simp only [signal, source_center_not_crossing ho, ite_false] - /-- Under the actual source width and literal-incidence bounds, raw output satisfaction implies source satisfaction. No local wire equality or endpoint assumption remains. -/ theorem eval_source_of_rawFormula {φ : CNF ℕ} diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean index d9971fc8e..e5ccff659 100755 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathGeometry public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing @@ -135,22 +136,6 @@ theorem crossingRoute_mem_openCell {e : ℕ × Crossover.SplitVariable × Route} rw [mem_openCell_add_origin_iff] simpa only [Int.reduceMul, Int.cast_ofNat] using Crossover.core_support_interior he hp -/-- Unit-adjacent integer cells differ by exactly one of the four cardinal displacements. -/ -theorem unit_neighbor_cases {p q : Point} (h : Orthogonal.length p q = 1) : - q = p + (-1, 0) ∨ q = p + (1, 0) ∨ q = p + (0, -1) ∨ q = p + (0, 1) := by - rcases p with ⟨px, py⟩ - rcases q with ⟨qx, qy⟩ - simp only [Orthogonal.length] at h - simp only [Prod.mk_add_mk, Prod.mk.injEq] - omega - -/-- Neighboring unit cells use exactly the same geometric midpoint for their shared port. -/ -theorem shared_cellPort {p q : Point} (h : Orthogonal.length p q = 1) : - cellPort 120 p (side p q) = cellPort 120 q (side q p) := by - rcases p with ⟨px, py⟩ - rcases unit_neighbor_cases h with rfl | rfl | rfl | rfl <;> - norm_num [side, cellPort, cellOrigin, Prod.ext_iff] <;> omega - private theorem mem_support_pair {a b : Point} {p : ℝ × ℝ} : p ∈ support [a, b] ↔ p ∈ segment a b := by rw [support_cons_cons] @@ -590,282 +575,6 @@ theorem crossingClause_mem_openCell {c : Point} {pc : PlacedClause} 0 < (Crossover.clausePositions.getD ci.2 (0, 0)).2 ∧ (Crossover.clausePositions.getD ci.2 (0, 0)).2 < 240 by omega) -private theorem consecutivePair_index {r : Route} {a b : Point} - (h : (a, b) ∈ r.consecutivePairs) : - ∃ (k : ℕ) (hk : k + 1 < r.length), r[k] = a ∧ r[k + 1] = b := by - obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp h - have hk' : k + 1 < r.length := by - simpa only [List.consecutivePairs, List.length_zip, List.length_tail, - min_eq_right (Nat.sub_le _ _), Nat.lt_sub_iff_add_lt] using hk - simp only [List.consecutivePairs, List.getElem_zip, List.getElem_tail] at heq - exact ⟨k, hk', congrArg Prod.fst heq, congrArg Prod.snd heq⟩ - -private theorem mem_of_adjacent {r : Route} {p q : Point} - (h : (p, q) ∈ r.consecutivePairs ∨ (q, p) ∈ r.consecutivePairs) : p ∈ r := by - rcases h with h | h - · exact (List.of_mem_zip h).1 - · exact List.mem_of_mem_tail (List.of_mem_zip h).2 - -private theorem neighbor_of_straight {r : Route} {p q d : Point} - (ht : StraightThrough r p d) (hn : r.Nodup) - (h : (p, q) ∈ r.consecutivePairs ∨ (q, p) ∈ r.consecutivePairs) : - q = p - d ∨ q = p + d := by - rcases h with h | h - · obtain ⟨k, hk, hp, hq⟩ := consecutivePair_index h - have hh := ht.getD_neighbors hn (by omega) hp - have hd : r.getD (k + 1) p = q := by rw [List.getD_eq_getElem _ _ hk]; exact hq - rcases hh.2.2 with ⟨_, hnext⟩ | ⟨_, hnext⟩ - · exact Or.inr (hd.symm.trans hnext) - · exact Or.inl (hd.symm.trans hnext) - · obtain ⟨k, hk, hq, hp⟩ := consecutivePair_index h - have hh := ht.getD_neighbors hn hk hp - have hd : r.getD (k + 1 - 1) p = q := by - rw [Nat.add_sub_cancel, List.getD_eq_getElem _ _ (by omega)] - exact hq - rcases hh.2.2 with ⟨hprev, _⟩ | ⟨hprev, _⟩ - · exact Or.inl (hd.symm.trans hprev) - · exact Or.inr (hd.symm.trans hprev) - -private theorem horizontal_vertical_neighbors {p q : Point} - (hx : q = p - (1, 0) ∨ q = p + (1, 0)) - (hy : q = p - (0, 1) ∨ q = p + (0, 1)) : False := by - rcases hx with hx | hx <;> rcases hy with hy | hy <;> - have h := hx.symm.trans hy <;> - have h' := congrArg Prod.fst h <;> simp at h' - -private theorem canonical_neighbor_unique (G : Graph) - (hG : ∀ e ∈ G.2, e.1 ∈ G.1 ∧ e.2 ∈ G.1) - (hloop : ∀ e ∈ G.2, e.1 ≠ e.2) - (hdeg : ∀ v, G.incidenceVertices.count v ≤ 3) {i j : ℕ} - (hi : i < G.2.length) (hj : j < G.2.length) (hij : i ≠ j) {p q : Point} - (hcenter : p ∉ G.orthogonalPositions) - (hiadj : (p, q) ∈ (G.unitPath i).consecutivePairs ∨ - (q, p) ∈ (G.unitPath i).consecutivePairs) - (hjadj : (p, q) ∈ (G.unitPath j).consecutivePairs ∨ - (q, p) ∈ (G.unitPath j).consecutivePairs) : False := by - have hn := Graph.unitPath_nodup G hG hloop hi - have hm := Graph.unitPath_nodup G hG hloop hj - rcases Graph.unitPath_crossing_neighbors G hG hloop hdeg hi hj hij hcenter - (mem_of_adjacent hiadj) (mem_of_adjacent hjadj) with ⟨hx, hy⟩ | ⟨hy, hx⟩ - · exact horizontal_vertical_neighbors (neighbor_of_straight hx hn hiadj) - (neighbor_of_straight hy hm hjadj) - · exact horizontal_vertical_neighbors (neighbor_of_straight hx hm hjadj) - (neighbor_of_straight hy hn hiadj) - -private theorem unit_not_both_centers (G : Graph) {p q : Point} - (hunit : Orthogonal.length p q = 1) (hp : p ∈ G.orthogonalPositions) - (hq : q ∈ G.orthogonalPositions) : False := by - obtain ⟨i, _, rfl⟩ := List.mem_map.mp hp - obtain ⟨j, _, rfl⟩ := List.mem_map.mp hq - simp only [Orthogonal.length, Layout.center] at hunit - omega - -/-- Two actual canonical paths cannot share a unit grid edge, even in opposite directions. -This count-free uniqueness statement also applies to the final step into a clause cell. -/ -theorem paths_shared_step_index {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {i j : ℕ} (hi : i < (paths φ).length) (hj : j < (paths φ).length) {p q : Point} - (he : (p, q) ∈ ((paths φ).getD i []).consecutivePairs) - (hf : (p, q) ∈ ((paths φ).getD j []).consecutivePairs ∨ - (q, p) ∈ ((paths φ).getD j []).consecutivePairs) : i = j := by - by_contra hij - have hi' : i < (SAT.incidenceGraph φ).2.length := by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi - have hj' : j < (SAT.incidenceGraph φ).2.length := by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hj - change (p, q) ∈ ((SAT.incidenceGraph φ).unitPath i).consecutivePairs at he - change (p, q) ∈ ((SAT.incidenceGraph φ).unitPath j).consecutivePairs ∨ - (q, p) ∈ ((SAT.incidenceGraph φ).unitPath j).consecutivePairs at hf - have hG : ∀ e ∈ (SAT.incidenceGraph φ).2, - e.1 ∈ (SAT.incidenceGraph φ).1 ∧ e.2 ∈ (SAT.incidenceGraph φ).1 := - fun _ => SAT.incidenceGraph_endpoints - have hloop : ∀ e ∈ (SAT.incidenceGraph φ).2, e.1 ≠ e.2 := - fun _ => SAT.incidenceGraph_loopless - have hdeg := SAT.incidenceGraph_degree_le hw hv - by_cases hp : p ∈ (SAT.incidenceGraph φ).orthogonalPositions - · have hq : q ∉ (SAT.incidenceGraph φ).orthogonalPositions := fun hq => - unit_not_both_centers _ (Graph.unitPath_unit _ hG hloop hi' he) hp hq - exact canonical_neighbor_unique _ hG hloop hdeg hi' hj' hij hq (Or.inr he) hf.symm - · exact canonical_neighbor_unique _ hG hloop hdeg hi' hj' hij hp (Or.inl he) hf - -/-- At a unit neighbor, the facing side determines the neighbor itself. -/ -theorem side_injective_on_unit_neighbors {p q t : Point} - (hq : Orthogonal.length p q = 1) (ht : Orthogonal.length p t = 1) - (hside : side p q = side p t) : q = t := by - rcases p with ⟨px, py⟩ - rcases unit_neighbor_cases hq with rfl | rfl | rfl | rfl <;> - rcases unit_neighbor_cases ht with rfl | rfl | rfl | rfl <;> - first | rfl | norm_num [side] at hside - -private def stepPorts (e : Point × Point) : List (Point × Fin 4) := - [(e.1, side e.1 e.2), (e.2, side e.2 e.1)] - -private theorem unit_reverse {p q : Point} (h : Orthogonal.length p q = 1) : - Orthogonal.length q p = 1 := by - simp only [Orthogonal.length] at h ⊢ - omega - -private theorem stepPorts_inter {e f : Point × Point} {x : Point × Fin 4} - (he : Orthogonal.length e.1 e.2 = 1) (hf : Orthogonal.length f.1 f.2 = 1) - (hx : x ∈ stepPorts e) (hy : x ∈ stepPorts f) : - e = f ∨ e = (f.2, f.1) := by - rcases e with ⟨a, b⟩ - rcases f with ⟨c, d⟩ - simp only [stepPorts, List.mem_cons, List.not_mem_nil, or_false] at hx hy - rcases hx with rfl | rfl <;> rcases hy with hy | hy - · obtain ⟨h, hs⟩ := Prod.mk.inj hy - subst c - have hb := side_injective_on_unit_neighbors he hf hs - exact Or.inl (Prod.ext rfl hb) - · obtain ⟨h, hs⟩ := Prod.mk.inj hy - subst d - have hb := side_injective_on_unit_neighbors he (unit_reverse hf) hs - exact Or.inr (Prod.ext rfl hb) - · obtain ⟨h, hs⟩ := Prod.mk.inj hy - subst c - have ha := side_injective_on_unit_neighbors (unit_reverse he) hf hs - exact Or.inr (Prod.ext ha rfl) - · obtain ⟨h, hs⟩ := Prod.mk.inj hy - subst d - have ha := side_injective_on_unit_neighbors (unit_reverse he) (unit_reverse hf) hs - exact Or.inl (Prod.ext ha rfl) - -private theorem routePorts_nodup {r : Route} (hn : r.Nodup) - (hu : ∀ e ∈ r.consecutivePairs, Orthogonal.length e.1 e.2 = 1) : - (r.consecutivePairs.flatMap stepPorts).Nodup := by - apply List.nodup_flatMap.mpr - constructor - · intro e he - have hne := (axisAligned_of_length_eq_one (hu e he)).2 - simp only [stepPorts, List.nodup_cons, List.not_mem_nil, List.nodup_nil, - List.mem_singleton, not_false_eq_true, and_true] - exact fun h => hne (congrArg Prod.fst h) - · rw [List.pairwise_iff_getElem] - intro i j hi hj hij x hx hy - have hi' : i + 1 < r.length := by - simp only [List.consecutivePairs, List.length_zip, List.length_tail] at hi - omega - have hj' : j + 1 < r.length := by - simp only [List.consecutivePairs, List.length_zip, List.length_tail] at hj - omega - rcases stepPorts_inter (hu _ (List.getElem_mem hi)) (hu _ (List.getElem_mem hj)) hx hy - with heq | heq - · have heq' : r[i] = r[j] := by - simpa only [List.consecutivePairs, List.getElem_zip, List.getElem_tail] using - congrArg Prod.fst heq - have := hn.eq_of_getElem_eq (by omega) (by omega) heq' - omega - · have heq' : r[i] = r[j + 1] := by - simpa only [List.consecutivePairs, List.getElem_zip, List.getElem_tail] using - congrArg Prod.fst heq - have := hn.eq_of_getElem_eq (by omega) hj' heq' - omega - -/-- All directed cell ports in the actual canonical paths are distinct. Both halves of every -unit step are included, even the final clause-directed half. No path witness is assumed. -/ -theorem pathPorts_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - ((paths φ).flatMap fun r => r.consecutivePairs.flatMap fun e => - [(e.1, side e.1 e.2), (e.2, side e.2 e.1)]).Nodup := by - have hi_edge {i : ℕ} (hi : i < (paths φ).length) : - i < (SAT.incidenceGraph φ).2.length := by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi - have hn {i : ℕ} (hi : i < (paths φ).length) : ((paths φ)[i]).Nodup := by - have h := Graph.unitPath_nodup (SAT.incidenceGraph φ) - (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) (hi_edge hi) - change ((paths φ).getD i []).Nodup at h - rwa [List.getD_eq_getElem _ _ hi] at h - have hu {i : ℕ} (hi : i < (paths φ).length) {e : Point × Point} - (he : e ∈ ((paths φ)[i]).consecutivePairs) : Orthogonal.length e.1 e.2 = 1 := by - apply Graph.unitPath_unit (SAT.incidenceGraph φ) - (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) (hi_edge hi) - change e ∈ ((paths φ).getD i []).consecutivePairs - rwa [List.getD_eq_getElem _ _ hi] - change ((paths φ).flatMap fun r => r.consecutivePairs.flatMap stepPorts).Nodup - apply List.nodup_flatMap.mpr - constructor - · intro r hr - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr - exact routePorts_nodup (hn hi) (fun _ he => hu hi he) - · rw [List.pairwise_iff_getElem] - intro i j hi hj hij x hx hy - obtain ⟨e, he, hx⟩ := List.mem_flatMap.mp hx - obtain ⟨f, hf, hy⟩ := List.mem_flatMap.mp hy - have hi_step : e ∈ ((paths φ).getD i []).consecutivePairs := by - rwa [List.getD_eq_getElem _ _ hi] - have hj_step : (e.1, e.2) ∈ ((paths φ).getD j []).consecutivePairs ∨ - (e.2, e.1) ∈ ((paths φ).getD j []).consecutivePairs := by - rw [List.getD_eq_getElem _ _ hj] - rcases stepPorts_inter (hu hi he) (hu hj hf) hx hy with heq | heq - · exact Or.inl (heq.symm ▸ hf) - · exact Or.inr (by simpa only [heq] using hf) - have := paths_shared_step_index hw hv hi hj hi_step hj_step - omega - -/-- Equal boundary midpoints identify the same unordered unit grid edge. -/ -theorem cellPort_step_eq_cases {p q a b : Point} - (hpq : Orthogonal.length p q = 1) (hab : Orthogonal.length a b = 1) - (h : cellPort 120 p (side p q) = cellPort 120 a (side a b)) : - (p = a ∧ q = b) ∨ (p = b ∧ q = a) := by - rcases p with ⟨px, py⟩ - rcases a with ⟨ax, ay⟩ - rcases unit_neighbor_cases hpq with rfl | rfl | rfl | rfl <;> - rcases unit_neighbor_cases hab with rfl | rfl | rfl | rfl <;> - norm_num [side, cellPort, cellOrigin, Prod.ext_iff] at h ⊢ <;> omega - -/-- One geometric midpoint per actual unit step gives a duplicate-free list. -This includes final steps, so any prefix selection used for binary clauses remains distinct. -/ -theorem pathMidpoints_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - ((paths φ).flatMap fun r => r.consecutivePairs.map fun e => - cellPort 120 e.1 (side e.1 e.2)).Nodup := by - let steps := (paths φ).flatMap List.consecutivePairs - have hu {e : Point × Point} (he : e ∈ steps) : Orthogonal.length e.1 e.2 = 1 := by - obtain ⟨r, hr, he⟩ := List.mem_flatMap.mp he - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr - have hi' : i < (SAT.incidenceGraph φ).2.length := by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi - apply Graph.unitPath_unit (SAT.incidenceGraph φ) - (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) hi' - change e ∈ ((paths φ).getD i []).consecutivePairs - rwa [List.getD_eq_getElem _ _ hi] - have hp : (steps.flatMap stepPorts).Nodup := by - have h := pathPorts_nodup hw hv - change ((paths φ).flatMap fun r => r.consecutivePairs.flatMap stepPorts).Nodup at h - simpa only [steps, List.flatMap_assoc] using h - have hpair := (List.nodup_flatMap.mp hp).2 - have hmid : (steps.map fun e => cellPort 120 e.1 (side e.1 e.2)).Nodup := by - apply List.pairwise_map.mpr - apply hpair.imp_of_mem - intro e f he hf hd heq - have hx : (e.1, side e.1 e.2) ∈ stepPorts e := by simp [stepPorts] - rcases cellPort_step_eq_cases (hu he) (hu hf) heq with ⟨h₁, h₂⟩ | ⟨h₁, h₂⟩ - · have heq' : e = f := Prod.ext h₁ h₂ - exact hd hx (heq' ▸ hx) - · have heq' : e = (f.2, f.1) := Prod.ext h₁ h₂ - exact hd hx (by simp [stepPorts, heq']) - simpa only [steps, List.map_flatMap] using hmid - -/-- Distinct integer cells have distinct displayed centers. -/ -theorem center_injective : Function.Injective center := by - intro p q h - have hp := center_mem_openCell (r := 120) (by decide) p - have hq := center_mem_openCell (r := 120) (by decide) q - change realPoint (center p) ∈ openCell 120 p at hp - change realPoint (center q) ∈ openCell 120 q at hq - rw [← h] at hq - exact cell_eq_of_mem_open_closed (by decide) hp - ⟨hq.1.le, hq.2.1.le, hq.2.2.1.le, hq.2.2.2.le⟩ - -/-- Original clause cells are declared source centers and are never selected as crossings. -/ -theorem clause_cell_not_mem_crossingSites (φ : CNF ℕ) {i : ℕ} (hi : i < φ.length) : - Layout.center (φ.distinctVars.length + i) ∉ crossingSites φ := by - intro h - apply ((mem_crossingSites φ _).mp h).2.1 - refine List.mem_map.mpr ⟨φ.distinctVars.length + i, List.mem_range.mpr ?_, rfl⟩ - simp only [SAT.incidenceGraph, List.length_range] - omega - /-- Original clause positions are pairwise distinct, including repeated and empty clauses. -/ theorem originalPositions_nodup (φ : CNF ℕ) (sites : List Point) : ((originalClauses φ sites).map fun pc => pc.2.1).Nodup := by @@ -1049,48 +758,6 @@ theorem raw_variable_cell_membership (φ : CNF ℕ) {v : Variable} | exact Or.inr ⟨o, ho, (List.of_mem_zip he).1⟩ | exact Or.inr ⟨o, ho, List.mem_of_mem_tail (List.of_mem_zip he).2⟩ -private theorem occurrencePath_clause_center_iff {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) {i : ℕ} (hi : i < φ.length) : - Layout.center (φ.distinctVars.length + i) ∈ occurrencePath φ o ↔ i = o.1 := by - have hoidx := occurrence_index_lt ho - have h := Graph.unitPath_center_iff (SAT.incidenceGraph φ) - (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) hoidx - (w := φ.distinctVars.length + i) (by simp only [SAT.incidenceGraph, List.length_range]; omega) - have he : (SAT.incidenceGraph φ).2[(Cslib.Logic.PL.occurrences φ).idxOf o] = - (φ.distinctVars.idxOf o.2.2.1, φ.distinctVars.length + o.1) := by - simp only [SAT.incidenceGraph, List.getElem_map] - rw [List.getElem_idxOf (List.idxOf_lt_length_of_mem ho)] - have hb := SAT.incidenceGraph_bipartite (List.getElem_mem hoidx) - rw [he] at hb h - change Layout.center (φ.distinctVars.length + i) ∈ occurrencePath φ o ↔ - φ.distinctVars.length + i = (List.range _).idxOf (φ.distinctVars.idxOf o.2.2.1) ∨ - φ.distinctVars.length + i = (List.range _).idxOf (φ.distinctVars.length + o.1) at h - rw [idxOf_range_eq (by omega), idxOf_range_eq hb.2.2] at h - exact h.trans (by omega) - -/-- No source clause center is used as a signal cell before a path's final endpoint. -/ -theorem clause_cell_not_mem_path_dropLast {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) {i : ℕ} (hi : i < φ.length) : - Layout.center (φ.distinctVars.length + i) ∉ (occurrencePath φ o).dropLast := by - intro hp - have hi' := (occurrencePath_clause_center_iff ho hi).mp - ((List.dropLast_sublist _).subset hp) - subst i - obtain ⟨k, hk, hget⟩ := List.mem_iff_getElem.mp hp - have hlen := occurrencePath_length_ge_two ho - have hend := (occurrencePath_endpoints ho).2 - rw [List.getLast?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hend - have hk' : k < (occurrencePath φ o).length := by - simp only [List.length_dropLast] at hk - omega - have heq : (occurrencePath φ o)[k] = - (occurrencePath φ o)[(occurrencePath φ o).length - 1] := by - rw [Option.some.inj hend] - simpa only [List.getElem_dropLast] using hget - have hidx := (occurrencePath_nodup ho).eq_of_getElem_eq hk' (by omega) heq - simp only [List.length_dropLast] at hk - omega - /-- Actual output variables never occupy a source clause cell. -/ theorem raw_variable_not_clause_cell {φ : CNF ℕ} {v : Variable} (hv : v ∈ (rawFormula φ).vars) {i : ℕ} (hi : i < φ.length) : diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean index 110a7990c..a24066603 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathGeometry public import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean new file mode 100644 index 000000000..fb99e4398 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean @@ -0,0 +1,393 @@ +/- +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.Paths +public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree +public import Complexity.Logics.Propositional.CNF.Planar.CrossoverSplit +import Complexity.Foundations.Data.List.Filter +import Mathlib.Data.List.GetD +import Mathlib.Tactic.SplitIfs + +/-! +# Compatible assignments on canonical paths + +The optional crossover tags are retained only as a logical assignment bridge for the +paired compiler. There is no second output formula or drawing. A compatible assignment +carries each source value along its path and satisfies each selected fixed crossover. + +## Main definitions + +* `Cslib.Complexity.SAT.PlanarCompile.Variable`, `.signal`, `.wire`: the logical path bridge. + +## Main results + +* `Cslib.Complexity.SAT.PlanarCompile.occurrencePath_crossing_straight`. +* `Cslib.Complexity.SAT.PlanarCompile.source_center_not_crossing`. +* `Cslib.Complexity.SAT.PlanarCompile.ordinary_cell_source_eq`. +* `Cslib.Complexity.SAT.PlanarCompile.crossing_axis_occurrence_eq`. +* `Cslib.Complexity.SAT.PlanarCompile.exists_compatible_assignment`. + +## References + +These are the shared canonical incidence-path constructions and certificates. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.PlanarCompile + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- A cell's ordinary signal, or a local variable of its crossover. -/ +abbrev Variable := Point × Option Crossover.SplitVariable + +/-- The signal presented by a cell toward a neighboring cell. -/ +def signal (sites : List Point) (p q : Point) : Variable := + (p, if p ∈ sites then some (Crossover.splitTerminal (side p q)) else none) + +/-- Every cell before the original clause vertex contributes an entry/exit signal pair. +At the source endpoint the unused entry defaults to the source's own ordinary signal. -/ +def wire (sites : List Point) (r : Route) : List (Variable × Variable) := + r.dropLast.zipIdx.map fun (p, i) => + (signal sites p (r.getD (i - 1) p), signal sites p (r.getD (i + 1) p)) + +/-- A path contributes one signal cell for each point before its final clause vertex. -/ +theorem length_wire (sites : List Point) (r : Route) : + (wire sites r).length = r.length - 1 := by simp [wire] + +/-- Every path of at least two points yields a nonempty cell wire. -/ +theorem wire_ne_nil (sites : List Point) (r : Route) (h : 2 ≤ r.length) : wire sites r ≠ [] := by + intro he + have hl := length_wire sites r + rw [he, List.length_nil] at hl + omega + +/-- Exact indexed cell signals in the executable wire list. -/ +theorem getElem_wire (sites : List Point) (r : Route) (i : ℕ) (hi : i < r.length - 1) : + (wire sites r)[i]'(by simpa [wire] using hi) = + (signal sites r[i] (r.getD (i - 1) r[i]), + signal sites r[i] (r.getD (i + 1) r[i])) := by + simp only [wire, List.getElem_map, List.getElem_zipIdx, Nat.zero_add, List.getElem_dropLast] + +/-- The actual graph edge has the occurrence's original variable and clause labels. -/ +theorem occurrence_edgeEndpoint {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) (side : Bool) : + (SAT.incidenceGraph φ).edgeEndpoint ((Cslib.Logic.PL.occurrences φ).idxOf o) side = + if side then φ.distinctVars.length + o.1 else φ.distinctVars.idxOf o.2.2.1 := by + unfold Graph.edgeEndpoint + rw [List.getD_eq_getElem _ _ (occurrence_index_lt ho)] + simp only [SAT.incidenceGraph, List.getElem_map, + List.getElem_idxOf (List.idxOf_lt_length_of_mem ho)] + +/-- A selected crossing is traversed straight along one coordinate axis by each occupying path. -/ +theorem occurrencePath_crossing_straight {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) + {p : Point} (hp : p ∈ crossingSites φ) (hpi : p ∈ occurrencePath φ o) : + StraightThrough (occurrencePath φ o) p (1, 0) ∨ + StraightThrough (occurrencePath φ o) p (0, 1) := by + have hsite := (mem_crossingSites φ p).1 hp + let G := SAT.incidenceGraph φ + have hG : ∀ e ∈ G.2, e.1 ∈ G.1 ∧ e.2 ∈ G.1 := + fun _ he => SAT.incidenceGraph_endpoints he + have hloop : ∀ e ∈ G.2, e.1 ≠ e.2 := fun _ he => SAT.incidenceGraph_loopless he + have hdeg : ∀ v, G.incidenceVertices.count v ≤ 3 := SAT.incidenceGraph_degree_le hw hv + have hi := occurrence_index_lt ho + obtain ⟨j, hj, hji, hpj⟩ := List.exists_other_index_of_two_le_filter_contains (paths φ) p + ((Cslib.Logic.PL.occurrences φ).idxOf o) + (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi) hsite.2.2 + have hj' : j < G.2.length := by + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hj + have hpi' : p ∈ G.unitPath ((Cslib.Logic.PL.occurrences φ).idxOf o) := by + simpa only [occurrencePath_eq_unitPath] using hpi + have hpj' : p ∈ G.unitPath j := by + unfold Graph.unitPath + change p ∈ (SAT.incidenceGraph φ).unitPaths.getD j [] + rw [← paths_eq_unitPaths, List.getD_eq_getElem _ _ hj] + exact hpj + have hnb := Graph.unitPath_crossing_neighbors G hG hloop hdeg hi hj' (Ne.symm hji) + hsite.2.1 hpi' hpj' + rcases hnb with ⟨h, _⟩ | ⟨h, _⟩ + · exact Or.inl (by simpa only [occurrencePath_eq_unitPath] using h) + · exact Or.inr (by simpa only [occurrencePath_eq_unitPath] using h) + +/-- The initial source center is excluded from the actual selected crossing list. -/ +theorem source_center_not_crossing {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) : + Layout.center (φ.distinctVars.idxOf o.2.2.1) ∉ crossingSites φ := by + intro hp + have hvar := List.idxOf_lt_length_of_mem + (CNF.mem_distinctVars.mpr (variable_mem_of_mem_occurrences ho)) + apply ((mem_crossingSites φ _).1 hp).2.1 + apply List.mem_map.mpr + refine ⟨φ.distinctVars.idxOf o.2.2.1, ?_, rfl⟩ + apply List.mem_range.mpr + simp only [SAT.incidenceGraph, List.length_range] + omega + +/-- The executable first entry is the original variable's ordinary cell signal. -/ +theorem wire_first_entry {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) (fallback : Variable) : + ((wire (crossingSites φ) (occurrencePath φ o)).headD (fallback, fallback)).1 = + (Layout.center (φ.distinctVars.idxOf o.2.2.1), none) := by + have hlen := occurrencePath_length_ge_two ho + have hwpos : 0 < (wire (crossingSites φ) (occurrencePath φ o)).length := by + rw [length_wire] + omega + have hhead : (wire (crossingSites φ) (occurrencePath φ o)).headD (fallback, fallback) = + (wire (crossingSites φ) (occurrencePath φ o))[0] := by + generalize hc : wire (crossingSites φ) (occurrencePath φ o) = xs at hwpos ⊢ + cases xs with + | nil => simp at hwpos + | cons a rest => rfl + rw [hhead, getElem_wire _ _ 0 (by omega)] + simp only [Nat.zero_sub] + rw [List.getD_eq_getElem _ _ (by omega)] + have hp := (occurrencePath_endpoints ho).1 + rw [List.head?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hp + rw [Option.some.inj hp] + simp only [signal, source_center_not_crossing ho, ite_false] + +private theorem path_mem_paths_get {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∈ occurrencePath φ o) : + p ∈ (paths φ)[(Cslib.Logic.PL.occurrences φ).idxOf o]'(by + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho) := by + unfold occurrencePath at hp + rwa [List.getD_eq_getElem _ _ (by + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho)] at hp + +/-- Two different occurrence paths sharing an ordinary cell meet at a declared vertex center. -/ +theorem shared_ordinary_cell_center {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) + (ht : t ∈ Cslib.Logic.PL.occurrences φ) (hot : o ≠ t) {p : Point} + (hp : p ∉ crossingSites φ) (hpo : p ∈ occurrencePath φ o) + (hpt : p ∈ occurrencePath φ t) : p ∈ (SAT.incidenceGraph φ).orthogonalPositions := by + by_contra hc + have hij : (Cslib.Logic.PL.occurrences φ).idxOf o ≠ + (Cslib.Logic.PL.occurrences φ).idxOf t := fun he => hot ((List.idxOf_inj ho).1 he) + have hcandidate := Graph.unitPath_shared_mem_crossingCandidates (SAT.incidenceGraph φ) + (fun _ he => SAT.incidenceGraph_endpoints he) + (fun _ he => SAT.incidenceGraph_loopless he) (SAT.incidenceGraph_degree_le hw hv) + (occurrence_index_lt ho) (occurrence_index_lt ht) hij hc + (by simpa only [occurrencePath_eq_unitPath] using hpo) + (by simpa only [occurrencePath_eq_unitPath] using hpt) + apply hp + apply (mem_crossingSites φ p).2 + refine ⟨hcandidate, hc, ?_⟩ + exact List.two_le_filter_contains_of_indices (paths φ) p + (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho) + (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ht) + hij (path_mem_paths_get ho hpo) (path_mem_paths_get ht hpt) + +/-- No retained wire cell is the clause-center endpoint removed by `dropLast`. -/ +theorem clause_center_not_mem_dropLast {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) : + Layout.center (φ.distinctVars.length + o.1) ∉ (occurrencePath φ o).dropLast := by + intro hp + obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hp + have hlen := occurrencePath_length_ge_two ho + have hk' : k < (occurrencePath φ o).length := by + simp only [List.length_dropLast] at hk + omega + have hlast := (occurrencePath_endpoints ho).2 + rw [List.getLast?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hlast + have heq' : (occurrencePath φ o)[k] = + (occurrencePath φ o)[(occurrencePath φ o).length - 1] := by + rw [← List.getElem_dropLast hk, heq, Option.some.inj hlast] + have hidx := (occurrencePath_nodup ho).getElem_inj_iff.1 heq' + simp only [List.length_dropLast] at hk + omega + +/-- A retained cell at a declared center is the source-variable center of its occurrence. -/ +theorem dropLast_center_eq_source {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} + (hp : p ∈ (occurrencePath φ o).dropLast) + (hc : p ∈ (SAT.incidenceGraph φ).orthogonalPositions) : + p = Layout.center (φ.distinctVars.idxOf o.2.2.1) := by + obtain ⟨w, hw, rfl⟩ := List.mem_map.mp hc + have hw' := List.mem_range.mp hw + have hwmem : w ∈ (SAT.incidenceGraph φ).1 := by + apply List.mem_range.mpr + simpa only [SAT.incidenceGraph, List.length_range] using hw' + have hi := List.idxOf_lt_length_of_mem hwmem + have hidx : (SAT.incidenceGraph φ).1.idxOf w = w := by + simpa only [SAT.incidenceGraph, List.getElem_range] using List.getElem_idxOf hi + have h := (Graph.unitPath_declared_center_iff (SAT.incidenceGraph φ) + (fun _ he => SAT.incidenceGraph_endpoints he) + (fun _ he => SAT.incidenceGraph_loopless he) (occurrence_index_lt ho) hwmem).1 + (by rw [hidx]; simpa only [occurrencePath_eq_unitPath] using List.dropLast_subset _ hp) + simp only [SAT.incidenceGraph, List.getElem_map, + List.getElem_idxOf (List.idxOf_lt_length_of_mem ho)] at h + rcases h with h | h + · rw [h] + · exact False.elim (clause_center_not_mem_dropLast ho (h ▸ hp)) + +/-- All occurrences using an ordinary retained cell have the same original variable. -/ +theorem ordinary_cell_source_eq {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) + (ht : t ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∉ crossingSites φ) + (hpo : p ∈ (occurrencePath φ o).dropLast) + (hpt : p ∈ (occurrencePath φ t).dropLast) : o.2.2.1 = t.2.2.1 := by + by_cases hot : o = t + · rw [hot] + have hc := shared_ordinary_cell_center hw hv ho ht hot hp + (List.dropLast_subset _ hpo) (List.dropLast_subset _ hpt) + have he := (dropLast_center_eq_source ho hpo hc).symm.trans + (dropLast_center_eq_source ht hpt hc) + have hx := congrArg Prod.fst he + simp only [Layout.center] at hx + have hi : φ.distinctVars.idxOf o.2.2.1 = φ.distinctVars.idxOf t.2.2.1 := by omega + apply (List.idxOf_inj ?_).1 hi + apply CNF.mem_distinctVars.mpr + rw [← Cslib.Logic.PL.map_occurrences] + exact List.mem_map_of_mem ho + +private theorem not_both_straight {r : Route} (hn : r.Nodup) {p : Point} (hp : p ∈ r) + (hh : StraightThrough r p (1, 0)) (hv : StraightThrough r p (0, 1)) : False := by + obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hp + obtain ⟨_, _, hhn⟩ := hh.getD_neighbors hn hk heq + obtain ⟨_, _, hvn⟩ := hv.getD_neighbors hn hk heq + rcases hhn with ⟨hh, _⟩ | ⟨hh, _⟩ <;> rcases hvn with ⟨hv, _⟩ | ⟨hv, _⟩ + all_goals + have hx := congrArg Prod.fst (hh.symm.trans hv) + simp only [Prod.fst_sub, Prod.fst_add] at hx + omega + +/-- The occurrence carrying either coordinate-axis signal at a crossing is unique. -/ +theorem crossing_axis_occurrence_eq {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) + (ht : t ∈ Cslib.Logic.PL.occurrences φ) {p d : Point} + (hp : p ∈ crossingSites φ) (hpo : p ∈ occurrencePath φ o) + (hpt : p ∈ occurrencePath φ t) (hd : d = (1, 0) ∨ d = (0, 1)) + (hs : StraightThrough (occurrencePath φ o) p d) + (hts : StraightThrough (occurrencePath φ t) p d) : o = t := by + by_contra hot + have hij : (Cslib.Logic.PL.occurrences φ).idxOf o ≠ + (Cslib.Logic.PL.occurrences φ).idxOf t := fun he => hot ((List.idxOf_inj ho).1 he) + have hn := Graph.unitPath_crossing_neighbors (SAT.incidenceGraph φ) + (fun _ he => SAT.incidenceGraph_endpoints he) + (fun _ he => SAT.incidenceGraph_loopless he) (SAT.incidenceGraph_degree_le hw hv) + (occurrence_index_lt ho) (occurrence_index_lt ht) hij + ((mem_crossingSites φ p).1 hp).2.1 + (by simpa only [occurrencePath_eq_unitPath] using hpo) + (by simpa only [occurrencePath_eq_unitPath] using hpt) + rw [← occurrencePath_eq_unitPath, ← occurrencePath_eq_unitPath] at hn + rcases hd with rfl | rfl + · rcases hn with ⟨_, htvert⟩ | ⟨hovert, _⟩ + · exact not_both_straight (occurrencePath_nodup ht) hpt hts htvert + · exact not_both_straight (occurrencePath_nodup ho) hpo hs hovert + · rcases hn with ⟨hohor, _⟩ | ⟨_, hthor⟩ + · exact not_both_straight (occurrencePath_nodup ho) hpo hohor hs + · exact not_both_straight (occurrencePath_nodup ht) hpt hthor hts + +open Classical in +private noncomputable def chosenValue (τ : ℕ → Bool) (P : Occurrence ℕ → Prop) : Bool := + if h : ∃ o, P o then τ (Classical.choose h).2.2.1 else false + +private theorem chosenValue_eq (τ : ℕ → Bool) (P : Occurrence ℕ → Prop) + {o : Occurrence ℕ} (ho : P o) (heq : ∀ t, P t → t.2.2.1 = o.2.2.1) : + chosenValue τ P = τ o.2.2.1 := by + classical + have h : ∃ t, P t := ⟨o, ho⟩ + simp only [chosenValue, dite_eq_left h] + rw [heq _ (Classical.choose_spec h)] + +/-- Every source assignment extends compatibly to all actual wire cells and crossover blocks. +The choice of auxiliary values is logical; this theorem makes no computational claim. -/ +theorem exists_compatible_assignment {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) (τ : ℕ → Bool) : + ∃ σ : Variable → Bool, + (∀ o ∈ Cslib.Logic.PL.occurrences φ, + ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), + σ c.1 = τ o.2.2.1 ∧ σ c.2 = τ o.2.2.1) ∧ + (∀ p ∈ crossingSites φ, Crossover.splitFormula.eval (fun v => σ (p, some v)) = true) := by + classical + let ordinary (p : Point) := chosenValue τ (fun o => + o ∈ Cslib.Logic.PL.occurrences φ ∧ p ∈ (occurrencePath φ o).dropLast) + let axis (p d : Point) := chosenValue τ (fun o => + o ∈ Cslib.Logic.PL.occurrences φ ∧ p ∈ occurrencePath φ o ∧ + StraightThrough (occurrencePath φ o) p d) + have hord {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} + (hp : p ∉ crossingSites φ) (hpo : p ∈ (occurrencePath φ o).dropLast) : + ordinary p = τ o.2.2.1 := by + apply chosenValue_eq τ _ ⟨ho, hpo⟩ + intro t ht + exact ordinary_cell_source_eq hw hv ht.1 ho hp ht.2 hpo + have haxis {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p d : Point} + (hp : p ∈ crossingSites φ) (hpo : p ∈ occurrencePath φ o) + (hd : d = (1, 0) ∨ d = (0, 1)) (hs : StraightThrough (occurrencePath φ o) p d) : + axis p d = τ o.2.2.1 := by + apply chosenValue_eq τ _ ⟨ho, hpo, hs⟩ + intro t ht + rw [crossing_axis_occurrence_eq hw hv ht.1 ho hp ht.2.1 hpo hd ht.2.2 hs] + let cross (p : Point) : Crossover.SplitVariable → Bool := + Classical.choose (Crossover.exists_split_holds (axis p (1, 0)) (axis p (0, 1))) + have hcross (p : Point) := + Classical.choose_spec (Crossover.exists_split_holds (axis p (1, 0)) (axis p (0, 1))) + let σ : Variable → Bool := fun v => match v.2 with + | none => ordinary v.1 + | some a => cross v.1 a + refine ⟨σ, ?_, fun p _ => (hcross p).1⟩ + intro o ho c hc + unfold wire at hc + obtain ⟨⟨p, k⟩, hpk, rfl⟩ := List.mem_map.mp hc + have hget := List.mem_zipIdx_iff_getElem?.mp hpk + obtain ⟨hk, heq⟩ := List.getElem?_eq_some_iff.mp hget + have hk' : k < (occurrencePath φ o).length := by + simp only [List.length_dropLast] at hk + omega + have heq' : (occurrencePath φ o)[k] = p := by + rw [← List.getElem_dropLast hk] + exact heq + have hpo : p ∈ occurrencePath φ o := heq' ▸ List.getElem_mem hk' + change (List.dropLast (occurrencePath φ o))[k] = p at heq + have hpod : p ∈ (occurrencePath φ o).dropLast := by + rw [← heq] + exact List.getElem_mem hk + by_cases hp : p ∈ crossingSites φ + · have hl : side p (p - (1, 0)) = 0 := by + rcases p with ⟨x, y⟩ + simp only [side, Prod.fst_sub, Prod.snd_sub] + split_ifs <;> first | rfl | omega + have hr : side p (p + (1, 0)) = 1 := by + rcases p with ⟨x, y⟩ + simp only [side, Prod.fst_add, Prod.snd_add] + split_ifs <;> first | rfl | omega + have ht : side p (p - (0, 1)) = 2 := by + rcases p with ⟨x, y⟩ + simp only [side, Prod.fst_sub, Prod.snd_sub] + split_ifs <;> first | rfl | omega + have hb : side p (p + (0, 1)) = 3 := by + rcases p with ⟨x, y⟩ + simp only [side, Prod.fst_add, Prod.snd_add] + split_ifs <;> first | rfl | omega + rcases occurrencePath_crossing_straight hw hv ho hp hpo with hs | hs + · have hav := haxis ho hp hpo (Or.inl rfl) hs + have hports := (hcross p).2 + obtain ⟨_, _, hnb⟩ := hs.getD_neighbors (occurrencePath_nodup ho) hk' heq' + rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ + all_goals + simp only [hprev, hnext, signal, hp, ite_true, hl, hr, Crossover.splitTerminal] + exact ⟨by simpa only [σ, cross, hports.1, hports.2.1] using hav, + by simpa only [σ, cross, hports.1, hports.2.1] using hav⟩ + · have hav := haxis ho hp hpo (Or.inr rfl) hs + have hports := (hcross p).2.2.2 + obtain ⟨_, _, hnb⟩ := hs.getD_neighbors (occurrencePath_nodup ho) hk' heq' + rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ + all_goals + simp only [hprev, hnext, signal, hp, ite_true, ht, hb, Crossover.splitTerminal] + exact ⟨by simpa only [σ, cross, hports.1, hports.2] using hav, + by simpa only [σ, cross, hports.1, hports.2] using hav⟩ + · simpa only [signal, hp, ite_false, σ] using + And.intro (hord ho hp hpod) (hord ho hp hpod) + +end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathBounds.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathBounds.lean new file mode 100644 index 000000000..f5c04ed09 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathBounds.lean @@ -0,0 +1,113 @@ +/- +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.PathData +import Mathlib.Algebra.BigOperators.Ring.List +import Mathlib.Data.List.GetD +import Mathlib.Tactic.Linarith + +/-! +# Bounds for shared incidence-path data + +Canonical path budgets, crossing counts, retained-gap counts, and 240-macrocell grid +sides are independent of the emitted clause template. No output formula is defined here. + +## Main definitions + +* `Cslib.Complexity.SAT.PlanarCompile.linkCount`: retained path gaps. +* `Cslib.Complexity.SAT.PlanarCompile.gridWidth`, `.gridHeight`: shared macrocell grid sides. + +## Main results + +* `Cslib.Complexity.SAT.PlanarCompile.crossingSites_length_le`. +* `Cslib.Complexity.SAT.PlanarCompile.paths_length`. +* `Cslib.Complexity.SAT.PlanarCompile.path_length_le`. +* `Cslib.Complexity.SAT.PlanarCompile.linkCount_le`. +* `Cslib.Complexity.SAT.PlanarCompile.gridWidth_le`. +* `Cslib.Complexity.SAT.PlanarCompile.gridHeight_le`. + +## References + +These are the shared canonical incidence-path constructions and certificates. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.PlanarCompile + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- Number of retained path gaps before the final step into each source clause. -/ +def linkCount (φ : CNF ℕ) : ℕ := + ((Cslib.Logic.PL.occurrences φ).map fun o => (occurrencePath φ o).length - 2).sum + +/-- Selected crossing sites form a sublist of the quadratic canonical cover after deduplication. +The bound counts all source literal incidences, including repetitions. -/ +theorem crossingSites_length_le (φ : CNF ℕ) : + (crossingSites φ).length ≤ 2 * φ.vars.length ^ 2 := by + unfold crossingSites + rw [length_selectDistinct_replicate] + exact (List.toFinset_card_le _).trans ((List.length_filter_le _ _).trans (by + simp [Graph.crossingCandidates_length, SAT.length_edges_incidenceGraph])) + +/-- There is one unit path per original literal incidence. -/ +theorem paths_length (φ : CNF ℕ) : (paths φ).length = φ.vars.length := by + simp [paths, SAT.length_edges_incidenceGraph] + +/-- The bounded enumerator emits at most five segment budgets plus the final endpoint. +This unconditional bound also applies to inputs that fail the degree-three restriction. -/ +theorem path_length_le {φ : CNF ℕ} {r : Route} (hr : r ∈ paths φ) : + r.length ≤ 5 * budget φ + 1 := by + change r ∈ ((SAT.incidenceGraph φ).orthogonalRoutes + (SAT.incidenceGraph φ).canonicalPorts).map (subdivideWithin (budget φ)) at hr + obtain ⟨base, hbase, rfl⟩ := List.mem_map.mp hr + have hs : base.consecutivePairs.length = 5 := by + obtain ⟨⟨e, i⟩, _, rfl⟩ := List.mem_map.mp hbase + rfl + simpa only [hs, Nat.mul_comm] using subdivideWithin_length_le (budget φ) base + +/-- Indexed access to a path obeys the same bound, including the empty fallback. -/ +theorem occurrencePath_length_le (φ : CNF ℕ) (o : Occurrence ℕ) : + (occurrencePath φ o).length ≤ 5 * budget φ + 1 := by + unfold occurrencePath + by_cases h : (Cslib.Logic.PL.occurrences φ).idxOf o < (paths φ).length + · rw [List.getD_eq_getElem _ _ h] + exact path_length_le (List.getElem_mem h) + · rw [List.getD_eq_default _ _ (Nat.le_of_not_gt h)] + exact Nat.zero_le _ + +/-- There are quadratically many links, even before checking the source restrictions. -/ +theorem linkCount_le (φ : CNF ℕ) : + linkCount φ ≤ φ.vars.length * (5 * budget φ + 1) := by + calc + _ ≤ ((Cslib.Logic.PL.occurrences φ).map fun _ => 5 * budget φ + 1).sum := + List.sum_le_sum fun o _ => (Nat.sub_le _ _).trans (occurrencePath_length_le φ o) + _ = _ := by simp [Cslib.Logic.PL.length_occurrences, Nat.mul_comm] + +/-- Horizontal side of the actual tiled drawing, including its last square. -/ +def gridWidth (φ : CNF ℕ) : ℕ := 240 * (8 * (SAT.incidenceGraph φ).1.length + 1) +/-- Vertical side of the actual tiled drawing, including its last square. -/ +def gridHeight (φ : CNF ℕ) : ℕ := + 240 * (8 * (SAT.incidenceGraph φ).1.length + 2 * (SAT.incidenceGraph φ).2.length + 1) + +/-- The horizontal grid side is at most 1920 times the source incidence size plus one. -/ +theorem gridWidth_le (φ : CNF ℕ) : + gridWidth φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := by + unfold gridWidth + rw [SAT.length_vertices_incidenceGraph] + nlinarith + +/-- The vertical grid side is at most 1920 times the source incidence size plus one. -/ +theorem gridHeight_le (φ : CNF ℕ) : + gridHeight φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := by + unfold gridHeight + rw [SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] + nlinarith + +end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathData.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathData.lean new file mode 100644 index 000000000..f08b7f279 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathData.lean @@ -0,0 +1,83 @@ +/- +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.Incidence +public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalLayout +public import Complexity.Foundations.Geometry.Orthogonal.Subdivision +public import Complexity.Foundations.Geometry.Orthogonal.Macrocell + +/-! +# Canonical incidence-path data + +The retained shared data consist of bounded unit paths, selected crossing cells, and the +common macrocell coordinates. No clauses, formula, or drawing are assembled here. + +## Main definitions + +* `Cslib.Complexity.SAT.PlanarCompile.budget`, `.paths`, `.occurrencePath`. +* `Cslib.Complexity.SAT.PlanarCompile.crossingSites`, `.side`, `.center`. + +## Main results + +* `Cslib.Complexity.SAT.PlanarCompile.mem_crossingSites`. +* `Cslib.Complexity.SAT.PlanarCompile.crossingSites_nodup`. + +## References + +These are the shared canonical incidence-path constructions and certificates. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.PlanarCompile + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- The explicit linear per-route expansion budget. -/ +def budget (φ : CNF ℕ) : ℕ := + 80 * (SAT.incidenceGraph φ).1.length + 10 * (SAT.incidenceGraph φ).2.length + +/-- Unit paths in the order of the original literal occurrences. -/ +def paths (φ : CNF ℕ) : List Route := + let G := SAT.incidenceGraph φ + (G.orthogonalRoutes G.canonicalPorts).map (subdivideWithin (budget φ)) + +/-- The path of a particular original literal occurrence. -/ +def occurrencePath (φ : CNF ℕ) (o : Occurrence ℕ) : Route := + (paths φ).getD ((Cslib.Logic.PL.occurrences φ).idxOf o) [] + +/-- Actual occupied crossing candidates, excluding every declared graph vertex center. +First-occurrence selection ensures exactly one local gadget per selected square. -/ +def crossingSites (φ : CNF ℕ) : List Point := + let G := SAT.incidenceGraph φ + let occupied := (G.crossingCandidates G.canonicalPorts).filter fun p => + !(G.orthogonalPositions.contains p) && + decide (2 ≤ ((paths φ).filter fun r => r.contains p).length) + Cslib.Complexity.selectDistinct occupied (List.replicate occupied.length true) + +/-- The selected cells are exactly occupied nonvertex candidates. -/ +theorem mem_crossingSites (φ : CNF ℕ) (p : Point) : + p ∈ crossingSites φ ↔ + p ∈ (SAT.incidenceGraph φ).crossingCandidates (SAT.incidenceGraph φ).canonicalPorts ∧ + p ∉ (SAT.incidenceGraph φ).orthogonalPositions ∧ + 2 ≤ ((paths φ).filter fun r => r.contains p).length := by + simp [crossingSites, mem_selectDistinct_replicate, Bool.and_eq_true] + +/-- Every selected square receives exactly one template. -/ +theorem crossingSites_nodup (φ : CNF ℕ) : (crossingSites φ).Nodup := nodup_selectDistinct _ _ + +/-- Side facing a neighboring square, in left/right/bottom/top order. +Only unit neighbors are used by the correctness theorem. -/ +def side (p q : Point) : Fin 4 := + if q.1 < p.1 then 0 else if p.1 < q.1 then 1 else if q.2 < p.2 then 2 else 3 + +/-- The center of a square of side 240 indexed by an integer grid point. -/ +def center (p : Point) : Point := cellOrigin 120 p + (120, 120) + +end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathGeometry.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathGeometry.lean new file mode 100644 index 000000000..21e494e60 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathGeometry.lean @@ -0,0 +1,378 @@ +/- +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.Paths +public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy +public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree +import Complexity.Foundations.Data.List.Range +import Mathlib.Data.List.GetD +import Mathlib.Data.List.Nodup +import Mathlib.Data.List.Flatten +import Mathlib.Tactic.NormNum + +/-! +# Geometry of canonical incidence paths + +Shared unit-step, directed-port and midpoint uniqueness certificates support the paired +compiler without retaining the obsolete directed-output formula or its drawing. + +## Main results + +* `Cslib.Complexity.SAT.PlanarCompile.paths_shared_step_index`. +* `Cslib.Complexity.SAT.PlanarCompile.pathPorts_nodup`. +* `Cslib.Complexity.SAT.PlanarCompile.pathMidpoints_nodup`. +* `Cslib.Complexity.SAT.PlanarCompile.clause_cell_not_mem_crossingSites`. +* `Cslib.Complexity.SAT.PlanarCompile.clause_cell_not_mem_path_dropLast`. + +## References + +These are the shared canonical incidence-path constructions and certificates. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.PlanarCompile + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- Unit-adjacent integer cells differ by exactly one of the four cardinal displacements. -/ +theorem unit_neighbor_cases {p q : Point} (h : Orthogonal.length p q = 1) : + q = p + (-1, 0) ∨ q = p + (1, 0) ∨ q = p + (0, -1) ∨ q = p + (0, 1) := by + rcases p with ⟨px, py⟩ + rcases q with ⟨qx, qy⟩ + simp only [Orthogonal.length] at h + simp only [Prod.mk_add_mk, Prod.mk.injEq] + omega + +/-- Neighboring unit cells use exactly the same geometric midpoint for their shared port. -/ +theorem shared_cellPort {p q : Point} (h : Orthogonal.length p q = 1) : + cellPort 120 p (side p q) = cellPort 120 q (side q p) := by + rcases p with ⟨px, py⟩ + rcases unit_neighbor_cases h with rfl | rfl | rfl | rfl <;> + norm_num [side, cellPort, cellOrigin, Prod.ext_iff] <;> omega + +private theorem consecutivePair_index {r : Route} {a b : Point} + (h : (a, b) ∈ r.consecutivePairs) : + ∃ (k : ℕ) (hk : k + 1 < r.length), r[k] = a ∧ r[k + 1] = b := by + obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp h + have hk' : k + 1 < r.length := by + simpa only [List.consecutivePairs, List.length_zip, List.length_tail, + min_eq_right (Nat.sub_le _ _), Nat.lt_sub_iff_add_lt] using hk + simp only [List.consecutivePairs, List.getElem_zip, List.getElem_tail] at heq + exact ⟨k, hk', congrArg Prod.fst heq, congrArg Prod.snd heq⟩ + +private theorem mem_of_adjacent {r : Route} {p q : Point} + (h : (p, q) ∈ r.consecutivePairs ∨ (q, p) ∈ r.consecutivePairs) : p ∈ r := by + rcases h with h | h + · exact (List.of_mem_zip h).1 + · exact List.mem_of_mem_tail (List.of_mem_zip h).2 + +private theorem neighbor_of_straight {r : Route} {p q d : Point} + (ht : StraightThrough r p d) (hn : r.Nodup) + (h : (p, q) ∈ r.consecutivePairs ∨ (q, p) ∈ r.consecutivePairs) : + q = p - d ∨ q = p + d := by + rcases h with h | h + · obtain ⟨k, hk, hp, hq⟩ := consecutivePair_index h + have hh := ht.getD_neighbors hn (by omega) hp + have hd : r.getD (k + 1) p = q := by rw [List.getD_eq_getElem _ _ hk]; exact hq + rcases hh.2.2 with ⟨_, hnext⟩ | ⟨_, hnext⟩ + · exact Or.inr (hd.symm.trans hnext) + · exact Or.inl (hd.symm.trans hnext) + · obtain ⟨k, hk, hq, hp⟩ := consecutivePair_index h + have hh := ht.getD_neighbors hn hk hp + have hd : r.getD (k + 1 - 1) p = q := by + rw [Nat.add_sub_cancel, List.getD_eq_getElem _ _ (by omega)] + exact hq + rcases hh.2.2 with ⟨hprev, _⟩ | ⟨hprev, _⟩ + · exact Or.inl (hd.symm.trans hprev) + · exact Or.inr (hd.symm.trans hprev) + +private theorem horizontal_vertical_neighbors {p q : Point} + (hx : q = p - (1, 0) ∨ q = p + (1, 0)) + (hy : q = p - (0, 1) ∨ q = p + (0, 1)) : False := by + rcases hx with hx | hx <;> rcases hy with hy | hy <;> + have h := hx.symm.trans hy <;> + have h' := congrArg Prod.fst h <;> simp at h' + +private theorem canonical_neighbor_unique (G : Graph) + (hG : ∀ e ∈ G.2, e.1 ∈ G.1 ∧ e.2 ∈ G.1) + (hloop : ∀ e ∈ G.2, e.1 ≠ e.2) + (hdeg : ∀ v, G.incidenceVertices.count v ≤ 3) {i j : ℕ} + (hi : i < G.2.length) (hj : j < G.2.length) (hij : i ≠ j) {p q : Point} + (hcenter : p ∉ G.orthogonalPositions) + (hiadj : (p, q) ∈ (G.unitPath i).consecutivePairs ∨ + (q, p) ∈ (G.unitPath i).consecutivePairs) + (hjadj : (p, q) ∈ (G.unitPath j).consecutivePairs ∨ + (q, p) ∈ (G.unitPath j).consecutivePairs) : False := by + have hn := Graph.unitPath_nodup G hG hloop hi + have hm := Graph.unitPath_nodup G hG hloop hj + rcases Graph.unitPath_crossing_neighbors G hG hloop hdeg hi hj hij hcenter + (mem_of_adjacent hiadj) (mem_of_adjacent hjadj) with ⟨hx, hy⟩ | ⟨hy, hx⟩ + · exact horizontal_vertical_neighbors (neighbor_of_straight hx hn hiadj) + (neighbor_of_straight hy hm hjadj) + · exact horizontal_vertical_neighbors (neighbor_of_straight hx hm hjadj) + (neighbor_of_straight hy hn hiadj) + +private theorem unit_not_both_centers (G : Graph) {p q : Point} + (hunit : Orthogonal.length p q = 1) (hp : p ∈ G.orthogonalPositions) + (hq : q ∈ G.orthogonalPositions) : False := by + obtain ⟨i, _, rfl⟩ := List.mem_map.mp hp + obtain ⟨j, _, rfl⟩ := List.mem_map.mp hq + simp only [Orthogonal.length, Layout.center] at hunit + omega + +/-- Two actual canonical paths cannot share a unit grid edge, even in opposite directions. +This count-free uniqueness statement also applies to the final step into a clause cell. -/ +theorem paths_shared_step_index {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {i j : ℕ} (hi : i < (paths φ).length) (hj : j < (paths φ).length) {p q : Point} + (he : (p, q) ∈ ((paths φ).getD i []).consecutivePairs) + (hf : (p, q) ∈ ((paths φ).getD j []).consecutivePairs ∨ + (q, p) ∈ ((paths φ).getD j []).consecutivePairs) : i = j := by + by_contra hij + have hi' : i < (SAT.incidenceGraph φ).2.length := by + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi + have hj' : j < (SAT.incidenceGraph φ).2.length := by + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hj + change (p, q) ∈ ((SAT.incidenceGraph φ).unitPath i).consecutivePairs at he + change (p, q) ∈ ((SAT.incidenceGraph φ).unitPath j).consecutivePairs ∨ + (q, p) ∈ ((SAT.incidenceGraph φ).unitPath j).consecutivePairs at hf + have hG : ∀ e ∈ (SAT.incidenceGraph φ).2, + e.1 ∈ (SAT.incidenceGraph φ).1 ∧ e.2 ∈ (SAT.incidenceGraph φ).1 := + fun _ => SAT.incidenceGraph_endpoints + have hloop : ∀ e ∈ (SAT.incidenceGraph φ).2, e.1 ≠ e.2 := + fun _ => SAT.incidenceGraph_loopless + have hdeg := SAT.incidenceGraph_degree_le hw hv + by_cases hp : p ∈ (SAT.incidenceGraph φ).orthogonalPositions + · have hq : q ∉ (SAT.incidenceGraph φ).orthogonalPositions := fun hq => + unit_not_both_centers _ (Graph.unitPath_unit _ hG hloop hi' he) hp hq + exact canonical_neighbor_unique _ hG hloop hdeg hi' hj' hij hq (Or.inr he) hf.symm + · exact canonical_neighbor_unique _ hG hloop hdeg hi' hj' hij hp (Or.inl he) hf + +/-- At a unit neighbor, the facing side determines the neighbor itself. -/ +theorem side_injective_on_unit_neighbors {p q t : Point} + (hq : Orthogonal.length p q = 1) (ht : Orthogonal.length p t = 1) + (hside : side p q = side p t) : q = t := by + rcases p with ⟨px, py⟩ + rcases unit_neighbor_cases hq with rfl | rfl | rfl | rfl <;> + rcases unit_neighbor_cases ht with rfl | rfl | rfl | rfl <;> + first | rfl | norm_num [side] at hside + +private def stepPorts (e : Point × Point) : List (Point × Fin 4) := + [(e.1, side e.1 e.2), (e.2, side e.2 e.1)] + +private theorem unit_reverse {p q : Point} (h : Orthogonal.length p q = 1) : + Orthogonal.length q p = 1 := by + simp only [Orthogonal.length] at h ⊢ + omega + +private theorem stepPorts_inter {e f : Point × Point} {x : Point × Fin 4} + (he : Orthogonal.length e.1 e.2 = 1) (hf : Orthogonal.length f.1 f.2 = 1) + (hx : x ∈ stepPorts e) (hy : x ∈ stepPorts f) : + e = f ∨ e = (f.2, f.1) := by + rcases e with ⟨a, b⟩ + rcases f with ⟨c, d⟩ + simp only [stepPorts, List.mem_cons, List.not_mem_nil, or_false] at hx hy + rcases hx with rfl | rfl <;> rcases hy with hy | hy + · obtain ⟨h, hs⟩ := Prod.mk.inj hy + subst c + have hb := side_injective_on_unit_neighbors he hf hs + exact Or.inl (Prod.ext rfl hb) + · obtain ⟨h, hs⟩ := Prod.mk.inj hy + subst d + have hb := side_injective_on_unit_neighbors he (unit_reverse hf) hs + exact Or.inr (Prod.ext rfl hb) + · obtain ⟨h, hs⟩ := Prod.mk.inj hy + subst c + have ha := side_injective_on_unit_neighbors (unit_reverse he) hf hs + exact Or.inr (Prod.ext ha rfl) + · obtain ⟨h, hs⟩ := Prod.mk.inj hy + subst d + have ha := side_injective_on_unit_neighbors (unit_reverse he) (unit_reverse hf) hs + exact Or.inl (Prod.ext ha rfl) + +private theorem routePorts_nodup {r : Route} (hn : r.Nodup) + (hu : ∀ e ∈ r.consecutivePairs, Orthogonal.length e.1 e.2 = 1) : + (r.consecutivePairs.flatMap stepPorts).Nodup := by + apply List.nodup_flatMap.mpr + constructor + · intro e he + have hne := (axisAligned_of_length_eq_one (hu e he)).2 + simp only [stepPorts, List.nodup_cons, List.not_mem_nil, List.nodup_nil, + List.mem_singleton, not_false_eq_true, and_true] + exact fun h => hne (congrArg Prod.fst h) + · rw [List.pairwise_iff_getElem] + intro i j hi hj hij x hx hy + have hi' : i + 1 < r.length := by + simp only [List.consecutivePairs, List.length_zip, List.length_tail] at hi + omega + have hj' : j + 1 < r.length := by + simp only [List.consecutivePairs, List.length_zip, List.length_tail] at hj + omega + rcases stepPorts_inter (hu _ (List.getElem_mem hi)) (hu _ (List.getElem_mem hj)) hx hy + with heq | heq + · have heq' : r[i] = r[j] := by + simpa only [List.consecutivePairs, List.getElem_zip, List.getElem_tail] using + congrArg Prod.fst heq + have := hn.eq_of_getElem_eq (by omega) (by omega) heq' + omega + · have heq' : r[i] = r[j + 1] := by + simpa only [List.consecutivePairs, List.getElem_zip, List.getElem_tail] using + congrArg Prod.fst heq + have := hn.eq_of_getElem_eq (by omega) hj' heq' + omega + +/-- All directed cell ports in the actual canonical paths are distinct. Both halves of every +unit step are included, even the final clause-directed half. No path witness is assumed. -/ +theorem pathPorts_nodup {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + ((paths φ).flatMap fun r => r.consecutivePairs.flatMap fun e => + [(e.1, side e.1 e.2), (e.2, side e.2 e.1)]).Nodup := by + have hi_edge {i : ℕ} (hi : i < (paths φ).length) : + i < (SAT.incidenceGraph φ).2.length := by + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi + have hn {i : ℕ} (hi : i < (paths φ).length) : ((paths φ)[i]).Nodup := by + have h := Graph.unitPath_nodup (SAT.incidenceGraph φ) + (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) (hi_edge hi) + change ((paths φ).getD i []).Nodup at h + rwa [List.getD_eq_getElem _ _ hi] at h + have hu {i : ℕ} (hi : i < (paths φ).length) {e : Point × Point} + (he : e ∈ ((paths φ)[i]).consecutivePairs) : Orthogonal.length e.1 e.2 = 1 := by + apply Graph.unitPath_unit (SAT.incidenceGraph φ) + (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) (hi_edge hi) + change e ∈ ((paths φ).getD i []).consecutivePairs + rwa [List.getD_eq_getElem _ _ hi] + change ((paths φ).flatMap fun r => r.consecutivePairs.flatMap stepPorts).Nodup + apply List.nodup_flatMap.mpr + constructor + · intro r hr + obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr + exact routePorts_nodup (hn hi) (fun _ he => hu hi he) + · rw [List.pairwise_iff_getElem] + intro i j hi hj hij x hx hy + obtain ⟨e, he, hx⟩ := List.mem_flatMap.mp hx + obtain ⟨f, hf, hy⟩ := List.mem_flatMap.mp hy + have hi_step : e ∈ ((paths φ).getD i []).consecutivePairs := by + rwa [List.getD_eq_getElem _ _ hi] + have hj_step : (e.1, e.2) ∈ ((paths φ).getD j []).consecutivePairs ∨ + (e.2, e.1) ∈ ((paths φ).getD j []).consecutivePairs := by + rw [List.getD_eq_getElem _ _ hj] + rcases stepPorts_inter (hu hi he) (hu hj hf) hx hy with heq | heq + · exact Or.inl (heq.symm ▸ hf) + · exact Or.inr (by simpa only [heq] using hf) + have := paths_shared_step_index hw hv hi hj hi_step hj_step + omega + +/-- Equal boundary midpoints identify the same unordered unit grid edge. -/ +theorem cellPort_step_eq_cases {p q a b : Point} + (hpq : Orthogonal.length p q = 1) (hab : Orthogonal.length a b = 1) + (h : cellPort 120 p (side p q) = cellPort 120 a (side a b)) : + (p = a ∧ q = b) ∨ (p = b ∧ q = a) := by + rcases p with ⟨px, py⟩ + rcases a with ⟨ax, ay⟩ + rcases unit_neighbor_cases hpq with rfl | rfl | rfl | rfl <;> + rcases unit_neighbor_cases hab with rfl | rfl | rfl | rfl <;> + norm_num [side, cellPort, cellOrigin, Prod.ext_iff] at h ⊢ <;> omega + +/-- One geometric midpoint per actual unit step gives a duplicate-free list. +This includes final steps, so any prefix selection used for binary clauses remains distinct. -/ +theorem pathMidpoints_nodup {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + ((paths φ).flatMap fun r => r.consecutivePairs.map fun e => + cellPort 120 e.1 (side e.1 e.2)).Nodup := by + let steps := (paths φ).flatMap List.consecutivePairs + have hu {e : Point × Point} (he : e ∈ steps) : Orthogonal.length e.1 e.2 = 1 := by + obtain ⟨r, hr, he⟩ := List.mem_flatMap.mp he + obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr + have hi' : i < (SAT.incidenceGraph φ).2.length := by + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi + apply Graph.unitPath_unit (SAT.incidenceGraph φ) + (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) hi' + change e ∈ ((paths φ).getD i []).consecutivePairs + rwa [List.getD_eq_getElem _ _ hi] + have hp : (steps.flatMap stepPorts).Nodup := by + have h := pathPorts_nodup hw hv + change ((paths φ).flatMap fun r => r.consecutivePairs.flatMap stepPorts).Nodup at h + simpa only [steps, List.flatMap_assoc] using h + have hpair := (List.nodup_flatMap.mp hp).2 + have hmid : (steps.map fun e => cellPort 120 e.1 (side e.1 e.2)).Nodup := by + apply List.pairwise_map.mpr + apply hpair.imp_of_mem + intro e f he hf hd heq + have hx : (e.1, side e.1 e.2) ∈ stepPorts e := by simp [stepPorts] + rcases cellPort_step_eq_cases (hu he) (hu hf) heq with ⟨h₁, h₂⟩ | ⟨h₁, h₂⟩ + · have heq' : e = f := Prod.ext h₁ h₂ + exact hd hx (heq' ▸ hx) + · have heq' : e = (f.2, f.1) := Prod.ext h₁ h₂ + exact hd hx (by simp [stepPorts, heq']) + simpa only [steps, List.map_flatMap] using hmid + +/-- Distinct integer cells have distinct displayed centers. -/ +theorem center_injective : Function.Injective center := by + intro p q h + have hp := center_mem_openCell (r := 120) (by decide) p + have hq := center_mem_openCell (r := 120) (by decide) q + change realPoint (center p) ∈ openCell 120 p at hp + change realPoint (center q) ∈ openCell 120 q at hq + rw [← h] at hq + exact cell_eq_of_mem_open_closed (by decide) hp + ⟨hq.1.le, hq.2.1.le, hq.2.2.1.le, hq.2.2.2.le⟩ + +/-- Original clause cells are declared source centers and are never selected as crossings. -/ +theorem clause_cell_not_mem_crossingSites (φ : CNF ℕ) {i : ℕ} (hi : i < φ.length) : + Layout.center (φ.distinctVars.length + i) ∉ crossingSites φ := by + intro h + apply ((mem_crossingSites φ _).mp h).2.1 + refine List.mem_map.mpr ⟨φ.distinctVars.length + i, List.mem_range.mpr ?_, rfl⟩ + simp only [SAT.incidenceGraph, List.length_range] + omega + +private theorem occurrencePath_clause_center_iff {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) {i : ℕ} (hi : i < φ.length) : + Layout.center (φ.distinctVars.length + i) ∈ occurrencePath φ o ↔ i = o.1 := by + have hoidx := occurrence_index_lt ho + have h := Graph.unitPath_center_iff (SAT.incidenceGraph φ) + (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) hoidx + (w := φ.distinctVars.length + i) (by simp only [SAT.incidenceGraph, List.length_range]; omega) + have he : (SAT.incidenceGraph φ).2[(Cslib.Logic.PL.occurrences φ).idxOf o] = + (φ.distinctVars.idxOf o.2.2.1, φ.distinctVars.length + o.1) := by + simp only [SAT.incidenceGraph, List.getElem_map] + rw [List.getElem_idxOf (List.idxOf_lt_length_of_mem ho)] + have hb := SAT.incidenceGraph_bipartite (List.getElem_mem hoidx) + rw [he] at hb h + change Layout.center (φ.distinctVars.length + i) ∈ occurrencePath φ o ↔ + φ.distinctVars.length + i = (List.range _).idxOf (φ.distinctVars.idxOf o.2.2.1) ∨ + φ.distinctVars.length + i = (List.range _).idxOf (φ.distinctVars.length + o.1) at h + rw [List.idxOf_range_of_lt (by omega), List.idxOf_range_of_lt hb.2.2] at h + exact h.trans (by omega) + +/-- No source clause center is used as a signal cell before a path's final endpoint. -/ +theorem clause_cell_not_mem_path_dropLast {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) {i : ℕ} (hi : i < φ.length) : + Layout.center (φ.distinctVars.length + i) ∉ (occurrencePath φ o).dropLast := by + intro hp + have hi' := (occurrencePath_clause_center_iff ho hi).mp + ((List.dropLast_sublist _).subset hp) + subst i + obtain ⟨k, hk, hget⟩ := List.mem_iff_getElem.mp hp + have hlen := occurrencePath_length_ge_two ho + have hend := (occurrencePath_endpoints ho).2 + rw [List.getLast?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hend + have hk' : k < (occurrencePath φ o).length := by + simp only [List.length_dropLast] at hk + omega + have heq : (occurrencePath φ o)[k] = + (occurrencePath φ o)[(occurrencePath φ o).length - 1] := by + rw [Option.some.inj hend] + simpa only [List.getElem_dropLast] using hget + have hidx := (occurrencePath_nodup ho).eq_of_getElem_eq hk' (by omega) heq + simp only [List.length_dropLast] at hk + omega + +end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PathPolyTime.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathPolyTime.lean new file mode 100644 index 000000000..7cc118ccd --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PathPolyTime.lean @@ -0,0 +1,324 @@ +/- +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.PathData +public import Complexity.Computability.Complexity.Problems.SAT +public import Complexity.Computability.Geometry.Orthogonal.Subdivision +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Finite +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option +public import Complexity.Logics.Propositional.CNF.PolyTime +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.Nat.Fin +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + + +/-! +# Native computation of canonical path data + +Input natural labels and coordinates use binary encodings; syntactic positions and the +subdivision budget use unary counters. These certificates compute only the shared paths, +crossing cells, and occurrence lookup, with no geometric validity assumption. + +## Main results + +* `Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_budget`. +* `Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_paths`. +* `Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_crossingSites`. +* `Cslib.Complexity.SAT.PlanarCompile.computableInPolyTime_occurrencePath`. + +## References + +These are the shared canonical incidence-path constructions and certificates. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.PlanarCompile + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal +open Turing.MultiTapeTM + +private theorem computable_natCast : + ComputableInPolyTime (fun n : ℕ => (n : ℤ)) encUnary encIntBin := + .of_tidy (ComputableTidilyInPolyTime.intBin_natCast.comp + ComputableTidilyInPolyTime.unary_to_binary) + +private theorem computable_finVal : + ComputableInPolyTime (fun s : Fin 3 => s.val) (encFinite (Fin 3)) encNat := + .of_tidy (ComputableTidilyInPolyTime.of_finite _) + +attribute [local fun_prop] computable_natCast computable_finVal ComputableInPolyTime.tidy + +private theorem computable_incidencePort : + ComputableInPolyTime (fun p : Graph × ℕ => p.1.incidencePort p.2) + (encPair encGraph encUnary) (encFinite (Fin 3)) := by + have hc : ComputableTidilyInPolyTime (fun p : Graph × ℕ => + (p.1.incidenceVertices.take p.2).count (p.1.incidenceVertices.getD p.2 0)) + (encPair encGraph encUnary) encUnary := by + unfold Graph.incidenceVertices encGraph + fun_prop + exact .of_tidy ((ComputableTidilyInPolyTime.unary_finMod (by decide) + (encFinite (Fin 3))).comp hc) + +attribute [local fun_prop] computable_incidencePort + +private theorem computable_canonicalPorts : + ComputableInPolyTime Graph.canonicalPorts encGraph + (encList (encPair (encFinite (Fin 3)) (encFinite (Fin 3)))) := by + refine .of_tidy ?_ + unfold Graph.canonicalPorts encGraph + fun_prop + +attribute [local fun_prop] computable_canonicalPorts + +private theorem computable_layoutCenter : + ComputableInPolyTime Layout.center encUnary encPoint := by + refine .of_tidy ?_ + unfold Layout.center encPoint + fun_prop + +private theorem computable_layoutColumn : + ComputableInPolyTime (fun p : ℕ × Fin 3 => Layout.column p.1 p.2) + (encPair encUnary (encFinite (Fin 3))) encIntBin := by + refine .of_tidy ?_ + unfold Layout.column + fun_prop + +private theorem computable_layoutTrack : + ComputableInPolyTime (fun p : ℕ × ℕ => Layout.track p.1 p.2) + (encPair encUnary encUnary) encIntBin := by + refine .of_tidy ?_ + unfold Layout.track + fun_prop + +attribute [local fun_prop] computable_layoutCenter computable_layoutColumn computable_layoutTrack + +private theorem computable_layoutElbow : + ComputableInPolyTime (fun p : ℕ × Fin 3 => Layout.elbow p.1 p.2) + (encPair encUnary (encFinite (Fin 3))) encPoint := by + refine .of_tidy ?_ + unfold Layout.elbow encPoint + fun_prop + +attribute [local fun_prop] computable_layoutElbow + +private theorem computable_layoutRoute : + ComputableInPolyTime (fun p : ℕ × ℕ × ℕ × ℕ × Fin 3 × Fin 3 => + Layout.route p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2.1 p.2.2.2.2.2) + (encPair encUnary (encPair encUnary (encPair encUnary + (encPair encUnary (encPair (encFinite (Fin 3)) (encFinite (Fin 3))))))) encRoute := by + refine .of_tidy ?_ + unfold Layout.route encRoute + fun_prop + +attribute [local fun_prop] computable_layoutRoute + +private theorem computable_orthogonalRoutes : + ComputableInPolyTime (fun G : Graph => G.orthogonalRoutes G.canonicalPorts) + encGraph (encList encRoute) := by + let edgeEncoding := encPair (encPair encNat encNat) encUnary + let routeInput := encPair encUnary (encPair encUnary (encPair encUnary + (encPair encUnary (encPair (encFinite (Fin 3)) (encFinite (Fin 3)))))) + have hcan := computable_canonicalPorts.tidy + have hp : ComputableTidilyInPolyTime (fun p : Graph × ((ℕ × ℕ) × ℕ) => + p.1.canonicalPorts.getD p.2.2 (0, 0)) + (encPair encGraph edgeEncoding) (encPair (encFinite (Fin 3)) (encFinite (Fin 3))) := by + unfold edgeEncoding encGraph + fun_prop + have hargs : ComputableInPolyTime (fun p : Graph × ((ℕ × ℕ) × ℕ) => + (p.1.1.length, p.2.2, p.1.1.idxOf p.2.1.1, p.1.1.idxOf p.2.1.2, + (p.1.canonicalPorts.getD p.2.2 (0, 0)).1, + (p.1.canonicalPorts.getD p.2.2 (0, 0)).2)) + (encPair encGraph edgeEncoding) routeInput := by + refine .of_tidy ?_ + unfold routeInput edgeEncoding encGraph at * + fun_prop + have hbody := computable_layoutRoute.comp hargs + have hlist : ComputableInPolyTime (fun G : Graph => G.2.zipIdx) encGraph + (encList edgeEncoding) := by + refine .of_tidy ?_ + unfold encGraph edgeEncoding + fun_prop + simpa only [Graph.orthogonalRoutes, Function.comp_def] using + ComputableInPolyTime.mapWithInput hlist hbody + +attribute [local fun_prop] computable_orthogonalRoutes + +/-- The budget is a linear expression in syntactic list lengths, computed as a unary counter. -/ +@[fun_prop] +theorem computableInPolyTime_budget : ComputableInPolyTime budget encCNF encUnary := by + refine .of_tidy ?_ + unfold budget encCNF + fun_prop + +/-- Canonical incidence routes have a native polynomial-time bounded unit expansion. +The input labels and output coordinates are binary; only the step budget is unary. -/ +@[fun_prop] +theorem computableInPolyTime_paths : + ComputableInPolyTime paths encCNF (encList encRoute) := by + change ComputableInPolyTime (fun φ => + ((SAT.incidenceGraph φ).orthogonalRoutes (SAT.incidenceGraph φ).canonicalPorts).map + (subdivideWithin (budget φ))) encCNF (encList encRoute) + have hraw := computable_orthogonalRoutes.comp (SAT.computableInPolyTime_incidenceGraph encNat) + have hargs : ComputableInPolyTime (fun p : CNF ℕ × Route => (budget p.1, p.2)) + (encPair encCNF encRoute) (encPair encUnary encRoute) := by fun_prop + have hsub := computableInPolyTime_subdivideWithin.comp hargs + simpa only [Function.comp_def, encCNF] using ComputableInPolyTime.mapWithInput hraw hsub + +private def endpointColumns (p : Graph × ℕ) : Point := + (Layout.column (p.1.1.idxOf (p.1.edgeEndpoint p.2 false)) + (Graph.portAt p.1.canonicalPorts p.2 false), + Layout.column (p.1.1.idxOf (p.1.edgeEndpoint p.2 true)) + (Graph.portAt p.1.canonicalPorts p.2 true)) + +private theorem computable_endpointColumns : + ComputableInPolyTime endpointColumns (encPair encGraph encUnary) encPoint := by + unfold endpointColumns + have hcan := computable_canonicalPorts.tidy + have hp : ComputableTidilyInPolyTime (fun p : Graph × ℕ => + p.1.canonicalPorts.getD p.2 (0, 0)) + (encPair encGraph encUnary) (encPair (encFinite (Fin 3)) (encFinite (Fin 3))) := by + unfold encGraph + fun_prop + have he : ComputableTidilyInPolyTime (fun p : Graph × ℕ => p.1.2.getD p.2 (0, 0)) + (encPair encGraph encUnary) (encPair encNat encNat) := by + unfold encGraph + fun_prop + refine .of_tidy ?_ + unfold Graph.edgeEndpoint Graph.portAt encPoint encGraph at * + simp only [Bool.false_eq_true, ↓reduceIte] + fun_prop + +attribute [local fun_prop] computable_endpointColumns + +private def candidatePair (p : Graph × (ℕ × ℕ)) : List Point := + [((endpointColumns (p.1, p.2.2)).1, Layout.track p.1.1.length p.2.1), + ((endpointColumns (p.1, p.2.2)).2, Layout.track p.1.1.length p.2.1)] + +private theorem computable_candidatePair : + ComputableInPolyTime candidatePair (encPair encGraph (encPair encUnary encUnary)) + (encList encPoint) := by + have hselect : ComputableTidilyInPolyTime + (fun p : Graph × (ℕ × ℕ) => (p.1, p.2.2)) + (encPair encGraph (encPair encUnary encUnary)) (encPair encGraph encUnary) := by fun_prop + have hcols := computable_endpointColumns.tidy.comp hselect + have hleft := hcols.fst' + have hright := hcols.snd' + have htrack : ComputableTidilyInPolyTime (fun p : Graph × (ℕ × ℕ) => + Layout.track p.1.1.length p.2.1) + (encPair encGraph (encPair encUnary encUnary)) encIntBin := by + unfold encGraph + fun_prop + refine .of_tidy ?_ + unfold candidatePair encPoint at * + fun_prop + +private def candidateRow (p : Graph × ℕ) : List Point := + (List.range p.1.2.length).flatMap fun j => candidatePair (p.1, p.2, j) + +private theorem computable_edgeRange : + ComputableInPolyTime (fun G : Graph => List.range G.2.length) encGraph + (encList encUnary) := by + refine .of_tidy ?_ + unfold encGraph + fun_prop + +private theorem computable_candidateRow : + ComputableInPolyTime candidateRow (encPair encGraph encUnary) (encList encPoint) := by + have hlist := computable_edgeRange.comp (ComputableInPolyTime.fst encGraph encUnary) + have harg : ComputableInPolyTime (fun p : (Graph × ℕ) × ℕ => (p.1.1, p.1.2, p.2)) + (encPair (encPair encGraph encUnary) encUnary) + (encPair encGraph (encPair encUnary encUnary)) := by fun_prop + have hbody := computable_candidatePair.comp harg + change ComputableInPolyTime (fun p : Graph × ℕ => + (List.range p.1.2.length).flatMap fun j => candidatePair (p.1, p.2, j)) _ _ + simpa only [Function.comp_def] using ComputableInPolyTime.flatMapWithInput hlist hbody + +private theorem computable_crossingCandidates : + ComputableInPolyTime (fun G : Graph => G.crossingCandidates G.canonicalPorts) + encGraph (encList encPoint) := by + have h := ComputableInPolyTime.flatMapWithInput + (f := fun G i => candidateRow (G, i)) (encB := encPoint) + computable_edgeRange computable_candidateRow + simpa only [candidateRow, candidatePair, endpointColumns, Graph.crossingCandidates] using h + +attribute [local fun_prop] computable_crossingCandidates + +private theorem computable_orthogonalPositions : + ComputableInPolyTime Graph.orthogonalPositions encGraph encRoute := by + refine .of_tidy ?_ + unfold Graph.orthogonalPositions encRoute encGraph + fun_prop + +attribute [local fun_prop] computable_orthogonalPositions + +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 + +private theorem computable_crossingPredicate : + ComputableInPolyTime (fun p : CNF ℕ × Point => + !((SAT.incidenceGraph p.1).orthogonalPositions.contains p.2) && + decide (2 ≤ ((paths p.1).filter fun r => r.contains p.2).length)) + (encPair encCNF encPoint) encBool := by + have hg := SAT.computableInPolyTime_incidenceGraph encNat + have hv : ComputableTidilyInPolyTime (fun p : CNF ℕ × Point => + (SAT.incidenceGraph p.1).orthogonalPositions) (encPair encCNF encPoint) encRoute := + (computable_orthogonalPositions.comp hg).tidy.comp (ComputableTidilyInPolyTime.fst _ _) + have hp : ComputableTidilyInPolyTime (fun p : CNF ℕ × Point => paths p.1) + (encPair encCNF encPoint) (encList encRoute) := + computableInPolyTime_paths.tidy.comp (ComputableTidilyInPolyTime.fst _ _) + refine .of_tidy ?_ + unfold encRoute at * + simp only [List.contains_eq_mem] + fun_prop + +/-- Occupied nonvertex crossing sites can be selected in native polynomial time. -/ +@[fun_prop] +theorem computableInPolyTime_crossingSites : + ComputableInPolyTime crossingSites encCNF encRoute := by + have hc := computable_crossingCandidates.comp (SAT.computableInPolyTime_incidenceGraph encNat) + have hf := ComputableInPolyTime.filterWithInput + (test := fun φ p => !((SAT.incidenceGraph φ).orthogonalPositions.contains p) && + decide (2 ≤ ((paths φ).filter fun r => r.contains p).length)) + hc computable_crossingPredicate + have h := computable_distinctPoints.comp hf + change ComputableInPolyTime (fun φ => + selectDistinct + (((SAT.incidenceGraph φ).crossingCandidates (SAT.incidenceGraph φ).canonicalPorts).filter + fun p => !((SAT.incidenceGraph φ).orthogonalPositions.contains p) && + decide (2 ≤ ((paths φ).filter fun r => r.contains p).length)) + (List.replicate + ((((SAT.incidenceGraph φ).crossingCandidates (SAT.incidenceGraph φ).canonicalPorts).filter + fun p => !((SAT.incidenceGraph φ).orthogonalPositions.contains p) && + decide (2 ≤ ((paths φ).filter fun r => r.contains p).length)).length) true)) _ _ + simpa only [Function.comp_def, encCNF] using h + +/-- Looking up the path for a syntactic literal occurrence is native polynomial-time. -/ +@[fun_prop] +theorem computableInPolyTime_occurrencePath : + ComputableInPolyTime (fun p : CNF ℕ × Occurrence ℕ => occurrencePath p.1 p.2) + (encPair encCNF (Cslib.Logic.PL.encOccurrence encNat)) encRoute := by + have hp := computableInPolyTime_paths.tidy + have ho := (Cslib.Logic.PL.computableInPolyTime_occurrences encNat).tidy + refine .of_tidy ?_ + unfold occurrencePath encCNF Cslib.Logic.PL.encOccurrence at * + fun_prop + +end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean index aa7f50a04..6e63918ec 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths.lean @@ -7,9 +7,10 @@ Authors: Erik Demaine module -- upstream: candidate -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalPath public import Complexity.Logics.Propositional.CNF.Occurrence +import Complexity.Foundations.Data.List.Range import Mathlib.Data.List.GetD /-! @@ -80,12 +81,6 @@ theorem occurrencePath_ne_nil {φ : CNF ℕ} {o : Occurrence ℕ} exact Graph.unitPath_ne_nil _ (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) (occurrence_index_lt ho) -private theorem idxOf_range_eq {i n : ℕ} (hi : i < n) : (List.range n).idxOf i = i := by - have h := (List.nodup_range : (List.range n).Nodup).idxOf_getElem i - (by simpa only [List.length_range] using hi) - rw [List.getElem_range] at h - exact h - /-- Actual occurrence paths start at the variable's source-grid center and end at their clause. -/ theorem occurrencePath_endpoints {φ : CNF ℕ} {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) : @@ -106,7 +101,7 @@ theorem occurrencePath_endpoints {φ : CNF ℕ} {o : Occurrence ℕ} some (Layout.center ((List.range _).idxOf (φ.distinctVars.idxOf o.2.2.1))) ∧ (occurrencePath φ o).getLast? = some (Layout.center ((List.range _).idxOf (φ.distinctVars.length + o.1))) at h - rw [idxOf_range_eq (by omega), idxOf_range_eq hb.2.2] at h + rw [List.idxOf_range_of_lt (by omega), List.idxOf_range_of_lt hb.2.2] at h exact h /-- Actual literal paths contain at least one unit step, so final-literal lookups are in range. -/ diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean index a3b374d48..70a78c5a8 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalPath public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree +import Complexity.Foundations.Data.List.Filter import Mathlib.Data.List.GetD /-! @@ -34,37 +35,6 @@ namespace Cslib.Complexity.SAT.PlanarCompile open Cslib.Logic.PL Orthogonal -private theorem canonical_paths (φ : CNF ℕ) : - paths φ = (SAT.incidenceGraph φ).unitPaths := rfl - -private theorem two_paths_of_filter_length (rs : List Route) (p : Point) - (hlen : 2 ≤ (rs.filter fun r => r.contains p).length) : - ∃ (i j : ℕ) (hi : i < rs.length) (hj : j < rs.length), - i ≠ j ∧ p ∈ rs[i] ∧ p ∈ rs[j] := by - induction rs with - | nil => simp at hlen - | cons r rs ih => - by_cases hp : p ∈ r - · have hne : (rs.filter fun r => r.contains p) ≠ [] := by - intro h - have hf : ((r :: rs).filter fun r => r.contains p) = [r] := by - have hpred : r.contains p = true := by simpa using hp - simp only [List.filter_cons, hpred, ↓reduceIte, h] - rw [hf] at hlen - simp at hlen - cases hf : rs.filter (fun r => r.contains p) with - | nil => exact False.elim (hne hf) - | cons t ts => - have ht : t ∈ rs.filter (fun r => r.contains p) := by rw [hf]; simp - obtain ⟨htmem, htp⟩ := List.mem_filter.mp ht - obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp htmem - exact ⟨0, j + 1, by simp, by simpa using hj, by omega, hp, by simpa using htp⟩ - · have hf : ((r :: rs).filter fun r => r.contains p) = rs.filter (fun r => r.contains p) := by - simp [hp] - rw [hf] at hlen - obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := ih hlen - exact ⟨i + 1, j + 1, by simpa using hi, by simpa using hj, by omega, hpi, hpj⟩ - /-- Away from source centers, an unselected ordinary cell belongs to at most one path. -/ theorem paths_filter_length_le_one {φ : CNF ℕ} (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) {p : Point} @@ -72,11 +42,12 @@ theorem paths_filter_length_le_one {φ : CNF ℕ} ((paths φ).filter fun r => r.contains p).length ≤ 1 := by by_contra h have ht : 2 ≤ ((paths φ).filter fun r => r.contains p).length := by omega - obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := two_paths_of_filter_length (paths φ) p ht + obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := + List.exists_pair_indices_of_two_le_filter_contains (paths φ) p ht have hi' : i < (SAT.incidenceGraph φ).2.length := by - simpa only [canonical_paths, Graph.unitPaths_length] using hi + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi have hj' : j < (SAT.incidenceGraph φ).2.length := by - simpa only [canonical_paths, Graph.unitPaths_length] using hj + simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hj have hpi' : p ∈ (SAT.incidenceGraph φ).unitPath i := by change p ∈ (paths φ).getD i [] rwa [List.getD_eq_getElem _ _ hi] diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean index 693e90cee..48178aa3a 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathPolyTime public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile public import Complexity.Computability.Complexity.Problems.SAT public import Complexity.Computability.Geometry.Orthogonal.Subdivision @@ -166,27 +167,6 @@ private theorem computable_orthogonalRoutes : attribute [local fun_prop] computable_orthogonalRoutes -/-- The budget is a linear expression in syntactic list lengths, computed as a unary counter. -/ -@[fun_prop] -theorem computableInPolyTime_budget : ComputableInPolyTime budget encCNF encUnary := by - refine .of_tidy ?_ - unfold budget encCNF - fun_prop - -/-- Canonical incidence routes have a native polynomial-time bounded unit expansion. -The input labels and output coordinates are binary; only the step budget is unary. -/ -@[fun_prop] -theorem computableInPolyTime_paths : - ComputableInPolyTime paths encCNF (encList encRoute) := by - change ComputableInPolyTime (fun φ => - ((SAT.incidenceGraph φ).orthogonalRoutes (SAT.incidenceGraph φ).canonicalPorts).map - (subdivideWithin (budget φ))) encCNF (encList encRoute) - have hraw := computable_orthogonalRoutes.comp (SAT.computableInPolyTime_incidenceGraph encNat) - have hargs : ComputableInPolyTime (fun p : CNF ℕ × Route => (budget p.1, p.2)) - (encPair encCNF encRoute) (encPair encUnary encRoute) := by fun_prop - have hsub := computableInPolyTime_subdivideWithin.comp hargs - simpa only [Function.comp_def, encCNF] using ComputableInPolyTime.mapWithInput hraw hsub - private def endpointColumns (p : Graph × ℕ) : Point := (Layout.column (p.1.1.idxOf (p.1.edgeEndpoint p.2 false)) (Graph.portAt p.1.canonicalPorts p.2 false), @@ -300,38 +280,6 @@ private theorem computable_crossingPredicate : simp only [List.contains_eq_mem] fun_prop -/-- Occupied nonvertex crossing sites can be selected in native polynomial time. -/ -@[fun_prop] -theorem computableInPolyTime_crossingSites : - ComputableInPolyTime crossingSites encCNF encRoute := by - have hc := computable_crossingCandidates.comp (SAT.computableInPolyTime_incidenceGraph encNat) - have hf := ComputableInPolyTime.filterWithInput - (test := fun φ p => !((SAT.incidenceGraph φ).orthogonalPositions.contains p) && - decide (2 ≤ ((paths φ).filter fun r => r.contains p).length)) - hc computable_crossingPredicate - have h := computable_distinctPoints.comp hf - change ComputableInPolyTime (fun φ => - selectDistinct - (((SAT.incidenceGraph φ).crossingCandidates (SAT.incidenceGraph φ).canonicalPorts).filter - fun p => !((SAT.incidenceGraph φ).orthogonalPositions.contains p) && - decide (2 ≤ ((paths φ).filter fun r => r.contains p).length)) - (List.replicate - ((((SAT.incidenceGraph φ).crossingCandidates (SAT.incidenceGraph φ).canonicalPorts).filter - fun p => !((SAT.incidenceGraph φ).orthogonalPositions.contains p) && - decide (2 ≤ ((paths φ).filter fun r => r.contains p).length)).length) true)) _ _ - simpa only [Function.comp_def, encCNF] using h - -/-- Looking up the path for a syntactic literal occurrence is native polynomial-time. -/ -@[fun_prop] -theorem computableInPolyTime_occurrencePath : - ComputableInPolyTime (fun p : CNF ℕ × Occurrence ℕ => occurrencePath p.1 p.2) - (encPair encCNF (Cslib.Logic.PL.encOccurrence encNat)) encRoute := by - have hp := computableInPolyTime_paths.tidy - have ho := (Cslib.Logic.PL.computableInPolyTime_occurrences encNat).tidy - refine .of_tidy ?_ - unfold occurrencePath encCNF Cslib.Logic.PL.encOccurrence at * - fun_prop - private theorem computable_side : ComputableInPolyTime (fun p : Point × Point => side p.1 p.2) (encPair encPoint encPoint) (encFinite (Fin 4)) := by diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean index c4ff97a2f..30f5ee086 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile public import Complexity.Logics.Propositional.CNF.Planar.DirectedWire import Mathlib.Data.List.GetD @@ -39,17 +40,6 @@ namespace Cslib.Complexity.SAT.PlanarCompile open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal -/-- A path contributes one signal cell for each point before its final clause vertex. -/ -theorem length_wire (sites : List Point) (r : Route) : - (wire sites r).length = r.length - 1 := by simp [wire] - -/-- Every path of at least two points yields a nonempty cell wire. -/ -theorem wire_ne_nil (sites : List Point) (r : Route) (h : 2 ≤ r.length) : wire sites r ≠ [] := by - intro he - have hl := length_wire sites r - rw [he, List.length_nil] at hl - omega - /-- Forgetting geometric data gives exactly the renamed fixed crossover clauses. -/ theorem map_fst_crossingClauses (p : Point) : (crossingClauses p).map Prod.fst = @@ -91,13 +81,6 @@ theorem crossing_boundary_eq {φ : CNF ℕ} {σ : Variable → Bool} σ (p, some .bTop) = σ (p, some .bBottom) := Crossover.split_boundary_eq_of_holds (((eval_rawFormula_iff φ σ).1 h).2.1 p hp) -/-- Exact indexed cell signals in the executable wire list. -/ -theorem getElem_wire (sites : List Point) (r : Route) (i : ℕ) (hi : i < r.length - 1) : - (wire sites r)[i]'(by simpa [wire] using hi) = - (signal sites r[i] (r.getD (i - 1) r[i]), - signal sites r[i] (r.getD (i + 1) r[i])) := by - simp only [wire, List.getElem_map, List.getElem_zipIdx, Nat.zero_add, List.getElem_dropLast] - /-- The placed intercell clauses are exactly the generic polarity-directed wire clauses. -/ theorem map_fst_links (sites : List Point) (b : Bool) (r : Route) : (links sites b r).map Prod.fst = CNF.DirectedWire.links b (wire sites r) := by diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean index 592978fe7..078a60735 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean @@ -7,6 +7,7 @@ Authors: Erik Demaine module -- upstream: candidate +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile import Mathlib.Algebra.BigOperators.Ring.List import Mathlib.Data.List.GetD @@ -40,19 +41,6 @@ namespace Cslib.Complexity.SAT.PlanarCompile open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal -/-- Number of external implication clauses actually emitted by the compiler. -/ -def linkCount (φ : CNF ℕ) : ℕ := - ((Cslib.Logic.PL.occurrences φ).map fun o => (occurrencePath φ o).length - 2).sum - -/-- Selected crossing sites form a sublist of the quadratic canonical cover after deduplication. -The bound counts all source literal incidences, including repetitions. -/ -theorem crossingSites_length_le (φ : CNF ℕ) : - (crossingSites φ).length ≤ 2 * φ.vars.length ^ 2 := by - unfold crossingSites - rw [length_selectDistinct_replicate] - exact (List.toFinset_card_le _).trans ((List.length_filter_le _ _).trans (by - simp [Graph.crossingCandidates_length, SAT.length_edges_incidenceGraph])) - /-- Original clauses keep their count. -/ theorem length_originalClauses (φ : CNF ℕ) (sites : List Point) : (originalClauses φ sites).length = φ.length := by simp [originalClauses] @@ -126,40 +114,6 @@ theorem width_formula {φ : CNF ℕ} (h : ∀ c ∈ φ, c.length ≤ 3) : rw [← he] exact width_rawFormula h d hd -/-- There is one unit path per original literal incidence. -/ -theorem paths_length (φ : CNF ℕ) : (paths φ).length = φ.vars.length := by - simp [paths, SAT.length_edges_incidenceGraph] - -/-- The bounded enumerator emits at most five segment budgets plus the final endpoint. -This unconditional bound also applies to inputs that fail the degree-three restriction. -/ -theorem path_length_le {φ : CNF ℕ} {r : Route} (hr : r ∈ paths φ) : - r.length ≤ 5 * budget φ + 1 := by - change r ∈ ((SAT.incidenceGraph φ).orthogonalRoutes - (SAT.incidenceGraph φ).canonicalPorts).map (subdivideWithin (budget φ)) at hr - obtain ⟨base, hbase, rfl⟩ := List.mem_map.mp hr - have hs : base.consecutivePairs.length = 5 := by - obtain ⟨⟨e, i⟩, _, rfl⟩ := List.mem_map.mp hbase - rfl - simpa only [hs, Nat.mul_comm] using subdivideWithin_length_le (budget φ) base - -/-- Indexed access to a path obeys the same bound, including the empty fallback. -/ -theorem occurrencePath_length_le (φ : CNF ℕ) (o : Occurrence ℕ) : - (occurrencePath φ o).length ≤ 5 * budget φ + 1 := by - unfold occurrencePath - by_cases h : (Cslib.Logic.PL.occurrences φ).idxOf o < (paths φ).length - · rw [List.getD_eq_getElem _ _ h] - exact path_length_le (List.getElem_mem h) - · rw [List.getD_eq_default _ _ (Nat.le_of_not_gt h)] - exact Nat.zero_le _ - -/-- There are quadratically many links, even before checking the source restrictions. -/ -theorem linkCount_le (φ : CNF ℕ) : - linkCount φ ≤ φ.vars.length * (5 * budget φ + 1) := by - calc - _ ≤ ((Cslib.Logic.PL.occurrences φ).map fun _ => 5 * budget φ + 1).sum := - List.sum_le_sum fun o _ => (Nat.sub_le _ _).trans (occurrencePath_length_le φ o) - _ = _ := by simp [Cslib.Logic.PL.length_occurrences, Nat.mul_comm] - /-- An explicit quadratic clause bound in the source incidence graph's combinatorial size. -/ theorem length_formula_le (φ : CNF ℕ) : (formula φ).length ≤ 600 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by