Documentation

CslibFrontier.Computability.Complexity.Problems.SAT.ExactOne.DrawingAssembly

Actual occurrence indices of the positive drawing #

The local clause records are assembled in the output formula's order. The occurrence-indexed view in this module retains precisely the emitted position and route lists.

Main definitions #

Main results #

References #

The assembly and indexing proofs are original.

source
def Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) :
FormulaDrawing (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)

Index the emitted route lists by actual output clause and literal positions.

Instances For
    source
    theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_drawing (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) :
    (positiveFormulaDrawing φ d).drawing = positiveDrawing φ d

    The occurrence-indexed view has exactly the compiler's actual position and route lists.

    source
    theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_occurrence (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {o : Logic.PL.Occurrence (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} (ho : o ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) :
    ∃ pc ∈ positivePlacedClauses φ d, pc.point = (positiveFormulaDrawing φ d).clausePoints.getD o.1 (0, 0) ∧ (o.2.2, (positiveFormulaDrawing φ d).incidenceRoute o) ∈ List.zip pc.clause pc.routes

    Each actual output occurrence selects its literal and route in the same placed clause.

    source
    theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_literal_indices (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) (j : Fin 22) {l : Logic.PL.Literal (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} {e : LocalIncidence} (he : (l, e) ∈ List.zip (List.getD (profileFormula (clauseProfile c)) ↑j []) (List.filter (fun (e : LocalIncidence) => e.clauseIndex == ↑j) (clauseGeometry φ d i c).incidenceRoutes)) :
    e.variableIndex = List.idxOf l.1 (profileVariables (clauseProfile c))

    Geometry transformations retain the literal-to-variable index of every profile incidence.

    source
    theorem Cslib.Complexity.SAT.ExactOne.positiveClauseBlock_incidence (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) {pc : PositivePlacedClause} (hpc : pc ∈ positiveClauseBlock φ d i c) {l : Logic.PL.Literal (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} {r : Orthogonal.Route} (hlr : (l, r) ∈ List.zip pc.clause pc.routes) :
    ∃ e ∈ (clauseGeometry φ d i c).incidenceRoutes, r = positiveIncidenceRoute φ d i c e ∧ pc.point = positiveBoxOrigin φ d i + (clauseGeometry φ d i c).clausePosition e.clauseIndex ∧ l.1 = profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) c ((profileVariables (clauseProfile c)).getD e.variableIndex (Sum.inl (Sum.inl 0)))

    A paired actual literal and route comes from its certified local incidence record.

    source
    theorem Cslib.Complexity.SAT.ExactOne.positiveFormulaDrawing_incidence (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {o : Logic.PL.Occurrence (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)} (ho : o ∈ Logic.PL.occurrences (Logic.PL.CNF.PositiveExactOneCompile.rawFormula φ)) :
    ∃ (i : ℕ) (hi : i < List.length φ), ∃ e ∈ (clauseGeometry φ d i φ[i]).incidenceRoutes, (positiveFormulaDrawing φ d).incidenceRoute o = positiveIncidenceRoute φ d i φ[i] e ∧ (positiveFormulaDrawing φ d).clausePoints.getD o.1 (0, 0) = positiveBoxOrigin φ d i + (clauseGeometry φ d i φ[i]).clausePosition e.clauseIndex ∧ o.2.2.1 = profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) φ[i] ((profileVariables (clauseProfile φ[i])).getD e.variableIndex (Sum.inl (Sum.inl 0)))

    Every actual output occurrence has a source-clause owner and a certified local route.