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; mem_placedClauses splits membership into the four kinds of record, and exists_occurrence_of_mem_originalClauses traces each literal and route of an original clause record to its source occurrence.
• 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.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.Variable : Type

An ordinary ring port or a local crossover variable, together with its unit-cell index.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.PlacedClause : Type

A clause, its position, and one incidence route per literal, in literal order.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.paths (φ : Logic.PL.CNF ℕ) : List Orthogonal.Route

Reuse the already-certified canonical unit paths.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.crossingSites (φ : Logic.PL.CNF ℕ) : List Orthogonal.Point

Reuse the selected crossing cells.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.occurrencePath (φ : Logic.PL.CNF ℕ) (o : Logic.PL.Occurrence ℕ) : Orthogonal.Route

Reuse the occurrence-indexed canonical unit path.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.side (p q : Orthogonal.Point) : Fin 4

Side facing a unit neighbor, in left/right/bottom/top order.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ParsimoniousPlanar.center (p : Orthogonal.Point) : Orthogonal.Point

The center of a macrocell of side 240.

def Cslib.Complexity.SAT.ParsimoniousPlanar.ordinaryCells (φ : Logic.PL.CNF ℕ) : List Orthogonal.Point

All occupied retained ordinary cells, listed without repetitions.

def Cslib.Complexity.SAT.ParsimoniousPlanar.port (sites : List Orthogonal.Point) (p : Orthogonal.Point) (s : Fin 4) (lane : Fin 2) : Variable

The signal variable on a particular side and lane of a cell.

def Cslib.Complexity.SAT.ParsimoniousPlanar.signal (sites : List Orthogonal.Point) (p q : Orthogonal.Point) (lane : Fin 2) : Variable

Signal presented toward the neighboring cell on one lane.

def Cslib.Complexity.SAT.ParsimoniousPlanar.variablePosition (v : Variable) : Orthogonal.Point

The actual displayed position of a structured variable.

def Cslib.Complexity.SAT.ParsimoniousPlanar.boundary (p : Orthogonal.Point) (s : Fin 4) (lane : Fin 2) : Orthogonal.Point

The shared side point for a specified lane.

def Cslib.Complexity.SAT.ParsimoniousPlanar.access (sites : List Orthogonal.Point) (p q : Orthogonal.Point) (lane : Fin 2) : Orthogonal.Route

A straight route from a cell boundary to its presented signal.

def Cslib.Complexity.SAT.ParsimoniousPlanar.link (sites : List Orthogonal.Point) (p q : Orthogonal.Point) (lane : Fin 2) : PlacedClause

The clause on lane zero goes forward; the clause on lane one goes backward.

def Cslib.Complexity.SAT.ParsimoniousPlanar.links (sites : List Orthogonal.Point) (r : Orthogonal.Route) : List PlacedClause

Two implication clauses per gap, excluding the final step into the original clause.

def Cslib.Complexity.SAT.ParsimoniousPlanar.lastLiteral (sites : List Orthogonal.Point) (r : Orthogonal.Route) (positive : Bool) : Logic.PL.Literal Variable × Orthogonal.Route

Final literal and its incidence route from the original clause center.

def Cslib.Complexity.SAT.ParsimoniousPlanar.originalClauses (φ : Logic.PL.CNF ℕ) (sites : List Orthogonal.Point) : List PlacedClause

Original clauses keep their order, arity and literal signs.

def Cslib.Complexity.SAT.ParsimoniousPlanar.ordinaryClauses (p : Orthogonal.Point) : List PlacedClause

The ordinary fixed implication ring in an occupied cell.

def Cslib.Complexity.SAT.ParsimoniousPlanar.crossingClauses (p : Orthogonal.Point) : List PlacedClause

The paired-port crossover in a selected crossing cell.

def Cslib.Complexity.SAT.ParsimoniousPlanar.placedClauses (φ : Logic.PL.CNF ℕ) : List PlacedClause

The actual finite output, with no clauses for unoccupied ordinary cells.

def Cslib.Complexity.SAT.ParsimoniousPlanar.rawFormula (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF Variable

Output formula with structured variable names.

def Cslib.Complexity.SAT.ParsimoniousPlanar.formula (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF ℕ

Compact natural-number labels for the actual formula.

def Cslib.Complexity.SAT.ParsimoniousPlanar.positions (φ : Logic.PL.CNF ℕ) : List Orthogonal.Point

Positions ordered by the final formula's distinct variables, then its clauses.

def Cslib.Complexity.SAT.ParsimoniousPlanar.routes (φ : Logic.PL.CNF ℕ) : List Orthogonal.Route

Incidence routes ordered by clauses and by literal positions.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.mem_links {sites : List Orthogonal.Point} {r : Orthogonal.Route} {pc : PlacedClause} : pc ∈ links sites r ↔ ∃ e ∈ (List.dropLast r).consecutivePairs, pc = link sites e.1 e.2 0 ∨ pc = link sites e.1 e.2 1

The seam clauses of a route are the two lane clauses of each step before the final one.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.mem_placedClauses {φ : Logic.PL.CNF ℕ} {pc : PlacedClause} : pc ∈ placedClauses φ ↔ pc ∈ originalClauses φ (crossingSites φ) ∨ (∃ p ∈ ordinaryCells φ, pc ∈ ordinaryClauses p) ∨ (∃ p ∈ crossingSites φ, pc ∈ crossingClauses p) ∨ ∃ o ∈ Logic.PL.occurrences φ, ∃ e ∈ (List.dropLast (occurrencePath φ o)).consecutivePairs, pc = link (crossingSites φ) e.1 e.2 0 ∨ pc = link (crossingSites φ) e.1 e.2 1

Case analysis on the output records: an original clause, a clause of an ordinary ring or of a crossover in its cell, or one of the two lane clauses of an occurrence path step.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.exists_occurrence_of_mem_originalClauses {φ : Logic.PL.CNF ℕ} {sites : List Orthogonal.Point} {c : Logic.PL.Clause Variable} {p : Orthogonal.Point} {rs : List Orthogonal.Route} (hpc : (c, p, rs) ∈ originalClauses φ sites) : (∀ l ∈ c, ∃ (i : ℕ) (j : ℕ) (x : Logic.PL.Literal ℕ), (i, j, x) ∈ Logic.PL.occurrences φ ∧ (lastLiteral sites (occurrencePath φ (i, j, x)) x.2).1 = l) ∧ ∀ r ∈ rs, ∃ (i : ℕ) (j : ℕ) (x : Logic.PL.Literal ℕ), (i, j, x) ∈ Logic.PL.occurrences φ ∧ (lastLiteral sites (occurrencePath φ (i, j, x)) x.2).2 = r

Each literal and each route of an original clause record (c, p, rs) is the final literal or final incidence of one occurrence (i, j, x) of the source formula, carrying the sign of its source literal x.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.mem_ordinaryCells (φ : Logic.PL.CNF ℕ) (p : Orthogonal.Point) : p ∈ ordinaryCells φ ↔ (∃ r ∈ paths φ, p ∈ List.dropLast r) ∧ p ∉ crossingSites φ

A point receives an ordinary ring exactly when a retained path uses it outside a crossing.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.ordinaryCells_nodup (φ : Logic.PL.CNF ℕ) : (ordinaryCells φ).Nodup

No ordinary ring is emitted twice.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.signal_position (sites : List Orthogonal.Point) (p q : Orthogonal.Point) (l : Fin 2) : variablePosition (signal sites p q l) = Orthogonal.cellOrigin 120 p + Orthogonal.PairedPorts.variablePosition (side p q) l

The compiler's presented signal always has the shared inner access position.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.access_eq_translate (sites : List Orthogonal.Point) (p q : Orthogonal.Point) (l : Fin 2) : access sites p q l = Orthogonal.translate (Orthogonal.cellOrigin 120 p) (Orthogonal.PairedPorts.accessRoute (side p q) l)

Actual accesses are translations of the fixed paired-port accesses.

def Cslib.Complexity.SAT.ParsimoniousPlanar.finalLocalRoute (s : Fin 4) : Orthogonal.Route

Local template of the final incidence route inside a clause cell.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.finalRoute_eq_translate (sites : List Orthogonal.Point) {p q : Orthogonal.Point} (h : Orthogonal.length p q = 1) : [center q, Orthogonal.cellOrigin 120 q + Orthogonal.PairedPorts.spokeElbow (side q p), boundary q (side q p) (Orthogonal.PairedPorts.spokeLane (side q p)), variablePosition (signal sites p q (Orthogonal.PairedPorts.spokeLane (side q p)))] = Orthogonal.translate (Orthogonal.cellOrigin 120 q) (finalLocalRoute (side q p))

Actual final literal routes are translations of finalLocalRoute.