Validity of the actual positive exact-one drawing

Each actual output occurrence is identified with its finite local incidence. Source ports splice into the original routes, and all contacts are checked on full real supports.

Main results

• positiveFormulaDrawing_valid: all actual output vertices and routes satisfy the geometric incidence conditions.
• positiveDrawing_isPlanarOrthogonalDrawing: the emitted drawing realizes the actual compact positive exact-one formula.

References

The global replacement and its continuous geometric correctness proof are original.

theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_clauseCount (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : (positiveFormulaDrawing φ d).clausePoints.length = List.length (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)

The actual occurrence-indexed compiler has exactly one clause point per output clause.

theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_clausePoint_injective {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i j : ℕ} (hi : i < List.length (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) (hj : j < List.length (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) (he : (positiveFormulaDrawing φ d).clausePoints.getD i (0, 0) = (positiveFormulaDrawing φ d).clausePoints.getD j (0, 0)) : i = j

Actual output clause positions identify their actual clause indices.

theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_occurrence_injective (φ : Logic.PL.CNF ℕ) {o t : Logic.PL.Occurrence (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} (ho : o ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) (ht : t ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) (hclause : o.1 = t.1) (hvar : o.2.2.1 = t.2.2.1) : o = t

A clause and its variable identify an actual output occurrence, since output clauses have distinct variables.

theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_endpoints {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {o : Logic.PL.Occurrence (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} (ho : o ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) : List.head? ((positiveFormulaDrawing φ d).incidenceRoute o) = some ((positiveFormulaDrawing φ d).clausePoints.getD o.1 (0, 0)) ∧ List.getLast? ((positiveFormulaDrawing φ d).incidenceRoute o) = some ((positiveFormulaDrawing φ d).variablePoint o.2.2.1)

Every actual route begins at its actual output clause and ends at its actual output variable.

theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_regular {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {o : Logic.PL.Occurrence (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} (ho : o ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) : Orthogonal.IsOrthogonal ((positiveFormulaDrawing φ d).incidenceRoute o) ∧ Orthogonal.IsSimple ((positiveFormulaDrawing φ d).incidenceRoute o)

Every actual output route is proper, orthogonal and continuously simple.

theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_contacts {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {o t : Logic.PL.Occurrence (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} (ho : o ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) (ht : t ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) (hot : o ≠ t) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support ((positiveFormulaDrawing φ d).incidenceRoute o)) (hq : p ∈ Orthogonal.support ((positiveFormulaDrawing φ d).incidenceRoute t)) : o.2.2.1 = t.2.2.1 ∧ p = Orthogonal.realPoint ((positiveFormulaDrawing φ d).variablePoint o.2.2.1) ∨ o.1 = t.1 ∧ p = Orthogonal.realPoint ((positiveFormulaDrawing φ d).clausePoints.getD o.1 (0, 0))

Full continuous contacts of distinct actual occurrences are their actual common endpoints.

theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_valid {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) : (positiveFormulaDrawing φ d).Valid

All actual output positions and full real route supports satisfy the incidence drawing laws.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_isPlanarOrthogonalDrawing {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) : (incidenceGraph (Logic.PL.CNF.PositiveExactOneCompile.formula φ)).IsPlanarOrthogonalDrawing (positiveDrawing φ d)

The emitted drawing realizes the incidence graph of the actual compact positive formula.