期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2012
卷号：2012
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：A decade has passed since Alekhnovich and Razborov presented an algorithm that solves SAT on instances of size n having tree-width TW() , using time (and space) bounded by 2O(TW())nO(1) . Although there have been several papers over the ensuing years building on the work of Alekhnovich and Razborov there has been no real progress on what they listed as their first open question: Can one ``do anything intelligent in polynomial space to check satisfiability of formulas'' with small tree-width?
We present both positive and negative results on this question; we present a fairly fast polynomial space algorithm, and present complexity-theoretic evidence that no significantly faster algorithm runs in polynomial space.
Our first positive result is a simple algorithm that runs in polynomial space and achieves run-time 3TW()lognnO(1) , nearly
matching the run-time of Aleknovich and Razborov, but with an annoying factor of logn in the exponent.
Our negative results indicate that this annoying factor of logn is unavoidable. For ease of exposition, let us focus on the case where the tree-width is logkn. Then, when k=1 we show that solving SAT instances of tree-width logn is complete for LOGCFL = SAC1, and for arbitrary k, SAT of tree-width logkn is complete for a level of the NSC hierarchy corresponding to log-depth semi-unbounded fan-in circuits of size 2O(logkn). (NSC is the class of problems solvable in nondeterministic polynomial time and poly-logarithmic space: i.e., the nondeterministic analog of the well-known class SC.) Problems in this class can be solved in space logk+1n (and hence in time 2O(logk+1n)), and also in time 2O(logkn) (with space bound the same as the time bound).
These results show that our conjecture (that the annoying factor of logn in the exponent of the running time of our polynomial-space algorithm cannot be eliminated) 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, possibly with different resource bounds depending on k, of the long-standing conjecture in complexity theory that SAC1 (and even its subclass NL) is not contained in SC, or even in the Time-Space class TISP(nO(1)2log1−n) .
The most involved part of this paper is the demonstration that the best-known time-efficient and space-efficient algorithms for small tree-width SAT can be combined using a new technique to obtain, for each with 01, an algorithm with time-space complexity 31441(1−)TW()logO(1) 22TW()O(1) . 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.
