Documentation

Complexity.Computability.Complexity.Problems.TwoSAT.Reduction

Unreachability as 2SAT #

An instance I of directed s–t connectivity becomes the formula Cslib.Complexity.TwoSAT.reachabilityFormula I whose variables are the vertices: the unit clauses x_s and ¬x_t, and a clause ¬x_u ∨ x_v for each arc from u to v. In a satisfying assignment every vertex reachable from s is true, so t is not reachable; conversely, making exactly the reachable vertices true satisfies the formula when t is not reachable (Cslib.Complexity.TwoSAT.reachabilityFormula_mem_TwoSAT_iff). This is the reduction from the complement of reachability in the proof that 2SAT is NL-complete Papadimitriou, Theorem 16.3.

The formula is written in logarithmic space by a counter program with output (Cslib.Complexity.TwoSAT.writer), which reads the header of the encoded instance and then the matrix entry by entry, keeping the header values, two vertices and a copy of one of them whose binary digits it writes (Cslib.Complexity.TwoSAT.computableInLogSpace_reachabilityFormula).

Main definitions #

Main results #

References #

source
def Cslib.Complexity.TwoSAT.arc (I : STCONInstance) (u v : ℕ) :
Bool

The arcs of an instance on natural numbers, with no arc outside the vertices.

Instances For
    source
    def Cslib.Complexity.TwoSAT.reachabilityFormula (I : STCONInstance) :
    Logic.PL.CNF ℕ

    The formula of an instance: a variable for each vertex, true when the vertex is reachable from s; the unit clauses x_s and ¬x_t, and the clause ¬x_u ∨ x_v for each arc from u to v, row by row.

    Instances For
      source
      theorem Cslib.Complexity.TwoSAT.mem_reachabilityFormula {I : STCONInstance} {c : Logic.PL.Clause ℕ} :
      c ∈ reachabilityFormula I ↔ c = [(↑I.s, true)] ∨ c = [(↑I.t, false)] ∨ ∃ (u : ℕ) (v : ℕ), arc I u v = true ∧ c = [(u, false), (v, true)]
      source
      theorem Cslib.Complexity.TwoSAT.reachabilityFormula_mem_TwoSAT_iff (I : STCONInstance) :
      reachabilityFormula I ∈ TwoSAT ↔ I ∉ STCON

      The formula is in TwoSAT exactly when t is not reachable from s.

      The writer #

      source
      def Cslib.Complexity.TwoSAT.literalCode (b r : ℕ) (sign : Bool) (exit : ℕ) :
      List Turing.CounterProgram.Instr

      The code writing the literal of register r with the polarity sign, placed at the label b, through register 5, and continuing at exit: the digits of the register, least significant first, each after seven markers, then the fixed end of the literal.

      Instances For
        source
        theorem Cslib.Complexity.TwoSAT.length_literalCode (b r : ℕ) (sign : Bool) (exit : ℕ) :
        (literalCode b r sign exit).length = 23
        source
        theorem Cslib.Complexity.TwoSAT.reachesOut_literalCode {P : Turing.CounterProgram} {w : List Bool} {B b r exit : ℕ} {sign : Bool} (hcode : P.CodeAt b (literalCode b r sign exit)) {regs : List ℕ} (h5 : 5 < regs.length) (hB : ∀ x ∈ regs, x ≤ B) :
        P.ReachesOut w (P.Active B) (b, regs) (exit, regs.set 5 0) (literalBits (regs.getD r 0) sign)

        The code of a literal writes it, through register 5, which ends at 0.

        The encoding of the formula #

        source
        theorem Cslib.Complexity.TwoSAT.encCNF_reachabilityFormula (I : STCONInstance) :
        encCNF (reachabilityFormula I) = literalBits (↑I.s) true ++ [false] ++ (literalBits (↑I.t) false ++ [false] ++ List.flatMap (fun (u : ℕ) => List.flatMap (fun (v : ℕ) => if arc I u v = true then literalBits u false ++ literalBits v true ++ [false] else []) (List.range I.n)) (List.range I.n))

        The encoded formula: the two unit clauses, then the clauses of the arcs row by row.

        The program #

        source
        def Cslib.Complexity.TwoSAT.writer :
        Turing.CounterProgram

        The writer of the encoded formula, on the encoded instance. Registers 0, 1 and 2 receive the header values n, s and t; registers 3 and 4 run over the rows and columns of the matrix; register 5 holds the number whose digits are written. Labels 0 to 5 read the header, labels 6 to 53 write the unit clauses, the nested loops at labels 54 and 57 write the clause of every arc, and label 108 halts.

        Instances For
          source
          theorem Cslib.Complexity.TwoSAT.computableInLogSpace_reachabilityFormula :
          Turing.MultiTapeTM.ComputableInLogSpace reachabilityFormula encSTCON encCNF

          The formula is computed in logarithmic space from the encoded instance.