Volume 10 (2014) Article 12 pp. 297-339
Width-Parametrized SAT: Time--Space Tradeoffs
Received: August 8, 2012
Revised: July 14, 2013
Published: October 8, 2014
Download article from ToC site:
[PDF (648K)]    [PS (2592K)]    [PS.GZ (703K)]
[Source ZIP]
Keywords: complexity theory, algorithms, complexity classes, circuit complexity, parametrized complexity, nondeterminism, CNF-DNF formulas, Boolean formulas, completeness, time-space tradeoff, treewidth, pathwidth
ACM Classification: F.1.3, F.2.2
AMS Classification: 68Q15, 68Q25

Abstract: [Plain Text Version]

$\newcommand{\tw}{\mathcal{TW}} \newcommand{\eps}{\varepsilon} \newcommand{\etal}{et al.\xspace}$

Alekhnovich and Razborov (2002) presented an algorithm that solves SAT on instances $\phi$ of size $n$ and tree-width $\tw(\phi)$, using time and space bounded by $2^{O(\tw(\phi))}n^{O(1)}$. 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 $3^{\tw(\phi)\log n}n^{O(1)}$, which approaches the run-time of Alekhnovich and Razborov (2002), but has an additional $\log n$ factor in the exponent. Then, we conjecture that this annoying $\log n$ factor is in general unavoidable.

Our negative results show our conjecture true if one believes a well-known complexity assumption, which is the SC $\neq$ 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 $2^{O(\log^k n)}$ (SAC$^1$ when $k=1$). Problems in this class can be solved simultaneously in time-space $(2^{O(\log^{k+1}n)}, O(\log^{k+1}n))$, and also in ($2^{O(\log^k n)}$, $2^{O(\log^k n)}$). 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$^1$ (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 $\varepsilon$ with $0 < \varepsilon <1$, we give an algorithm in time-space $\big( 3^{1.441(1-\varepsilon)\tw(\phi)\log{|\phi|}}|\phi|^{O(1)},\; 2^{2\varepsilon\tw(\phi)}|\phi|^{O(1)} \big)\,.$ 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.
{"ft_lang_label":"__label__en","ft_lang_prob":0.8872091,"math_prob":0.99321675,"size":2771,"snap":"2021-04-2021-17","text_gpt3_token_len":714,"char_repetition_ratio":0.105890855,"word_repetition_ratio":0.0,"special_character_ratio":0.2630819,"punctuation_ratio":0.09090909,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9983662,"pos_list":[0,1,2],"im_url_duplicate_count":[null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-04-19T07:36:31Z\",\"WARC-Record-ID\":\"<urn:uuid:8f267282-e9c5-44ce-8d15-811dd86bb490>\",\"Content-Length\":\"10867\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:1870ac20-a20b-464c-a3ad-3fdaa400dfb6>\",\"WARC-Concurrent-To\":\"<urn:uuid:7d6a20eb-36e6-457e-89fc-1efc3ba4ec7a>\",\"WARC-IP-Address\":\"128.135.164.114\",\"WARC-Target-URI\":\"http://theoryofcomputing.org/articles/v010a012/\",\"WARC-Payload-Digest\":\"sha1:SKJYN7P5RK2GL54KWKAGS6LDDPEKZK4M\",\"WARC-Block-Digest\":\"sha1:2LJDBZJH7F3SWZLOKC62JWICVEAEZMV6\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-17/CC-MAIN-2021-17_segments_1618038878326.67_warc_CC-MAIN-20210419045820-20210419075820-00262.warc.gz\"}"}