Widthparameterized SAT: TimeSpace Tradeoffs
AbstractWidth parameterizations of SAT, such as treewidth and pathwidth, enable the study of computationally more tractable and practical SAT instances. We give two simple algorithms, one that runs simultaneously in timespace (O^{*}(2^{2tw(φ)}), O^{*}(2^{tw(φ)}) and another that runs in timespace (O^{*}(3^{tw(φ) log φ}),φ^{O(1)}), where tw(φ) is the treewidth of a formula φ with φ many clauses and variables. This partially answers the question of Alekhnovitch and Razborov, who also gave algorithms exponential both in time and space, and asked whether the space can be made smaller. We conjecture that every algorithm for this problem that runs in time 2^{tw(φ) o(log φ)} necessarily blows up the space to exponential in tw(φ). We introduce a novel way to combine the two simple algorithms that allows us to trade constant factors in the exponents between running time and space. Our technique gives rise to a family of algorithms controlled by two parameters. By fixing one parameter we obtain an algorithm that runs in timespace (O^{*}(3^{1.441(1ε) tw(φ) log φ}), O^{*}(2^{2ε tw(φ)}}), for every 0<ε<1. We systematically study the limitations of this technique, and show that these algorithmic results are the best achievable using this technique. We also study further the computational complexity of width parameterizations of SAT. We prove nonsparsification lower bounds for formulas of pathwidth ω(log φ), and a separation between the complexity of pathwidth and treewidth parametrized SAT modulo plausible complexity assumptions. Joint work with Eric Allender, Shiteng Chen, Tiancheng Lou, and Periklis Papakonstantinou.
