Local orthogonal drawings for parsimonious exact-one gadgets

The three fixed drawings fit in [0,180]². Their core vertices and routes lie in [20,160]²; access routes run from designated boundary ports to their terminals. The ports are on the y = 0 (north), x = 0 (west) and x = 180 (east) sides: the side midpoints for disjunctionGeometry and complementGeometry, and (80, 0) for falseGeometry. The unsigned incidence signatures deliberately leave clause semantics to the logical gadgets.

Main definitions

• LocalIncidence: an incidence record, read through clauseIndex, variableIndex and route.
• LocalGeometry: finite vertex, incidence, and access data for a local replacement.
• disjunctionGeometry: the four-clause parsimonious disjunction replacement.
• falseGeometry: the three-clause positive gadget with a forced-false exterior terminal.
• complementGeometry: a positive two-terminal gadget forcing opposite values.

References

The incidence graphs are from [HuntMaratheRadhakrishnanStearns1998, Theorem 3.8, Figures 3.4–3.5 and Lemma 3.6]. The orthogonal coordinates and routes are original.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.LocalIncidence : Type

An incidence records its clause index, variable index, and clause-to-variable route.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.LocalIncidence.clauseIndex (e : LocalIncidence) : ℕ

The local index of the incident clause.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.LocalIncidence.variableIndex (e : LocalIncidence) : ℕ

The local index of the incident variable.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.LocalIncidence.route (e : LocalIncidence) : Orthogonal.Route

The route from the clause position to the variable position.

structure Cslib.Complexity.SAT.ExactOne.LocalGeometry : Type

Finite local replacement data. Variables and clauses have separate zero-based indices. terminalVariables, boundaryPorts, and accessRoutes have corresponding orders.

• size : ℕ

  Common square side length; the elementary templates use 180.

• variablePositions : List Orthogonal.Point

  Positions in variable-index order.

• clausePositions : List Orthogonal.Point

  Positions in clause-index order.

• incidenceRoutes : List LocalIncidence

  Routes with their incident clause and variable indices.

• terminalVariables : List ℕ

  Variables exposed to the exterior.

• boundaryPorts : List Orthogonal.Point

  Exterior endpoints of the access routes.

• accessRoutes : List Orthogonal.Route

  Boundary-to-terminal routes.

def Cslib.Complexity.SAT.ExactOne.LocalGeometry.variablePosition (g : LocalGeometry) (v : ℕ) : Orthogonal.Point

Indexed variable position; valid incidence indices are certified separately.

def Cslib.Complexity.SAT.ExactOne.LocalGeometry.clausePosition (g : LocalGeometry) (i : ℕ) : Orthogonal.Point

Indexed clause position; valid incidence indices are certified separately.

def Cslib.Complexity.SAT.ExactOne.LocalGeometry.commonEndpoints (g : LocalGeometry) (e f : LocalIncidence) : List Orthogonal.Point

Permitted contacts of two incidence routes: their shared graph endpoints.

def Cslib.Complexity.SAT.ExactOne.disjunctionGeometry : LocalGeometry

The four-clause disjunction gadget. Variables are p,q,r,u,v,w,t,x in that order; the incidence signature is [[p,u,v],[q,u,w],[v,w,t],[r,v,x]]. The boundary terminals are p,q,r, with north, west, and east accesses.

def Cslib.Complexity.SAT.ExactOne.falseGeometry : LocalGeometry

The positive forced-false gadget. Variables are c,d,e,f; the three clauses have signature [[c,d,e],[c,e,f],[d,e,f]]. The terminal c has a north access.

def Cslib.Complexity.SAT.ExactOne.complementGeometry : LocalGeometry

A positive complement gadget: one clause on p,q,c followed by the forced-false gadget on c,d,e,f. The terminals p,q have west and east accesses.