Documentation

CslibFrontier.Computability.Complexity.Problems.SAT.ExactOne.Geometry

Continuous geometry certificates for exact-one gadgets #

Finite arithmetic checks certify the entire real supports of the fixed gadget routes, including their isolated exterior accesses. These are local replacement certificates; composition with an input drawing is a separate construction.

Main definitions #

Main results #

References #

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

source
def Cslib.Complexity.SAT.ExactOne.LocalGeometry.segmentEndpoints (a b : Orthogonal.Point × Orthogonal.Point) :
List Orthogonal.Point

Common listed endpoints of two segments are the permitted self-contacts.

Instances For
    source
    def Cslib.Complexity.SAT.ExactOne.LocalGeometry.SimpleCheck (r : Orthogonal.Route) :
    Prop

    A decidable finite simplicity certificate for an individual polygonal route.

    Instances For
      source
      @[instance_reducible]
      instance Cslib.Complexity.SAT.ExactOne.LocalGeometry.instDecidableSimpleCheck (r : Orthogonal.Route) :
      Decidable (SimpleCheck r)
      source
      def Cslib.Complexity.SAT.ExactOne.LocalGeometry.Check (g : LocalGeometry) :
      Prop

      The finite certificate refers to graph endpoints, complete routes, and all exterior accesses. The core lies strictly inside the square cell of side g.size.

      Instances For
        source
        @[instance_reducible]
        instance Cslib.Complexity.SAT.ExactOne.LocalGeometry.instDecidableCheck (g : LocalGeometry) :
        Decidable g.Check
        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.isSimple_of_check {r : Orthogonal.Route} (h : SimpleCheck r) :
        Orthogonal.IsSimple r

        The finite simplicity certificate controls full real segment intersections.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.incidence_endpoints {g : LocalGeometry} (h : g.Check) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) :
        e.clauseIndex < g.clausePositions.length ∧ e.variableIndex < g.variablePositions.length ∧ List.head? e.route = some (g.clausePosition e.clauseIndex) ∧ List.getLast? e.route = some (g.variablePosition e.variableIndex)

        Every checked incidence has its prescribed clause and variable endpoints.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.incidence_orthogonal {g : LocalGeometry} (h : g.Check) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) :
        Orthogonal.IsOrthogonal e.route

        Every checked incidence is properly orthogonal.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.incidence_isSimple {g : LocalGeometry} (h : g.Check) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) :
        Orthogonal.IsSimple e.route

        Every checked incidence is simple over its full continuous support.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.routes_contact {g : LocalGeometry} (h : g.Check) {e f : LocalIncidence} (he : e ∈ g.incidenceRoutes) (hf : f ∈ g.incidenceRoutes) (hne : e ≠ f) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support e.route) (hq : p ∈ Orthogonal.support f.route) :
        ∃ q ∈ g.commonEndpoints e f, p = Orthogonal.realPoint q

        Checked incidence routes can meet only at a shared clause or variable vertex.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.variable_not_mem_support {g : LocalGeometry} (h : g.Check) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) {v : Fin g.variablePositions.length} (hv : ↑v ≠ e.variableIndex) :
        Orthogonal.realPoint (g.variablePosition ↑v) ∉ Orthogonal.support e.route

        Checked incidences avoid every nonincident variable vertex.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.clause_not_mem_support {g : LocalGeometry} (h : g.Check) {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) {i : Fin g.clausePositions.length} (hi : ↑i ≠ e.clauseIndex) :
        Orthogonal.realPoint (g.clausePosition ↑i) ∉ Orthogonal.support e.route

        Checked incidences avoid every nonincident clause vertex.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.access_isSimple {g : LocalGeometry} (h : g.Check) (i : Fin g.accessRoutes.length) :
        Orthogonal.IsSimple (g.accessRoutes.getD ↑i [])

        Exterior access routes are simple over their full continuous support.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.access_disjoint {g : LocalGeometry} (h : g.Check) {i j : Fin g.accessRoutes.length} (hne : i ≠ j) :
        Disjoint (Orthogonal.support (g.accessRoutes.getD ↑i [])) (Orthogonal.support (g.accessRoutes.getD ↑j []))

        Distinct checked accesses have disjoint full real supports.

        source
        theorem Cslib.Complexity.SAT.ExactOne.LocalGeometry.access_contact {g : LocalGeometry} (h : g.Check) {i : Fin g.accessRoutes.length} {e : LocalIncidence} (he : e ∈ g.incidenceRoutes) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (g.accessRoutes.getD ↑i [])) (hq : p ∈ Orthogonal.support e.route) :
        e.variableIndex = g.terminalVariables.getD (↑i) 0 ∧ p = Orthogonal.realPoint (g.variablePosition (g.terminalVariables.getD (↑i) 0))

        A checked access meets the core only at its corresponding terminal.

        source
        theorem Cslib.Complexity.SAT.ExactOne.disjunctionGeometry_check :
        disjunctionGeometry.Check

        Complete finite certificate for the parsimonious disjunction replacement.

        source
        theorem Cslib.Complexity.SAT.ExactOne.falseGeometry_check :
        falseGeometry.Check

        Complete finite certificate for the positive forced-false gadget.

        source
        theorem Cslib.Complexity.SAT.ExactOne.complementGeometry_check :
        complementGeometry.Check

        Complete finite certificate for the positive complement gadget.