Width-Parameterized SAT: Time-space tradeoffs

Alekhnovich and Razborov (2002) presented an algorithm that solves SAT on instances φ of size n and tree-width TW(φ), using time and space bounded by (Formula Presented). Although several follow-up works appeared over the last decade, the first open question of Alekhnovich and Razborov remained essentially unresolved: Can one check satisfiability of formulas with small tree-width in polynomial space and time as above? We essentially resolve this question, by (1) giving a polynomial space algorithm with a slightly worse run-time, (2) providing a complexity-theoretic characterization of bounded tree-width SAT, which strongly suggests that no polynomial-space algorithm can run significantly faster, and (3) presenting a spectrum of algorithms trading off time for space, between our PSPACE algorithm and the fastest known algorithm. First, we give a simple algorithm that runs in polynomial space and achieves run-time (Formula Presented), which approaches the run-time of Alekhnovich and Razborov (2002), but has an additional logn factor in the exponent. Then, we conjecture that this annoying logn factor is in general unavoidable. Our negative results show our conjecture true if one believes a well-known complexity assumption, which is the SC ≠ NC conjecture and its scaled variants. Technically, we base our result on the following lemma. For arbitrary k, SAT of tree-width log^k n is complete for the class of problems computed by circuits of logarithmic depth, semi-unbounded fan-in and size (Formula Presented). Problems in this class can be solved simultaneously in time-space (Formula Presented), and also in (Formula Presented). Then, we show that our conjecture (for SAT instances with poly-log tree-width) is equivalent to the question of whether the small-space simulation of semi-unbounded circuit classes can be sped up without incurring a large space penalty. This is a recasting of the conjecture that SAC¹ (and even its subclass NL) is not contained in SC. Although we cannot hope for an improvement asymptotically in the exponent of time and space, we introduce a new algorithmic technique which trades constants in the exponents: for each e with 0 < e < 1, we give an algorithm in time-space (Formula Presented) We systematically study the limitations of our technique for trading off time and space, and we show that our bounds are the best achievable using this technique.