A note on width-parameterized SAT: An exact machine-model characterization

We characterize the complexity of SAT instances with path-decompositions of width w (n). Although pathwidth is the most restrictive among the studied width-parameterizations of SAT, the most time-efficient algorithms known for such SAT instances run in time 2^{Ω (w (n))}, even when the path-decomposition is given in the input. We wish to better understand the decision complexity of SAT instances of width ω (log n). We provide an exact correspondence between SAT_pw [w (n)], the problem of SAT instances with given path decomposition of width w (n), and NL [r (n)], the class of problems decided by logspace Turing Machines with at most r (n) passes over the nondeterministic tape. In particular, we show that SAT_pw [w (n)] is hard for NL [frac(w (n), log n)] under log-space reductions. When NL [frac(w (n), log n)] is closed under logspace reductions, which is the case for the most interesting w (n)'s, we show that SAT_pw [w (n)] is also complete.