Nonincident-vertex avoidance from actual occurrence contacts

Once every displayed variable and nonempty clause has its own incident route, pairwise contact control already implies nonincident-vertex avoidance. The only possible ambiguity would identify a variable point with a clause point; the distinct displayed positions exclude that ambiguity.

Main results

• FormulaDrawing.avoidsVariables_of_contacts: used variable vertices cannot lie on other routes.
• FormulaDrawing.avoidsClauses_of_contacts: nonempty clause vertices cannot lie on other routes.

References

These elementary consequences of occurrence-indexed drawing certificates are original.

theorem Cslib.Complexity.SAT.ExactOne.FormulaDrawing.avoidsVariables_of_contacts {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} {a : FormulaDrawing φ} (hcount : a.clausePoints.length = List.length φ) (hnd : a.positions.Nodup) (hends : ∀ o ∈ Logic.PL.occurrences φ, List.getLast? (a.incidenceRoute o) = some (a.variablePoint o.2.2.1)) (hcontacts : ∀ o ∈ Logic.PL.occurrences φ, ∀ t ∈ Logic.PL.occurrences φ, o ≠ t → ∀ p ∈ Orthogonal.support (a.incidenceRoute o), p ∈ Orthogonal.support (a.incidenceRoute t) → o.2.2.1 = t.2.2.1 ∧ p = Orthogonal.realPoint (a.variablePoint o.2.2.1) ∨ o.1 = t.1 ∧ p = Orthogonal.realPoint (a.clausePoints.getD o.1 (0, 0))) (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → ∀ v ∈ φ.vars, Orthogonal.realPoint (a.variablePoint v) ∈ Orthogonal.support (a.incidenceRoute o) → v = o.2.2.1

Used variable vertices cannot lie on another incidence once actual endpoint contacts and variable/clause separation have been checked.

theorem Cslib.Complexity.SAT.ExactOne.FormulaDrawing.avoidsClauses_of_contacts {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} {a : FormulaDrawing φ} (hcount : a.clausePoints.length = List.length φ) (hnd : a.positions.Nodup) (hnonempty : ∀ c ∈ φ, c ≠ []) (hends : ∀ o ∈ Logic.PL.occurrences φ, List.head? (a.incidenceRoute o) = some (a.clausePoints.getD o.1 (0, 0))) (hcontacts : ∀ o ∈ Logic.PL.occurrences φ, ∀ t ∈ Logic.PL.occurrences φ, o ≠ t → ∀ p ∈ Orthogonal.support (a.incidenceRoute o), p ∈ Orthogonal.support (a.incidenceRoute t) → o.2.2.1 = t.2.2.1 ∧ p = Orthogonal.realPoint (a.variablePoint o.2.2.1) ∨ o.1 = t.1 ∧ p = Orthogonal.realPoint (a.clausePoints.getD o.1 (0, 0))) (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → ∀ i < List.length φ, Orthogonal.realPoint (a.clausePoints.getD i (0, 0)) ∈ Orthogonal.support (a.incidenceRoute o) → i = o.1

Every nonempty clause vertex avoids other incidence routes once actual endpoint contacts and variable/clause separation have been checked.