Documentation

Complexity.Computability.PCP.Encoded.AddTrivial

Adding trivial edges to encoded constraint graphs #

Adding universally accepting constraints is a step of Dinur's preprocessing. These programs append supplied edges or construct a loop at every vertex. Their interpretation is exactly the existing union of constraint graphs, with its proved satisfiability and value laws.

Main definitions #

Main results #

References #

source
def Cslib.PCP.Encoded.Graph.addTrivial {C : Type} (truth : C) (g : Graph C) (extra : List (ℕ × ℕ)) :
Graph C

Append edges carrying a specified constraint descriptor. In applications truth is a constraint that accepts every pair of labels.

Instances For
    source
    def Cslib.PCP.Encoded.Graph.addLoops {C : Type} (truth : C) (g : Graph C) :
    Graph C

    Add one edge with constraint truth from each declared vertex to itself.

    Instances For
      source
      theorem Cslib.PCP.Encoded.Graph.isPolyTime_addTrivial {C : Type} (enc : C ↪ List Bool) (truth : C) :
      Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : Graph C × List (ℕ × ℕ)) => addTrivial truth p.1 p.2) (Turing.MultiTapeTM.encPair (encoding enc) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary))) (encoding enc)

      Appending explicitly listed trivial edges is uniformly polynomial-time in both lists.

      source
      theorem Cslib.PCP.Encoded.Graph.isPolyTime_addLoops {C : Type} (enc : C ↪ List Bool) (truth : C) :
      Turing.MultiTapeTM.ComputableTidilyInPolyTime (addLoops truth) (encoding enc) (encoding enc)

      Constructing all self-loops, including enumerating their endpoints, is polynomial-time.

      source
      @[simp]
      theorem Cslib.PCP.Encoded.Graph.length_edges_addTrivial {C : Type} (truth : C) (g : Graph C) (extra : List (ℕ × ℕ)) :
      (addTrivial truth g extra).edges.length = g.edges.length + extra.length

      An appended edge list has the declared number of old and new edges.

      source
      @[simp]
      theorem Cslib.PCP.Encoded.Graph.length_edges_addLoops {C : Type} (truth : C) (g : Graph C) :
      (addLoops truth g).edges.length = g.edges.length + g.vertices

      Adding one self-loop per declared vertex adds exactly that many edges.

      source
      theorem Cslib.PCP.Encoded.Graph.WellFormed.addTrivial {C : Type} {g : Graph C} (hg : g.WellFormed) (truth : C) {extra : List (ℕ × ℕ)} (hextra : ∀ p ∈ extra, p.1 < g.vertices ∧ p.2 < g.vertices) :
      (Graph.addTrivial truth g extra).WellFormed

      Adding edges within the declared vertex set preserves well-formedness.

      source
      theorem Cslib.PCP.Encoded.Graph.WellFormed.addLoops {C : Type} {g : Graph C} (hg : g.WellFormed) (truth : C) :
      (Graph.addLoops truth g).WellFormed

      Self-loops stay in the declared vertex set, including when it is empty.

      source
      def Cslib.PCP.Encoded.Graph.appendEdgeEquiv {C : Type} (left right : List (Edge C)) :
      Fin left.length ⊕ Fin right.length ≃ Fin (left ++ right).length

      The ordered concatenation of edge lists numbers their disjoint union.

      Instances For
        source
        theorem Cslib.PCP.Encoded.Graph.toGraph_append {C α : Type} (vertices : ℕ) (left right : List (Edge C)) (eval : C → α → α → Bool) :
        ({ vertices := vertices, edges := left ++ right }.toGraph eval).comap ⇑(appendEdgeEquiv left right) = ({ vertices := vertices, edges := left }.toGraph eval).union ({ vertices := vertices, edges := right }.toGraph eval)

        Appending edge records interprets as the union of the corresponding constraint graphs, with the canonical enumeration of their disjoint edge sets.

        source
        theorem Cslib.PCP.Encoded.Graph.satisfiable_addTrivial_iff {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (truth : C) (htruth : ∀ (a b : α), eval truth a b = true) (extra : List (ℕ × ℕ)) :
        ((addTrivial truth g extra).toGraph eval).Satisfiable ↔ (g.toGraph eval).Satisfiable

        Appending universally accepting constraints preserves satisfiability.

        source
        theorem Cslib.PCP.Encoded.Graph.unsatVal_addTrivial {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (truth : C) (htruth : ∀ (a b : α), eval truth a b = true) (extra : List (ℕ × ℕ)) :
        ((addTrivial truth g extra).toGraph eval).unsatVal = ↑g.edges.length / (↑g.edges.length + ↑extra.length) * (g.toGraph eval).unsatVal

        Appending universally accepting constraints scales the value by the fraction of original edges. This also covers empty input and output edge sets.

        source
        theorem Cslib.PCP.Encoded.Graph.satisfiable_addLoops_iff {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (truth : C) (htruth : ∀ (a b : α), eval truth a b = true) :
        ((addLoops truth g).toGraph eval).Satisfiable ↔ (g.toGraph eval).Satisfiable

        Adding universally accepting self-loops preserves satisfiability.

        source
        theorem Cslib.PCP.Encoded.Graph.unsatVal_addLoops {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (truth : C) (htruth : ∀ (a b : α), eval truth a b = true) :
        ((addLoops truth g).toGraph eval).unsatVal = ↑g.edges.length / (↑g.edges.length + ↑g.vertices) * (g.toGraph eval).unsatVal

        Adding one universally accepting self-loop per vertex scales the value by the fraction of original edges.