Directed s–t connectivity is NL-complete

Directed s–t connectivity on adjacency matrices (Cslib.Complexity.STCON, encoded by Cslib.Complexity.encSTCON) is complete for nondeterministic logarithmic space under logspace many-one reductions Sipser, Theorem 8.25 (Cslib.Complexity.STCON.logSpaceComplete). The classes are the library's native ones: NL is decided by one finite-state nondeterministic machine within work space c * (Nat.log2 n + 1), every branch halting, and the reductions are computed by deterministic machines within such space (Cslib.Complexity.LogSpaceReducible).

• Membership (Cslib.Complexity.STCON.mem_NL) Sipser, Example 8.19: a nondeterministic counter program walks from s, guessing one vertex at a time and giving up after n steps (Cslib.Complexity.STCON.searchProgram).
• Hardness (Cslib.Complexity.STCON.logSpaceHard): a problem decided by a machine within space c * (Nat.log2 n + 1) reduces to STCON by mapping an instance to the configuration graph of the machine on its encoding, with a sink after the accepting vertices (Cslib.Complexity.STCON.configurationInstance), computed in logarithmic space by a counter program (Cslib.Complexity.STCON.computableInLogSpace_configurationInstance).

The complement of STCON is in NL too (Cslib.Complexity.STCON.compl_mem_NL) by the Immerman–Szelepcsényi theorem Cslib.Complexity.NL_eq_coNL Sipser, Section 8.6, proved for these native classes by Erik Demaine's inductive-counting construction. Consequently the complement is NL-complete as well (Cslib.Complexity.STCON.compl_logSpaceComplete), the form in which the hardness of 2SAT is usually derived. Finally STCON is in L exactly when NL = L (Cslib.Complexity.STCON.mem_L_iff_forall_NL_eq_L) Sipser, Corollary 8.24.

Main results

• Cslib.Complexity.STCON.mem_NL: STCON ∈ NL.
• Cslib.Complexity.STCON.logSpaceReducible_of_mem_NL, Cslib.Complexity.STCON.logSpaceHard: every problem in NL reduces to STCON in logarithmic space.
• Cslib.Complexity.STCON.logSpaceComplete: STCON is NL-complete.
• Cslib.Complexity.STCON.compl_mem_NL: the complement of STCON is in NL.
• Cslib.Complexity.STCON.compl_logSpaceComplete: the complement of STCON is NL-complete.
• Cslib.Complexity.STCON.mem_L_iff_forall_NL_eq_L: STCON ∈ L exactly when NL = L.

References

• M. Sipser, Introduction to the Theory of Computation, Example 8.19, Corollary 8.24, Theorem 8.25 and Section 8.6
• N. Immerman, Nondeterministic Space Is Closed under Complementation
• R. Szelepcsényi, The Method of Forcing for Nondeterministic Automata

theorem Cslib.Complexity.STCON.mem_NL : STCON ∈ NL encSTCON

Directed s–t connectivity is in NL Sipser, Example 8.19.

theorem Cslib.Complexity.STCON.logSpaceReducible_of_mem_NL {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ NL enc) : LogSpaceReducible enc encSTCON A STCON

Every problem in NL reduces to directed s–t connectivity in logarithmic space: an instance is mapped to the configuration graph of a logarithmic-space decider on its encoding, with a sink after the accepting vertices Sipser, Theorem 8.25.

theorem Cslib.Complexity.STCON.logSpaceHard : LogSpaceHard (fun {α : Type} => NL) encSTCON STCON

Directed s–t connectivity is NL-hard under logspace many-one reductions.

theorem Cslib.Complexity.STCON.logSpaceComplete : LogSpaceComplete (fun {α : Type} => NL) encSTCON STCON

Directed s–t connectivity is NL-complete under logspace many-one reductions Sipser, Theorem 8.25.

theorem Cslib.Complexity.STCON.compl_mem_NL : STCONᶜ ∈ NL encSTCON

The complement of directed s–t connectivity is in NL, by the Immerman–Szelepcsényi theorem NL = coNL Sipser, Section 8.6.

theorem Cslib.Complexity.STCON.compl_logSpaceComplete : LogSpaceComplete (fun {α : Type} => NL) encSTCON STCONᶜ

The complement of directed s–t connectivity is NL-complete: a problem in NL has its complement in NL, which reduces to STCON. This combines Theorem 8.25 of Sipser with NL = coNL Sipser, Section 8.6.

theorem Cslib.Complexity.STCON.mem_L_iff_forall_NL_eq_L : STCON ∈ L encSTCON ↔ ∀ {α : Type} (enc : α ↪ List Bool), NL enc = L enc

Directed s–t connectivity is in L exactly when NL = L, for every encoding of instances Sipser, Corollary 8.24.