diff --git a/Complexity.lean b/Complexity.lean index 25efc8cb80..56d0bd1da2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -812,9 +812,13 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverL public import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry public import Complexity.Computability.Complexity.Problems.SAT.Planar.Occurrence public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRing +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCorrectness +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCounting public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayout public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutChecks public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutData +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedSemantics public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean new file mode 100644 index 0000000000..84ab9effa3 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean @@ -0,0 +1,158 @@ +/- +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.Planar.OrdinaryRing +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayout +public import Complexity.Foundations.Geometry.Orthogonal.PairedSpokes +public import Complexity.Logics.Propositional.CNF.Compact + +/-! +# A finite compiler with paired wire ports + +Canonical incidence paths and their crossing sites are reused. Each ordinary retained cell +contains a fixed implication ring whose eight ports carry the same value. A crossing cell +contains a crossover with two equal ports on each side. Each gap receives opposite implications +on its two separate ports. Consequently the adjacent signal values must agree. + +Original clause cells contain no auxiliary variables. Their final incidences use one of the two +ports facing the clause, with four disjoint offset spokes inside the clause cell. Unused ports +belong to their cell's implication ring and introduce no independent choices. + +## Main definitions + +* `Cslib.Complexity.SAT.ParsimoniousPlanar.placedClauses`: actual clauses and geometric data. +* `Cslib.Complexity.SAT.ParsimoniousPlanar.formula`: compact natural-number output labels. +* `Cslib.Complexity.SAT.ParsimoniousPlanar.positions`, `.routes`: finite drawing data. + +## References + +The paired assembly is original. The crossover's source credit is documented in `PairedCrossover`. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- An ordinary ring port or a local crossover variable, together with its unit-cell index. -/ +abbrev Variable := Point × ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable) + +/-- A clause, its position, and one incidence route per literal, in literal order. -/ +abbrev PlacedClause := Clause Variable × Point × List Route + +/-- Reuse the already-certified canonical unit paths. -/ +abbrev paths := PlanarCompile.paths + +/-- Reuse the selected crossing cells. -/ +abbrev crossingSites := PlanarCompile.crossingSites + +/-- Reuse the occurrence-indexed canonical unit path. -/ +abbrev occurrencePath := PlanarCompile.occurrencePath + +/-- Side facing a unit neighbor, in left/right/bottom/top order. -/ +abbrev side := PlanarCompile.side + +/-- The center of a macrocell of side 240. -/ +abbrev center := PlanarCompile.center + +/-- All occupied retained ordinary cells, listed without repetitions. -/ +def ordinaryCells (φ : CNF ℕ) : List Point := + let occupied := ((paths φ).flatMap List.dropLast).filter fun p => decide (p ∉ crossingSites φ) + selectDistinct occupied (List.replicate occupied.length true) + +/-- The signal variable on a particular side and lane of a cell. -/ +def port (sites : List Point) (p : Point) (s : Fin 4) (lane : Fin 2) : Variable := + (p, if p ∈ sites then .inr (PairedCrossover.terminal s lane) else .inl (s, lane)) + +/-- Signal presented toward the neighboring cell on one lane. -/ +def signal (sites : List Point) (p q : Point) (lane : Fin 2) : Variable := + port sites p (side p q) lane + +/-- The actual displayed position of a structured variable. -/ +def variablePosition (v : Variable) : Point := + cellOrigin 120 v.1 + v.2.elim + (fun p => PairedPorts.variablePosition p.1 p.2) PairedCrossover.variablePosition + +/-- The shared side point for a specified lane. -/ +def boundary (p : Point) (s : Fin 4) (lane : Fin 2) : Point := + cellOrigin 120 p + PairedPorts.boundaryPort s lane + +/-- A straight route from a cell boundary to its presented signal. -/ +def access (sites : List Point) (p q : Point) (lane : Fin 2) : Route := + [boundary p (side p q) lane, variablePosition (signal sites p q lane)] + +/-- The clause on lane zero goes forward; the clause on lane one goes backward. -/ +def link (sites : List Point) (p q : Point) (lane : Fin 2) : PlacedClause := + let a := signal sites p q lane + let b := signal sites q p lane + let ra := access sites p q lane + let rb := access sites q p lane + (if lane = 0 then [(a, false), (b, true)] else [(b, false), (a, true)], + boundary p (side p q) lane, if lane = 0 then [ra, rb] else [rb, ra]) + +/-- Two implication clauses per gap, excluding the final step into the original clause. -/ +def links (sites : List Point) (r : Route) : List PlacedClause := + r.dropLast.consecutivePairs.flatMap fun e => [link sites e.1 e.2 0, link sites e.1 e.2 1] + +/-- Final literal and its incidence route from the original clause center. -/ +def lastLiteral (sites : List Point) (r : Route) (positive : Bool) : Literal Variable × Route := + let p := r.getD (r.length - 2) (0, 0) + let q := r.getLastD (0, 0) + let s := side q p + let lane := PairedPorts.spokeLane s + ((signal sites p q lane, positive), + [center q, cellOrigin 120 q + PairedPorts.spokeElbow s, boundary q s lane, + variablePosition (signal sites p q lane)]) + +/-- Original clauses keep their order, arity and literal signs. -/ +def originalClauses (φ : CNF ℕ) (sites : List Point) : List PlacedClause := + φ.zipIdx.map fun (c, i) => + let ls := c.zipIdx.map fun (l, j) => + lastLiteral sites (occurrencePath φ (i, j, l)) l.2 + (ls.map Prod.fst, center (Layout.center (φ.distinctVars.length + i)), ls.map Prod.snd) + +/-- The ordinary fixed implication ring in an occupied cell. -/ +def ordinaryClauses (p : Point) : List PlacedClause := + OrdinaryRing.formula.zipIdx.map fun (c, i) => + (c.relabel (fun v => (p, .inl v)), + cellOrigin 120 p + OrdinaryRing.clausePositions.getD i (0, 0), + (OrdinaryRing.incidenceRoutes.filter fun e => e.1 == i).map fun e => + translate (cellOrigin 120 p) e.2.2) + +/-- The paired-port crossover in a selected crossing cell. -/ +def crossingClauses (p : Point) : List PlacedClause := + PairedCrossover.formula.zipIdx.map fun (c, i) => + (c.relabel (fun v => (p, .inr v)), + cellOrigin 120 p + PairedCrossover.clausePositions.getD i (0, 0), + (PairedCrossover.incidenceRoutes.filter fun e => e.1 == i).map fun e => + translate (cellOrigin 120 p) e.2.2) + +/-- The actual finite output, with no clauses for unoccupied ordinary cells. -/ +def placedClauses (φ : CNF ℕ) : List PlacedClause := + let sites := crossingSites φ + originalClauses φ sites ++ (ordinaryCells φ).flatMap ordinaryClauses ++ + sites.flatMap crossingClauses ++ + (Cslib.Logic.PL.occurrences φ).flatMap fun o => links sites (occurrencePath φ o) + +/-- Output formula with structured variable names. -/ +def rawFormula (φ : CNF ℕ) : CNF Variable := (placedClauses φ).map Prod.fst + +/-- Compact natural-number labels for the actual formula. -/ +def formula (φ : CNF ℕ) : CNF ℕ := (rawFormula φ).compact + +/-- Positions ordered by the final formula's distinct variables, then its clauses. -/ +def positions (φ : CNF ℕ) : List Point := + (rawFormula φ).distinctVars.map variablePosition ++ (placedClauses φ).map fun c => c.2.1 + +/-- Incidence routes ordered by clauses and by literal positions. -/ +def routes (φ : CNF ℕ) : List Route := (placedClauses φ).flatMap fun c => c.2.2 + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean new file mode 100644 index 0000000000..fbe3820c8e --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean @@ -0,0 +1,179 @@ +/- +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.PairedSemantics +public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths +import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments +import Complexity.Foundations.Data.List.Filter +import Mathlib.Data.List.GetD + +/-! +# Unique assignments in the actual paired compiler + +Every occupied ordinary cell belongs to a retained occurrence path. Each selected crossing is +occupied by a horizontal and a vertical occurrence path. The constant-wire theorem therefore +determines both crossover inputs and every ordinary ring from the original assignment. + +## Main results + +* `Cslib.Complexity.SAT.ParsimoniousPlanar.crossing_axes_exist`: actual selected crossings carry + both independent signals. + +## References + +These are original composition proofs using the canonical path occupancy certificates. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- Every actual selected crossing is used by both a horizontal and a vertical occurrence. -/ +theorem crossing_axes_exist {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {p : Point} (hp : p ∈ crossingSites φ) : + ∃ o ∈ Cslib.Logic.PL.occurrences φ, ∃ t ∈ Cslib.Logic.PL.occurrences φ, + p ∈ occurrencePath φ o ∧ p ∈ occurrencePath φ t ∧ + StraightThrough (occurrencePath φ o) p (1, 0) ∧ + StraightThrough (occurrencePath φ t) p (0, 1) := by + have hc := ((PlanarCompile.mem_crossingSites φ p).1 hp).2.2 + rw [← PlanarCompile.occurrencePaths_eq_paths] at hc + obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := List.exists_pair_indices_of_two_le_filter_contains _ p hc + have hi' : i < (Cslib.Logic.PL.occurrences φ).length := by + simpa only [List.length_map] using hi + have hj' : j < (Cslib.Logic.PL.occurrences φ).length := by + simpa only [List.length_map] using hj + simp only [List.getElem_map] at hpi hpj + have hoi := List.getElem_mem hi' + have hoj := List.getElem_mem hj' + have hot : (Cslib.Logic.PL.occurrences φ)[i] ≠ (Cslib.Logic.PL.occurrences φ)[j] := by + intro he + exact hij ((Cslib.Logic.PL.occurrences_nodup φ).getElem_inj_iff.1 he) + rcases PlanarCompile.occurrencePath_crossing_straight hw hv hoi hp hpi with hs | hs <;> + rcases PlanarCompile.occurrencePath_crossing_straight hw hv hoj hp hpj with ht | ht + · exact False.elim (hot (PlanarCompile.crossing_axis_occurrence_eq hw hv hoi hoj hp + hpi hpj (Or.inl rfl) hs ht)) + · exact ⟨_, hoi, _, hoj, hpi, hpj, hs, ht⟩ + · exact ⟨_, hoj, _, hoi, hpj, hpi, ht, hs⟩ + · exact False.elim (hot (PlanarCompile.crossing_axis_occurrence_eq hw hv hoi hoj hp + hpi hpj (Or.inr rfl) hs ht)) + +/-- Every retained ordinary cell lies on an actual source occurrence path. -/ +theorem ordinary_occurrence_exists {φ : CNF ℕ} {p : Point} (hp : p ∈ ordinaryCells φ) : + ∃ o ∈ Cslib.Logic.PL.occurrences φ, p ∈ (occurrencePath φ o).dropLast := by + obtain ⟨⟨r, hr, hpr⟩, _⟩ := (mem_ordinaryCells φ p).1 hp + change r ∈ PlanarCompile.paths φ at hr + rw [← PlanarCompile.occurrencePaths_eq_paths] at hr + obtain ⟨o, ho, rfl⟩ := List.mem_map.mp hr + exact ⟨o, ho, hpr⟩ + +/-- A satisfying ordinary ring's value is determined by any occurrence retaining its cell. -/ +theorem ordinary_value_source {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true) + {p : Point} (hp : p ∈ ordinaryCells φ) {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) (hpo : p ∈ (occurrencePath φ o).dropLast) : + σ (p, Sum.inl (0, 0)) = sourceValue φ σ o.2.2.1 := by + obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hpo + have hk' : k < (occurrencePath φ o).length - 1 := by + simpa only [List.length_dropLast] using hk + have hwi : k < (wire (crossingSites φ) (occurrencePath φ o)).length := by + rwa [length_wire] + have hc := (wire_values_source hw hv h ho _ (List.getElem_mem hwi) 0).1 + rw [getElem_wire _ _ _ hk'] at hc + rw [← List.getElem_dropLast hk, heq] at hc + simpa only [signal, ordinary_port_value h hp] using hc + +/-- Each crossover input is exactly the source value on its occupying axis. -/ +theorem crossing_axis_value {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true) + {p : Point} (hp : p ∈ crossingSites φ) {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) (hpo : p ∈ occurrencePath φ o) + (axis : Bool) + (hs : StraightThrough (occurrencePath φ o) p (if axis then (0, 1) else (1, 0))) : + σ (p, Sum.inr (PairedCrossover.terminal (if axis then 2 else 0) 0)) = + sourceValue φ σ o.2.2.1 := by + obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hpo + obtain ⟨_, hnext, hnb⟩ := hs.getD_neighbors (PlanarCompile.occurrencePath_nodup ho) hk heq + have hk' : k < (occurrencePath φ o).length - 1 := by omega + have hwi : k < (wire (crossingSites φ) (occurrencePath φ o)).length := by + rwa [length_wire] + have hc := (wire_values_source hw hv h ho _ (List.getElem_mem hwi) 0).1 + rw [getElem_wire _ _ _ hk', heq] at hc + cases axis with + | false => + have hl : side p (p - (1, 0)) = 0 := by + simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 0 + have hr : side p (p + (1, 0)) = 1 := by + simpa [PairedPorts.neighbor] using side_neighbor p 1 + rcases hnb with ⟨hprev, _⟩ | ⟨hprev, _⟩ + all_goals + simp only [Bool.false_eq_true, ↓reduceIte] at hprev ⊢ + simp only [signal, hprev, hl, hr] at hc + rw [crossing_port_value h hp] at hc + simpa using hc + | true => + have hb : side p (p - (0, 1)) = 2 := by + simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 2 + have ht : side p (p + (0, 1)) = 3 := by + simpa [PairedPorts.neighbor] using side_neighbor p 3 + rcases hnb with ⟨hprev, _⟩ | ⟨hprev, _⟩ + all_goals + simp only [↓reduceIte] at hprev ⊢ + simp only [signal, hprev, hb, ht] at hc + rw [crossing_port_value h hp] at hc + simpa using hc + +/-- Source agreement forces agreement on every variable of every emitted ordinary ring. -/ +theorem ordinary_assignments_agree {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ τ : Variable → Bool} (hσ : (rawFormula φ).eval σ = true) + (hτ : (rawFormula φ).eval τ = true) + (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v) + {p : Point} (hp : p ∈ ordinaryCells φ) (v : OrdinaryRing.Variable) : + σ (p, Sum.inl v) = τ (p, Sum.inl v) := by + obtain ⟨o, ho, hpo⟩ := ordinary_occurrence_exists hp + have hs := (OrdinaryRing.eval_formula_iff _).1 + (((eval_rawFormula_iff φ σ).1 hσ).2.1 p hp) v + have ht := (OrdinaryRing.eval_formula_iff _).1 + (((eval_rawFormula_iff φ τ).1 hτ).2.1 p hp) v + exact hs.trans ((ordinary_value_source hw hv hσ hp ho hpo).trans + ((he _ (variable_mem_of_mem_occurrences ho)).trans + ((ordinary_value_source hw hv hτ hp ho hpo).symm.trans ht.symm))) + +/-- Source agreement forces agreement on every variable of every emitted crossover. -/ +theorem crossing_assignments_agree {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ τ : Variable → Bool} (hσ : (rawFormula φ).eval σ = true) + (hτ : (rawFormula φ).eval τ = true) + (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v) + {p : Point} (hp : p ∈ crossingSites φ) (v : PairedCrossover.Variable) : + σ (p, Sum.inr v) = τ (p, Sum.inr v) := by + obtain ⟨o, ho, t, ht, hpo, hpt, hhor, hver⟩ := crossing_axes_exist hw hv hp + have ha : σ (p, Sum.inr (PairedCrossover.terminal 0 0)) = + τ (p, Sum.inr (PairedCrossover.terminal 0 0)) := + (crossing_axis_value hw hv hσ hp ho hpo false hhor).trans + ((he _ (variable_mem_of_mem_occurrences ho)).trans + (crossing_axis_value hw hv hτ hp ho hpo false hhor).symm) + have hb : σ (p, Sum.inr (PairedCrossover.terminal 2 0)) = + τ (p, Sum.inr (PairedCrossover.terminal 2 0)) := + (crossing_axis_value hw hv hσ hp ht hpt true hver).trans + ((he _ (variable_mem_of_mem_occurrences ht)).trans + (crossing_axis_value hw hv hτ hp ht hpt true hver).symm) + have hs := congrFun (PairedCrossover.eq_canonicalExtension_of_holds + (((eval_rawFormula_iff φ σ).1 hσ).2.2.1 p hp)) v + have ht := congrFun (PairedCrossover.eq_canonicalExtension_of_holds + (((eval_rawFormula_iff φ τ).1 hτ).2.2.1 p hp)) v + exact hs.trans (by rw [ha, hb]; exact ht.symm) + + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCounting.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCounting.lean new file mode 100644 index 0000000000..4165529768 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCounting.lean @@ -0,0 +1,199 @@ +/- +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.PairedCorrectness +public import Complexity.Logics.Propositional.CNF.Compact.ModelCount +import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments +import Mathlib.Data.List.GetD + +/-! +# Parsimony of the actual paired-port compiler + +For width-three inputs with at most three literal occurrences per variable, every satisfying +source assignment has a satisfying output extension. Its values on the occurring output +variables are uniquely determined by the source assignment. Conversely, reading the ordinary +source cells recovers the source assignment. Counts use only occurring variables on both sides. + +## Main results + +* `sourceVariable_mem_rawFormula`: every used source representative occurs in the actual output. +* `raw_assignments_agree_iff`: source and output agreement coincide for satisfying assignments. +* `exists_satisfying_extension`: every satisfying source assignment has an output extension. +* `modelCount_rawFormula`, `modelCount_formula`: the actual compiler preserves model counts. +* `satisfiable_formula_iff`: the corresponding satisfiability equivalence. + +## References + +These are original counting and assignment-correspondence proofs for `PairedCompile`. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- A used source variable has an indexed literal occurrence, including repeated literals. -/ +private theorem exists_occurrence_of_mem_vars {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) : + ∃ o ∈ Cslib.Logic.PL.occurrences φ, o.2.2.1 = v := by + rw [← map_occurrences] at hv + exact List.mem_map.mp hv + +/-- Every used source cell is retained and receives an ordinary ring. -/ +theorem source_cell_mem_ordinary {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) : + Layout.center (φ.distinctVars.idxOf v) ∈ ordinaryCells φ := by + obtain ⟨o, ho, rfl⟩ := exists_occurrence_of_mem_vars hv + have hlen := PlanarCompile.occurrencePath_length_ge_two ho + change 2 ≤ (occurrencePath φ o).length at hlen + have hhead := (PlanarCompile.occurrencePath_endpoints ho).1 + change (occurrencePath φ o).head? = _ at hhead + rw [List.head?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hhead + have he := Option.some.inj hhead + have hret : Layout.center (φ.distinctVars.idxOf o.2.2.1) ∈ + (occurrencePath φ o).dropLast := by + rw [← he] + have hi : 0 < (occurrencePath φ o).dropLast.length := by + simp only [List.length_dropLast] + omega + rw [← List.getElem_dropLast hi] + exact List.getElem_mem _ + exact (mem_ordinaryCells φ _).2 + ⟨⟨_, occurrencePath_mem_paths ho, hret⟩, PlanarCompile.source_center_not_crossing ho⟩ + +/-- Every used source representative is an occurring variable of the actual raw output. -/ +theorem sourceVariable_mem_rawFormula {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) : + (Layout.center (φ.distinctVars.idxOf v), Sum.inl (0, 0)) ∈ (rawFormula φ).vars := by + have hp := source_cell_mem_ordinary hv + have hm : (Layout.center (φ.distinctVars.idxOf v), Sum.inl (0, 0)) ∈ + CNF.vars ((ordinaryClauses (Layout.center (φ.distinctVars.idxOf v))).map Prod.fst) := by + rw [map_fst_ordinaryClauses, CNF.vars_relabel] + exact List.mem_map_of_mem (OrdinaryRing.variables_used (0, 0)) + obtain ⟨c, hc, b, hvar⟩ := CNF.mem_vars.mp hm + obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hc + apply CNF.mem_vars.mpr + refine ⟨pc.1, List.mem_map.mpr ⟨pc, ?_, rfl⟩, b, hvar⟩ + simp only [placedClauses, List.mem_append, List.mem_flatMap] + exact Or.inl (Or.inl (Or.inr ⟨_, hp, hpc⟩)) + +private theorem pairedLinks_variable_value {V : Type*} (σ : V → Bool) + (cells : List (PairedWire.Cell V)) (value : Bool) + (h : ∀ c ∈ cells, ∀ lane, σ (c lane).1 = value ∧ σ (c lane).2 = value) + {v : V} (hv : v ∈ (PairedWire.links cells).vars) : σ v = value := by + obtain ⟨c, hc, b, hl⟩ := CNF.mem_vars.mp hv + obtain ⟨p, hp, hc⟩ := List.mem_flatMap.mp hc + have hm := List.of_mem_zip hp + have hfirst := h p.1 hm.1 + have hnext := h p.2 (List.mem_of_mem_tail hm.2) + simp only [PairedWire.gapClauses, List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl + · rcases Clause.fst_mem_of_mem_imp hl with hv | hv + · exact (congrArg σ (List.mem_singleton.mp hv)).trans (hfirst 0).2 + · exact (congrArg σ hv).trans (hnext 0).1 + · rcases Clause.fst_mem_of_mem_imp hl with hv | hv + · exact (congrArg σ (List.mem_singleton.mp hv)).trans (hnext 1).1 + · exact (congrArg σ hv).trans (hfirst 1).2 + +/-- Source agreement determines every occurring raw output variable. Assignments outside the +formula's variable support are unrestricted. -/ +theorem raw_assignments_agree {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ τ : Variable → Bool} (hσ : (rawFormula φ).eval σ = true) + (hτ : (rawFormula φ).eval τ = true) + (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v) : + ∀ v ∈ (rawFormula φ).vars, σ v = τ v := by + intro v hvar + obtain ⟨c, hc, b, hl⟩ := CNF.mem_vars.mp hvar + obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hc + simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc + rcases hpc with ((hpc | ⟨p, hp, hpc⟩) | ⟨p, hp, hpc⟩) | ⟨o, ho, hpc⟩ + · obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc + obtain ⟨lr, hlr, heq⟩ := List.mem_map.mp hl + obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr + have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := + List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ + have heq' : (lastLiteral (crossingSites φ) + (occurrencePath φ (ci.2, lj.2, lj.1)) lj.1.2).1.1 = v := congrArg Prod.fst heq + rw [← heq'] + exact (lastLiteral_value hw hv hσ ho).trans + ((he _ (variable_mem_of_mem_occurrences ho)).trans (lastLiteral_value hw hv hτ ho).symm) + · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc + obtain ⟨lit, _, heq⟩ := List.mem_map.mp hl + have heq' : (p, Sum.inl lit.1) = v := congrArg Prod.fst heq + rw [← heq'] + exact ordinary_assignments_agree hw hv hσ hτ he hp lit.1 + · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc + obtain ⟨lit, _, heq⟩ := List.mem_map.mp hl + have heq' : (p, Sum.inr lit.1) = v := congrArg Prod.fst heq + rw [← heq'] + exact crossing_assignments_agree hw hv hσ hτ he hp lit.1 + · have hm : v ∈ CNF.vars ((links (crossingSites φ) (occurrencePath φ o)).map Prod.fst) := + CNF.mem_vars.mpr ⟨pc.1, List.mem_map.mpr ⟨pc, hpc, rfl⟩, b, hl⟩ + rw [map_fst_links] at hm + exact (pairedLinks_variable_value σ _ _ (wire_values_source hw hv hσ ho) hm).trans + ((he _ (variable_mem_of_mem_occurrences ho)).trans + (pairedLinks_variable_value τ _ _ (wire_values_source hw hv hτ ho) hm).symm) + +/-- Among satisfying assignments, agreement on raw variables is equivalent to agreement on the +occurring source variables read at their fixed source representatives. -/ +theorem raw_assignments_agree_iff {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ τ : Variable → Bool} (hσ : (rawFormula φ).eval σ = true) + (hτ : (rawFormula φ).eval τ = true) : + (∀ v ∈ (rawFormula φ).vars, σ v = τ v) ↔ + ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v := + ⟨fun he _ hm => he _ (sourceVariable_mem_rawFormula hm), + raw_assignments_agree hw hv hσ hτ⟩ + +/-- Every satisfying source assignment extends to a satisfying raw output assignment with the +same source values. Together with `raw_assignments_agree_iff`, its occurring values are unique. -/ +theorem exists_satisfying_extension {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + (τ : ℕ → Bool) (hτ : φ.eval τ = true) : + ∃ σ : Variable → Bool, (rawFormula φ).eval σ = true ∧ + ∀ v ∈ φ.vars, sourceValue φ σ v = τ v := by + obtain ⟨σ, hcompat, hord, hcross⟩ := exists_compatible_assignment hw hv τ + have hσ := eval_rawFormula_of_compatible τ σ hcompat hord hcross hτ + refine ⟨σ, hσ, fun v hmem => ?_⟩ + obtain ⟨o, ho, rfl⟩ := exists_occurrence_of_mem_vars hmem + obtain ⟨c, hc⟩ := List.exists_mem_of_ne_nil _ (wire_ne_nil ho) + exact (wire_values_source hw hv hσ ho c hc 0).1.symm.trans (hcompat o ho c hc 0).1 + +/-- The actual raw compiler preserves satisfying-assignment counts under the source width and +literal-occurrence restrictions. Both sides count only occurring variables. -/ +theorem modelCount_rawFormula (φ : CNF ℕ) + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + (rawFormula φ).modelCount = φ.modelCount := by + refine CNF.modelCount_eq_card_filter + (fun σ (v : φ.vars.toFinset) => sourceValue φ σ v) + (fun τ => φ.eval (φ.extendAssignment τ) = true) (fun σ τ hσ hτ => ?_) fun τ => ?_ + · rw [funext_iff, Subtype.forall] + simp only [List.mem_toFinset] + exact (raw_assignments_agree_iff hw hv hσ hτ).symm + · constructor + · intro hτ + obtain ⟨σ, hσ, he⟩ := exists_satisfying_extension hw hv (φ.extendAssignment τ) hτ + exact ⟨σ, hσ, funext fun v => (he v (List.mem_toFinset.mp v.2)).trans + (CNF.extendAssignment_of_mem _ (List.mem_toFinset.mp v.2))⟩ + · rintro ⟨σ, hσ, rfl⟩ + rw [CNF.eval_extendAssignment_restrict] + exact eval_source_of_rawFormula hw hv hσ + +/-- Compact natural-number labels preserve the raw compiler's exact model count. -/ +theorem modelCount_formula (φ : CNF ℕ) + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + (formula φ).modelCount = φ.modelCount := by + rw [formula, CNF.modelCount_compact, modelCount_rawFormula φ hw hv] + +/-- The actual compact compiler preserves satisfiability under the source restrictions. -/ +theorem satisfiable_formula_iff (φ : CNF ℕ) + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + (formula φ).Satisfiable ↔ φ.Satisfiable := by + rw [← CNF.modelCount_pos_iff, ← CNF.modelCount_pos_iff, modelCount_formula φ hw hv] + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSemantics.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSemantics.lean new file mode 100644 index 0000000000..5b766bf8bf --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedSemantics.lean @@ -0,0 +1,439 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile +public import Complexity.Logics.Propositional.CNF.Planar.PairedWire +import Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments +import Complexity.Foundations.Data.List.Last +import Mathlib.Data.List.GetD +import Mathlib.Tactic.FinCases + +/-! +# Assignment semantics of the paired compiler + +The actual clause blocks use ordinary CNF evaluation. Local rings and crossovers identify the +four wire values within each cell; paired links identify consecutive cell values. The source +assignment then determines every used output variable. + +## Main definitions + +* `Cslib.Complexity.SAT.ParsimoniousPlanar.wire`: the actual two-lane entry and exit variables. + +## Main results + +* `Cslib.Complexity.SAT.ParsimoniousPlanar.eval_rawFormula_iff`: exact clause-block semantics. + +## References + +These are original composition proofs for the finite paired compiler. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.ParsimoniousPlanar + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- Every retained point contributes the entry and exit on each of its two lanes. -/ +def wire (sites : List Point) (r : Route) : List (PairedWire.Cell Variable) := + r.dropLast.zipIdx.map fun (p, i) lane => + (signal sites p (r.getD (i - 1) p) lane, signal sites p (r.getD (i + 1) p) lane) + +/-- A point receives an ordinary ring exactly when a retained path uses it outside a crossing. -/ +theorem mem_ordinaryCells (φ : CNF ℕ) (p : Point) : + p ∈ ordinaryCells φ ↔ + (∃ r ∈ paths φ, p ∈ r.dropLast) ∧ p ∉ crossingSites φ := by + simp [ordinaryCells, mem_selectDistinct_replicate, List.mem_flatMap] + +/-- No ordinary ring is emitted twice. -/ +theorem ordinaryCells_nodup (φ : CNF ℕ) : (ordinaryCells φ).Nodup := + nodup_selectDistinct _ _ + +/-- The two local clause tables retain their exact formulas under variable tagging. -/ +theorem map_fst_ordinaryClauses (p : Point) : + (ordinaryClauses p).map Prod.fst = + OrdinaryRing.formula.relabel (fun v => ((p, Sum.inl v) : Variable)) := by + change (OrdinaryRing.formula.zipIdx.map fun c => + c.1.relabel (fun v => ((p, Sum.inl v) : Variable))) = _ + calc + _ = (OrdinaryRing.formula.zipIdx.map Prod.fst).map + (Clause.relabel (fun v => ((p, Sum.inl v) : Variable))) := by rw [List.map_map]; rfl + _ = _ := by rw [List.zipIdx_map_fst]; rfl + +/-- The crossover clause table is exactly the renamed paired-port formula. -/ +theorem map_fst_crossingClauses (p : Point) : + (crossingClauses p).map Prod.fst = + PairedCrossover.formula.relabel (fun v => ((p, Sum.inr v) : Variable)) := by + change (PairedCrossover.formula.zipIdx.map fun c => + c.1.relabel (fun v => ((p, Sum.inr v) : Variable))) = _ + calc + _ = (PairedCrossover.formula.zipIdx.map Prod.fst).map + (Clause.relabel (fun v => ((p, Sum.inr v) : Variable))) := by rw [List.map_map]; rfl + _ = _ := by rw [List.zipIdx_map_fst]; rfl + +/-- The emitted formula evaluates precisely its original, ordinary, crossing, and link blocks. -/ +theorem eval_rawFormula_iff (φ : CNF ℕ) (σ : Variable → Bool) : + (rawFormula φ).eval σ = true ↔ + CNF.eval σ ((originalClauses φ (crossingSites φ)).map Prod.fst) = true ∧ + (∀ p ∈ ordinaryCells φ, + OrdinaryRing.formula.eval (fun v => σ (p, Sum.inl v)) = true) ∧ + (∀ p ∈ crossingSites φ, + PairedCrossover.formula.eval (fun v => σ (p, Sum.inr v)) = true) ∧ + ∀ o ∈ Cslib.Logic.PL.occurrences φ, + CNF.eval σ ((links (crossingSites φ) (occurrencePath φ o)).map Prod.fst) = true := by + simp only [rawFormula, placedClauses, List.map_append, List.map_flatMap] + simp_rw [map_fst_ordinaryClauses, map_fst_crossingClauses] + simp only [eval_append, Bool.and_eq_true, eval_flatMap_eq_true_iff, eval_relabel, + Function.comp_def, and_assoc] + +/-- Ordinary cell ports all carry the same value. -/ +theorem ordinary_port_value {φ : CNF ℕ} {σ : Variable → Bool} + (h : (rawFormula φ).eval σ = true) {p : Point} (hp : p ∈ ordinaryCells φ) + (s : Fin 4) (lane : Fin 2) : + σ (port (crossingSites φ) p s lane) = σ (p, Sum.inl (0, 0)) := by + have hn := ((mem_ordinaryCells φ p).1 hp).2 + have hr := ((eval_rawFormula_iff φ σ).1 h).2.1 p hp + simpa only [port, hn, ↓reduceIte] using (OrdinaryRing.eval_formula_iff _).1 hr (s, lane) + +/-- A crossing port carries the horizontal or vertical incoming value, independently of lane. -/ +theorem crossing_port_value {φ : CNF ℕ} {σ : Variable → Bool} + (h : (rawFormula φ).eval σ = true) {p : Point} (hp : p ∈ crossingSites φ) + (s : Fin 4) (lane : Fin 2) : + σ (port (crossingSites φ) p s lane) = + if s.val < 2 then σ (p, Sum.inr (PairedCrossover.terminal 0 0)) + else σ (p, Sum.inr (PairedCrossover.terminal 2 0)) := by + have hr := ((eval_rawFormula_iff φ σ).1 h).2.2.1 p hp + simpa only [port, hp, ↓reduceIte] using PairedCrossover.terminal_value_of_holds hr s lane + +/-- The paired wire has one cell for each retained path point. -/ +theorem length_wire (sites : List Point) (r : Route) : (wire sites r).length = r.length - 1 := by + simp [wire] + +/-- The actual entry and exit variables at a retained path index. -/ +theorem getElem_wire (sites : List Point) (r : Route) (i : ℕ) (hi : i < r.length - 1) : + (wire sites r)[i]'(by simpa [wire] using hi) = fun lane => + (signal sites r[i] (r.getD (i - 1) r[i]) lane, + signal sites r[i] (r.getD (i + 1) r[i]) lane) := by + simp only [wire, List.getElem_map, List.getElem_zipIdx, Nat.zero_add, List.getElem_dropLast] + +/-- An actual occurrence selects a member of the canonical path list. -/ +theorem occurrencePath_mem_paths {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) : occurrencePath φ o ∈ paths φ := by + change PlanarCompile.occurrencePath φ o ∈ PlanarCompile.paths φ + rw [← PlanarCompile.occurrencePaths_eq_paths] + exact List.mem_map_of_mem ho + +/-- The side lookup recovers each cardinal neighbor's side. -/ +theorem side_neighbor (p : Point) (s : Fin 4) : + side p (p + PairedPorts.neighbor s) = s := by + rcases p with ⟨x, y⟩ + fin_cases s <;> simp [side, PlanarCompile.side, PairedPorts.neighbor] + +/-- All four actual entry and exit values within each retained wire cell agree. -/ +theorem wire_cells_agree {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true) : + ∀ o ∈ Cslib.Logic.PL.occurrences φ, + ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), c.Agree σ := by + intro o ho c hc + unfold wire at hc + obtain ⟨⟨p, k⟩, hpk, rfl⟩ := List.mem_map.mp hc + obtain ⟨hk, heq⟩ := List.getElem?_eq_some_iff.mp (List.mem_zipIdx_iff_getElem?.mp hpk) + change (occurrencePath φ o).dropLast[k] = p at heq + 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' + 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 + simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 0 + have hr : side p (p + (1, 0)) = 1 := by + simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 1 + have hb : side p (p - (0, 1)) = 2 := by + simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 2 + have ht : side p (p + (0, 1)) = 3 := by + simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 3 + rcases PlanarCompile.occurrencePath_crossing_straight hw hv ho hp hpo with hs | hs + · obtain ⟨_, _, hnb⟩ := hs.getD_neighbors (PlanarCompile.occurrencePath_nodup ho) hk' heq' + rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ + all_goals + simp only [PairedWire.Cell.Agree, hprev, hnext, signal, hl, hr] + intro lane + rw [crossing_port_value h hp, crossing_port_value h hp, crossing_port_value h hp] + simp + · obtain ⟨_, _, hnb⟩ := hs.getD_neighbors (PlanarCompile.occurrencePath_nodup ho) hk' heq' + rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ + all_goals + simp only [PairedWire.Cell.Agree, hprev, hnext, signal, hb, ht] + intro lane + rw [crossing_port_value h hp, crossing_port_value h hp, crossing_port_value h hp] + simp + · have hord : p ∈ ordinaryCells φ := + (mem_ordinaryCells φ p).2 ⟨⟨_, occurrencePath_mem_paths ho, hpod⟩, hp⟩ + intro lane + change σ (signal _ _ _ lane) = σ (signal _ _ _ 0) ∧ + σ (signal _ _ _ lane) = σ (signal _ _ _ 0) + simp [signal, ordinary_port_value h hord] + +/-- Forgetting geometric annotations gives the generic paired-wire links exactly. -/ +theorem map_fst_links (sites : List Point) (r : Route) : + (links sites r).map Prod.fst = PairedWire.links (wire sites r) := by + simp only [links, List.map_flatMap, List.map_cons, List.map_nil, PairedWire.links] + rw [List.flatMap_def, List.flatMap_def] + congr 1 + apply List.ext_getElem + · simp [wire, List.consecutivePairs] + · intro i hi hj + have hi' : i + 2 < r.length := by + simp only [List.length_map, List.consecutivePairs, List.length_zip, + List.length_tail, List.length_dropLast] at hi + omega + simp only [List.getElem_map, List.consecutivePairs, List.getElem_zip, List.getElem_tail] + rw [getElem_wire sites r i (by omega), getElem_wire sites r (i + 1) (by omega)] + simp only [List.getElem_dropLast] + have hn : r.getD (i + 1) r[i] = r[i + 1] := List.getD_eq_getElem _ _ (by omega) + have hp : r.getD (i + 1 - 1) r[i + 1] = r[i] := by + rw [Nat.add_sub_cancel, List.getD_eq_getElem _ _ (by omega)] + simp only [hn, hp] + rfl + +/-- The source value is read at one fixed port of its ordinary source cell. -/ +def sourceValue (φ : CNF ℕ) (σ : Variable → Bool) (v : ℕ) : Bool := + σ (Layout.center (φ.distinctVars.idxOf v), Sum.inl (0, 0)) + +/-- Actual occurrence wires are nonempty. -/ +theorem wire_ne_nil {φ : CNF ℕ} {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) : + wire (crossingSites φ) (occurrencePath φ o) ≠ [] := by + have hlen := PlanarCompile.occurrencePath_length_ge_two ho + change 2 ≤ (occurrencePath φ o).length at hlen + intro he + have hw := length_wire (crossingSites φ) (occurrencePath φ o) + rw [he, List.length_nil] at hw + omega + +/-- The actual first entry has the source cell's value. -/ +theorem wire_first_value {φ : CNF ℕ} {σ : Variable → Bool} + (h : (rawFormula φ).eval σ = true) {o : Occurrence ℕ} + (ho : o ∈ Cslib.Logic.PL.occurrences φ) (fallback : PairedWire.Cell Variable) : + σ (((wire (crossingSites φ) (occurrencePath φ o)).headD fallback 0).1) = + sourceValue φ σ o.2.2.1 := by + have hlen := PlanarCompile.occurrencePath_length_ge_two ho + change 2 ≤ (occurrencePath φ o).length at hlen + have hwpos : 0 < (wire (crossingSites φ) (occurrencePath φ o)).length := by + rw [length_wire] + omega + have hhead : (wire (crossingSites φ) (occurrencePath φ o)).headD 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 + have hp := (PlanarCompile.occurrencePath_endpoints ho).1 + change (occurrencePath φ o).head? = _ at hp + rw [List.head?_eq_getElem?, List.getElem?_eq_getElem (by omega)] at hp + have hp' : (occurrencePath φ o)[0] = Layout.center (φ.distinctVars.idxOf o.2.2.1) := + Option.some.inj hp + have hret : Layout.center (φ.distinctVars.idxOf o.2.2.1) ∈ + (occurrencePath φ o).dropLast := by + rw [← hp'] + have hdrop : 0 < (occurrencePath φ o).dropLast.length := by + simp only [List.length_dropLast] + omega + rw [← List.getElem_dropLast hdrop] + exact List.getElem_mem _ + have hord := (mem_ordinaryCells φ _).2 + ⟨⟨_, occurrencePath_mem_paths ho, hret⟩, PlanarCompile.source_center_not_crossing ho⟩ + rw [hhead, getElem_wire _ _ 0 (by omega)] + simp only [Nat.zero_sub] + rw [List.getD_eq_getElem _ _ (by omega), hp'] + exact ordinary_port_value h hord _ 0 + +/-- Every actual entry and exit along an occurrence wire has exactly its source value. -/ +theorem wire_values_source {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true) + {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) : + ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), ∀ lane, + σ (c lane).1 = sourceValue φ σ o.2.2.1 ∧ + σ (c lane).2 = sourceValue φ σ o.2.2.1 := by + let fallback : PairedWire.Cell Variable := fun _ => (((0, 0), Sum.inl (0, 0)), + ((0, 0), Sum.inl (0, 0))) + have hl := ((eval_rawFormula_iff φ σ).1 h).2.2.2 o ho + rw [map_fst_links] at hl + have he := PairedWire.agree_head_of_ne_nil σ fallback _ (wire_ne_nil ho) + (wire_cells_agree hw hv h o ho) hl + rwa [wire_first_value h ho fallback] at he + +/-- Constant values along a nonempty retained wire determine its final literal. -/ +theorem lastLiteral_value_of_wire (sites : List Point) (r : Route) (positive value : Bool) + (σ : Variable → Bool) (hlen : 2 ≤ r.length) + (hcompat : ∀ c ∈ wire sites r, ∀ lane, + σ (c lane).1 = value ∧ σ (c lane).2 = value) : + σ (lastLiteral sites r positive).1.1 = value := by + have hi : r.length - 2 < r.length - 1 := by omega + have hwi : r.length - 2 < (wire sites r).length := by rwa [length_wire] + have hc := hcompat _ (List.getElem_mem hwi) + rw [getElem_wire _ _ _ hi] at hc + have hnext : r.length - 2 + 1 = r.length - 1 := by omega + have hget (d : Point) : r.getD (r.length - 1) d = r[r.length - 1] := + List.getD_eq_getElem _ _ (by omega) + simp only [hnext, hget] at hc + have hne : r ≠ [] := by intro he; rw [he] at hlen; simp at hlen + unfold lastLiteral + rw [List.getD_eq_getElem _ _ (by omega), List.getLastD_eq_getElem _ _ hne] + exact (hc _).2 + +/-- The literal emitted at an occurrence has precisely its source variable's value. -/ +theorem lastLiteral_value {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true) + {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) : + σ (lastLiteral (crossingSites φ) (occurrencePath φ o) o.2.2.2).1.1 = + sourceValue φ σ o.2.2.1 := + lastLiteral_value_of_wire _ _ _ _ σ (PlanarCompile.occurrencePath_length_ge_two ho) + (wire_values_source hw hv h ho) + +/-- Replacing occurrence variables by equal-valued endpoint variables preserves evaluation. -/ +theorem eval_originalClauses_of_values (φ : CNF ℕ) (sites : List Point) + (σ : Variable → Bool) (τ : ℕ → Bool) + (hvalues : ∀ o ∈ Cslib.Logic.PL.occurrences φ, + σ (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1 = τ o.2.2.1) : + CNF.eval σ ((originalClauses φ sites).map Prod.fst) = φ.eval τ := by + have hc (c : Clause ℕ × ℕ) (hc : c ∈ φ.zipIdx) : + Clause.eval σ (c.1.zipIdx.map fun l => + (lastLiteral sites (occurrencePath φ (c.2, l.2, l.1)) l.1.2).1) = + c.1.eval τ := by + have hm : + (c.1.zipIdx.map fun l => + (lastLiteral sites (occurrencePath φ (c.2, l.2, l.1)) l.1.2).1).map + (Literal.eval σ) = c.1.map (Literal.eval τ) := by + calc + _ = c.1.zipIdx.map (fun l => Literal.eval τ l.1) := by + rw [List.map_map] + apply List.map_congr_left + intro l hl + have ho : (c.2, l.2, l.1) ∈ Cslib.Logic.PL.occurrences φ := + List.mem_flatMap.mpr ⟨c, hc, List.mem_map.mpr ⟨l, hl, rfl⟩⟩ + simp only [Function.comp_def, Literal.eval] + rw [hvalues _ ho] + rfl + _ = (c.1.zipIdx.map Prod.fst).map (Literal.eval τ) := by rw [List.map_map]; rfl + _ = _ := by rw [List.zipIdx_map_fst] + have he := congrArg (fun bs : List Bool => bs.any id) hm + simpa only [List.any_map, Function.comp_def, id_eq, Clause.eval] using he + have hm : ((originalClauses φ sites).map Prod.fst).map (Clause.eval σ) = + φ.map (Clause.eval τ) := by + calc + _ = φ.zipIdx.map (fun c => Clause.eval τ c.1) := by + simp only [originalClauses, List.map_map, Function.comp_def] + apply List.map_congr_left + exact hc + _ = (φ.zipIdx.map Prod.fst).map (Clause.eval τ) := by rw [List.map_map]; rfl + _ = _ := by rw [List.zipIdx_map_fst] + have he := congrArg (fun bs : List Bool => bs.all id) hm + simpa only [List.all_map, Function.comp_def, id_eq, CNF.eval] using he + +/-- Every satisfying output assignment projects to a satisfying source assignment. -/ +theorem eval_source_of_rawFormula {φ : CNF ℕ} + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) + {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true) : + φ.eval (sourceValue φ σ) = true := by + rw [← eval_originalClauses_of_values φ (crossingSites φ) σ (sourceValue φ σ) + (fun _ ho => lastLiteral_value hw hv h ho)] + exact ((eval_rawFormula_iff φ σ).1 h).1 + +/-- Lift compatible values on the original path cells to the new local templates. -/ +def liftAssignment (σ : PlanarCompile.Variable → Bool) : Variable → Bool + | (p, .inl _) => σ (p, none) + | (p, .inr v) => PairedCrossover.canonicalExtension + (σ (p, some .aLeft)) (σ (p, some .bTop)) v + +/-- The lifted paired signal is the original signal on either lane. -/ +theorem liftAssignment_signal (sites : List Point) (σ : PlanarCompile.Variable → Bool) + (hcross : ∀ p ∈ sites, Crossover.splitFormula.eval (fun v => σ (p, some v)) = true) + (p q : Point) (lane : Fin 2) : + liftAssignment σ (signal sites p q lane) = σ (PlanarCompile.signal sites p q) := by + by_cases hp : p ∈ sites + · have heq := congrFun (Crossover.eq_canonicalSplitExtension_of_holds (hcross p hp)) + (Crossover.splitTerminal (side p q)) + simp only [signal, port, hp, ↓reduceIte, liftAssignment, + PairedCrossover.terminal_values_canonicalExtension, PlanarCompile.signal] + change (if (side p q).val < 2 then σ (p, some .aLeft) else σ (p, some .bTop)) = + σ (p, some (Crossover.splitTerminal (side p q))) + generalize hs : side p q = s at heq ⊢ + fin_cases s + all_goals first + | rfl + | simpa [Crossover.splitTerminal, Crossover.canonicalSplitExtension, + Crossover.canonicalExtension, Crossover.assignment, Function.comp_def, + Crossover.SplitVariable.origin] using heq.symm + · simp [signal, port, hp, liftAssignment, PlanarCompile.signal] + +/-- Every source assignment has compatible values in every local template and on both lanes. -/ +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), ∀ lane, + σ (c lane).1 = τ o.2.2.1 ∧ σ (c lane).2 = τ o.2.2.1) ∧ + (∀ p ∈ ordinaryCells φ, + OrdinaryRing.formula.eval (fun v => σ (p, Sum.inl v)) = true) ∧ + (∀ p ∈ crossingSites φ, + PairedCrossover.formula.eval (fun v => σ (p, Sum.inr v)) = true) := by + obtain ⟨σ, hcompat, hcross⟩ := PlanarCompile.exists_compatible_assignment hw hv τ + refine ⟨liftAssignment σ, ?_, ?_, ?_⟩ + · intro o ho c hc lane + unfold wire at hc + obtain ⟨⟨p, k⟩, hpk, rfl⟩ := List.mem_map.mp hc + dsimp only + rw [liftAssignment_signal _ σ hcross, liftAssignment_signal _ σ hcross] + apply hcompat o ho + (PlanarCompile.signal (crossingSites φ) p ((occurrencePath φ o).getD (k - 1) p), + PlanarCompile.signal (crossingSites φ) p ((occurrencePath φ o).getD (k + 1) p)) + exact List.mem_map.mpr ⟨(p, k), hpk, rfl⟩ + · intro p _ + exact OrdinaryRing.eval_constant _ + · intro p _ + exact PairedCrossover.eval_canonicalExtension _ _ + +/-- Compatible local assignments satisfy the actual output exactly when the source holds. -/ +theorem eval_rawFormula_of_compatible {φ : CNF ℕ} (τ : ℕ → Bool) (σ : Variable → Bool) + (hcompat : ∀ o ∈ Cslib.Logic.PL.occurrences φ, + ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), ∀ lane, + σ (c lane).1 = τ o.2.2.1 ∧ σ (c lane).2 = τ o.2.2.1) + (hord : ∀ p ∈ ordinaryCells φ, + OrdinaryRing.formula.eval (fun v => σ (p, Sum.inl v)) = true) + (hcross : ∀ p ∈ crossingSites φ, + PairedCrossover.formula.eval (fun v => σ (p, Sum.inr v)) = true) + (h : φ.eval τ = true) : (rawFormula φ).eval σ = true := by + apply (eval_rawFormula_iff φ σ).2 + refine ⟨?_, hord, hcross, ?_⟩ + · rw [eval_originalClauses_of_values φ (crossingSites φ) σ τ ?_] + · exact h + · intro o ho + exact lastLiteral_value_of_wire _ _ _ _ σ + (PlanarCompile.occurrencePath_length_ge_two ho) (hcompat o ho) + · intro o ho + rw [map_fst_links] + exact PairedWire.eval_links_of_constant σ (τ o.2.2.1) _ (hcompat o ho) + + + + + + +end Cslib.Complexity.SAT.ParsimoniousPlanar diff --git a/ComplexityTests/PairedCounting.lean b/ComplexityTests/PairedCounting.lean new file mode 100644 index 0000000000..2a2ad51583 --- /dev/null +++ b/ComplexityTests/PairedCounting.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCounting + +/-! # Exact counts and assignment correspondence of the actual paired compiler -/ + +open Cslib.Logic.PL Cslib.Complexity.SAT.ParsimoniousPlanar + +/-- The empty source has one assignment on its empty variable set. -/ +example : (formula []).modelCount = 1 := by + rw [modelCount_formula _ (by simp) (by simp [CNF.vars])] + decide + +/-- An empty clause remains unsatisfiable. -/ +example : (formula [[]]).modelCount = 0 := by + rw [modelCount_formula _ (by simp) (by simp [CNF.vars])] + decide + +/-- A singleton source variable acquires no auxiliary choices. -/ +example : (formula [[(7, true)]]).modelCount = 1 := by + rw [modelCount_formula _ (by simp) (fun _ => List.count_le_length.trans (by decide))] + decide + +/-- Repeated literal occurrences remain one forced source variable. -/ +example : (formula [[(7, true), (7, true), (7, true)]]).modelCount = 1 := by + rw [modelCount_formula _ (by simp) (fun _ => List.count_le_length.trans (by decide))] + decide + +/-- A tautological source variable retains both choices. -/ +example : (formula [[(7, true), (7, false)]]).modelCount = 2 := by + rw [modelCount_formula _ (by simp) (fun _ => List.count_le_length.trans (by decide))] + decide + +/-- Contradictory source unit clauses have no output models. -/ +example : (formula [[(0, true)], [(0, false)]]).modelCount = 0 := by + rw [modelCount_formula _ (by simp) (fun _ => List.count_le_length.trans (by decide))] + decide + +/-- Both source variables occur twice, on paths with actual selected crossings. -/ +private def crossedSource : CNF ℕ := + [[(0, true), (1, true)], [(1, false), (0, true)]] + +private theorem crossed_width : ∀ c ∈ crossedSource, c.length ≤ 3 := by decide + +private theorem crossed_count : ∀ v, crossedSource.vars.count v ≤ 3 := by + intro v + by_cases h0 : v = 0 + · subst v + decide + by_cases h1 : v = 1 + · subst v + decide + simp [crossedSource, CNF.vars, Ne.symm h0, Ne.symm h1] + +example : crossingSites crossedSource ≠ [] := by decide +kernel + +example : (formula crossedSource).modelCount = 2 := by + rw [modelCount_formula _ crossed_width crossed_count] + decide + +example : (rawFormula crossedSource).modelCount = 2 := by + rw [modelCount_rawFormula _ crossed_width crossed_count] + decide + +/-- Source values determine the actual raw models, including crossover internals. -/ +example (σ τ : Variable → Bool) (hσ : (rawFormula crossedSource).eval σ = true) + (hτ : (rawFormula crossedSource).eval τ = true) + (he : ∀ v ∈ crossedSource.vars, sourceValue crossedSource σ v = sourceValue crossedSource τ v) : + ∀ v ∈ (rawFormula crossedSource).vars, σ v = τ v := + raw_assignments_agree crossed_width crossed_count hσ hτ he + +/-- First-occurrence compaction works for an infinite variable type and sparse source names. -/ +example : (CNF.compact [[(7, true), (7, false)], [(1000000, true)]]).modelCount = 2 := by + rw [CNF.modelCount_compact] + decide + +/-- Compaction also works when the variable type is empty. -/ +example : (CNF.compact ([] : CNF Empty)).modelCount = 1 := by + rw [CNF.modelCount_compact] + decide diff --git a/ComplexityTests/PlanarCompile.lean b/ComplexityTests/PlanarCompile.lean index c6ee76142c..18766bc64c 100644 --- a/ComplexityTests/PlanarCompile.lean +++ b/ComplexityTests/PlanarCompile.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Erik Demaine -/ -import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree import Complexity.Logics.Propositional.CNF.ImplicationChain @@ -12,7 +12,7 @@ import Complexity.Logics.Propositional.CNF.ImplicationChain namespace ComplexityTests.PlanarCompile open Cslib.Logic.PL Cslib.Orthogonal Cslib.Complexity -open SAT.PlanarCompile +open SAT.ParsimoniousPlanar -- The compiler preserves the two degenerate SAT instances, including the empty clause. example : formula [] = [] := by decide +kernel @@ -20,20 +20,20 @@ example : formula [[]] = [[]] := by decide +kernel -- A unit clause produces a nonempty wire, without inserting any crossing gadgets. example : crossingSites [[(7, true)]] = [] := by decide +kernel -example : (rawFormula [[(7, true)]]).length = 32 := by decide +kernel -example : (rawFormula [[(7, true)]]).vars.length = 63 := by decide +kernel +example : (rawFormula [[(7, true)]]).length = 319 := by decide +kernel +example : (rawFormula [[(7, true)]]).vars.length = 637 := by decide +kernel example : (rawFormula [[(7, true)]]).eval (fun _ => true) = true := by decide +kernel --- Crossing ports use the same left/right/bottom/top order as the macrocell API. -example : signal [(0, 0)] (0, 0) (-1, 0) = - ((0, 0), some CNF.Crossover.SplitVariable.aLeft) := by decide -example : access [] (0, 0) (1, 0) = [(240, 120), (120, 120)] := by decide +-- Crossing ports retain the side order and keep both lanes separate. +example : signal [(0, 0)] (0, 0) (-1, 0) 0 = + ((0, 0), Sum.inr (CNF.PairedCrossover.terminal 0 0)) := by decide +example : access [] (0, 0) (1, 0) 0 = [(240, 110), (220, 110)] := by decide --- Directed links need one binary clause, with the polarity-dependent orientation. -example : (link [] true (0, 0) (1, 0)).1 = - [(((1, 0), none), false), (((0, 0), none), true)] := by decide -example : (link [] false (0, 0) (1, 0)).1 = - [(((0, 0), none), false), (((1, 0), none), true)] := by decide +-- Separate forward and backward lanes close the slack between adjacent cells. +example : (link [] (0, 0) (1, 0) 0).1 = + [(((0, 0), Sum.inl (1, 0)), false), (((1, 0), Sum.inl (0, 0)), true)] := by decide +example : (link [] (0, 0) (1, 0) 1).1 = + [(((1, 0), Sum.inl (0, 1)), false), (((0, 0), Sum.inl (1, 1)), true)] := by decide -- Repeated literal incidences contribute separately to the actual graph degree. example : (SAT.incidenceGraph [[(5, true), (5, false)]]).incidenceVertices.count 0 = 2 := diff --git a/ComplexityTests/PlanarSemantics.lean b/ComplexityTests/PlanarSemantics.lean index d82724d1ce..d2947cb382 100644 --- a/ComplexityTests/PlanarSemantics.lean +++ b/ComplexityTests/PlanarSemantics.lean @@ -3,9 +3,10 @@ Copyright (c) 2026 Erik Demaine. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Erik Demaine -/ -import Complexity.Computability.Complexity.Problems.SAT.Planar.Completeness +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCounting +import Mathlib.Tactic.FinCases -open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Complexity.SAT.PlanarCompile +open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Complexity.SAT.ParsimoniousPlanar -- Concrete nonempty actual compiler outputs have satisfying assignments for both polarities. example : (rawFormula [[(0, true)]]).eval (fun _ => true) = true := by decide +kernel @@ -14,11 +15,12 @@ example : (rawFormula [[(0, false)]]).eval (fun _ => false) = true := by decide -- The actual compact output cannot manufacture a model of contradictory unit clauses. example : ¬ (formula [[(0, true)], [(0, false)]]).Satisfiable := by intro hs - obtain ⟨τ, hτ⟩ := satisfiable_source_of_formula + have hsource := (satisfiable_formula_iff [[(0, true)], [(0, false)]] (by decide : ∀ c ∈ ([[(0, true)], [(0, false)]] : CNF ℕ), c.length ≤ 3) (fun v => (List.count_le_length : (CNF.vars ([[(0, true)], [(0, false)]] : CNF ℕ)).count v ≤ - (CNF.vars ([[(0, true)], [(0, false)]] : CNF ℕ)).length).trans (by decide)) hs + (CNF.vars ([[(0, true)], [(0, false)]] : CNF ℕ)).length).trans (by decide))).1 hs + obtain ⟨τ, hτ⟩ := hsource cases hv : τ 0 <;> simp [CNF.eval, Clause.eval, Literal.eval, hv] at hτ private def crossedSource : CNF ℕ := @@ -40,29 +42,39 @@ private theorem crossed_count : ∀ v, crossedSource.vars.count v ≤ 3 := by simp [crossedSource, CNF.vars, Ne.symm h0, Ne.symm h1] example : (formula crossedSource).Satisfiable := by - apply (satisfiable_formula_iff crossed_width crossed_count).2 + apply (satisfiable_formula_iff crossedSource crossed_width crossed_count).2 exact ⟨fun v => v == 0, by decide⟩ example : (formula []).Satisfiable := by - apply (satisfiable_formula_iff (by simp) (by simp [CNF.vars])).2 + apply (satisfiable_formula_iff [] (by simp) (by simp [CNF.vars])).2 exact ⟨fun _ => false, rfl⟩ example : ¬ (formula [[]]).Satisfiable := by - rw [satisfiable_formula_iff (by simp) (by simp [CNF.vars])] + rw [satisfiable_formula_iff [[]] (by simp) (by simp [CNF.vars])] rintro ⟨τ, hτ⟩ simp [CNF.eval, Clause.eval] at hτ -- At this actual selected crossing, horizontal true and vertical false coexist in one model. example : ∃ σ : Variable → Bool, (rawFormula crossedSource).eval σ = true ∧ - σ ((10, 34), some Crossover.SplitVariable.aLeft) = true ∧ - σ ((10, 34), some Crossover.SplitVariable.bTop) = false := by + σ ((10, 34), Sum.inr (CNF.PairedCrossover.terminal 0 0)) = true ∧ + σ ((10, 34), Sum.inr (CNF.PairedCrossover.terminal 2 0)) = false := by let τ : ℕ → Bool := fun v => v == 0 - obtain ⟨σ, hcompat, hcross⟩ := exists_compatible_assignment crossed_width crossed_count τ + obtain ⟨σ, hcompat, hord, hcross⟩ := exists_compatible_assignment crossed_width crossed_count τ have hh := hcompat (0, 0, (0, true)) (by decide) - (((10, 34), some Crossover.SplitVariable.aLeft), - ((10, 34), some Crossover.SplitVariable.aRight)) (by decide +kernel) + (fun lane => (signal (crossingSites crossedSource) (10, 34) (9, 34) lane, + signal (crossingSites crossedSource) (10, 34) (11, 34) lane)) (by + apply List.mem_iff_getElem.mpr + refine ⟨40, by decide +kernel, ?_⟩ + funext lane + fin_cases lane <;> decide +kernel) 0 have hv := hcompat (0, 1, (1, true)) (by decide) - (((10, 34), some Crossover.SplitVariable.bTop), - ((10, 34), some Crossover.SplitVariable.bBottom)) (by decide +kernel) - exact ⟨σ, eval_rawFormula_complete_of_compatible crossedSource τ σ - (fun _ ho => occurrencePath_length_ge_two ho) hcompat hcross (by decide), hh.1, hv.1⟩ + (fun lane => (signal (crossingSites crossedSource) (10, 34) (10, 33) lane, + signal (crossingSites crossedSource) (10, 34) (10, 35) lane)) (by + apply List.mem_iff_getElem.mpr + refine ⟨24, by decide +kernel, ?_⟩ + funext lane + fin_cases lane <;> decide +kernel) 0 + have hp : (10, 34) ∈ crossingSites crossedSource := by decide +kernel + refine ⟨σ, eval_rawFormula_of_compatible τ σ hcompat hord hcross (by decide), ?_, ?_⟩ + · simpa [signal, port, hp, side, Cslib.Complexity.SAT.PlanarCompile.side, τ] using hh.1 + · simpa [signal, port, hp, side, Cslib.Complexity.SAT.PlanarCompile.side, τ] using hv.1