Distinct actual clause and variable vertices

The actual clause-position list follows the output formula. Certified inner profile vertices are distinct, different boxes have different original clause owners, and original variable centers cannot lie in any clause box.

Main results

• positiveClausePositions_nodup: actual clause vertices have no repeated position.
• positiveVariablePoint_ne_clause: actual variables avoid every clause vertex.
• positiveDrawing_positions_nodup: all actual output graph vertices are distinct.

References

These global vertex-separation proofs are original.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_clause_length (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) : (clauseGeometry φ d i c).clausePositions.length = List.length (profileFormula (clauseProfile c))

The selected clause-position list has the exact actual profile clause length.

theorem Cslib.Complexity.SAT.ExactOne.positiveClauseBlock_positions (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) : List.map (fun (pc : PositivePlacedClause) => pc.point) (positiveClauseBlock φ d i c) = List.map (fun (x : Orthogonal.Point) => positiveBoxOrigin φ d i + x) (clauseGeometry φ d i c).clausePositions

A clause block lists precisely the translated local clause positions in order.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_clause_bounds (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) {p : Orthogonal.Point} (hp : p ∈ (clauseGeometry φ d i c).clausePositions) : InPositiveLocalBox p

Every actual local clause point lies in the common closed collar square.

theorem Cslib.Complexity.SAT.ExactOne.positiveClauseBlock_positions_nodup (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) : (List.map (fun (pc : PositivePlacedClause) => pc.point) (positiveClauseBlock φ d i c)).Nodup

A single actual clause box has distinct clause points.

theorem Cslib.Complexity.SAT.ExactOne.positiveClauseBlock_positions_disjoint {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) (hij : i ≠ j) (c c' : Logic.PL.Clause ℕ) : (List.map (fun (pc : PositivePlacedClause) => pc.point) (positiveClauseBlock φ d i c)).Disjoint (List.map (fun (pc : PositivePlacedClause) => pc.point) (positiveClauseBlock φ d j c'))

A clause-box point identifies its original source-clause owner.

theorem Cslib.Complexity.SAT.ExactOne.positiveClausePositions_nodup {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) : (List.map (fun (pc : PositivePlacedClause) => pc.point) (positivePlacedClauses φ d)).Nodup

Every actual output clause has its own distinct displayed point.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_auxiliary_ne_clause (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ profileVariables (clauseProfile c)) (ha : ∀ (n : ℕ), v ≠ Sum.inl (Sum.inl n)) {p : Orthogonal.Point} (hp : p ∈ (clauseGeometry φ d i c).clausePositions) : (clauseGeometry φ d i c).variablePosition (List.idxOf v (profileVariables (clauseProfile c))) ≠ p

Private local auxiliary points and actual local clause points are different.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePoint_ne_clause {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {v : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} (hv : v ∈ (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ).vars) {p : Orthogonal.Point} (hp : p ∈ List.map (fun (pc : PositivePlacedClause) => pc.point) (positivePlacedClauses φ d)) : positiveVariablePoint φ d v ≠ p

No actual source or private variable point coincides with an actual clause point.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_positions_nodup {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) : (positiveDrawing φ d).1.Nodup

Every actual output graph vertex has a distinct displayed point.