Explicit orthogonal crossover data

The original straight-ray crossover is scaled by twenty. Each degree-six variable is replaced inside its radius-four square by six occurrence variables and a cyclic implication ring. The original incidence rays are replaced by explicit orthogonal paths in disjoint narrow corridors. The core lies in [20,220]². Four access routes connect its signal terminals to the boundary of [0,240]², using the free third incidence direction at each terminal.

Main definitions

• Cslib.Logic.PL.CNF.Crossover.variablePosition: the 53 distinct variable positions.
• Cslib.Logic.PL.CNF.Crossover.clausePositions: the 74 clause positions.
• Cslib.Logic.PL.CNF.Crossover.incidenceRoutes: the 154 clause-to-variable incidence routes.

Main results

The finite certificates for these data are in CrossoverLayoutChecks; their continuous consequences are in CrossoverLayout.

References

• David Lichtenstein, Planar Formulae and Their Uses, Figs. 4–5 [Lic82].
• MIT–ULB CompGeom Group, Undecidability of Tiling with a Tromino, Fig. 8(b) [MITULBCGGAA+25].

The fixed orthogonal routes and local splitting are original modifications of that grid drawing.

def Cslib.Logic.PL.CNF.Crossover.variablePosition : SplitVariable → Orthogonal.Point

Distinct positions for the five unsplit variables and the 48 local occurrence copies.

def Cslib.Logic.PL.CNF.Crossover.clausePositions : List Orthogonal.Point

Clause positions, in precisely the order of splitFormula.

def Cslib.Logic.PL.CNF.Crossover.incidenceRoutes : List (ℕ × SplitVariable × Orthogonal.Route)

All clause-to-variable incidence routes, in clause and literal order. The first component is a clause index; the second is its incident variable.

def Cslib.Logic.PL.CNF.Crossover.boundaryPort : Fin 4 → Orthogonal.Point

Boundary access points in left/right/top/bottom order. They are geometric ports, not additional SAT variables. An external implication route continues from this point to the terminal.

def Cslib.Logic.PL.CNF.Crossover.accessRoute (i : Fin 4) : Orthogonal.Route

Straight access from the outer box boundary to the degree-two terminal.