Abstract
This paper consists of two conceptually related but independent parts. In the first part we initiate the study of k-SAT instances of bounded diameter. The diameter of an ordered CNF formula is defined as the maximum difference between the index of the first and the last occurrence of a variable. We investigate the relation between the diameter of a formula and the tree-width and the path-width of its corresponding incidence graph. We show that under highly parallel and efficient transformations, diameter and path-width are equal up to a constant factor. Our main result is that the computational complexity of SAT, Max-SAT, #SAT grows smoothly with the diameter (as a function of the number of variables). Our focus is in providing space efficient and highly parallel algorithms, while the running time of our algorithms matches previously known results. Our results refer to any diameter, whereas for the special case where the diameter is O(logn) we show NL-completeness of SAT and NC2 algorithms for Max-SAT and #SAT.
In the second part we deal directly with k-CNF formulas of bounded tree-width. We describe algorithms in an intuitive but not-so-standard model of computation. Then we apply constructive theorems from computational complexity to obtain deterministic time-efficient and simultaneously space-efficient algorithms for k-SAT as asked by Alekhnovich and Razborov [1].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alekhnovich, A., Razborov, A.: Satisfiability, branch-width and Tseitin tautologies. In: FOCS, pp. 593–603 (2002)
Amir, E., Mcilraith, S.: Solving satisfiability using decomposition and the most constrained subproblem. In: LICS workshop on Theory and Applications of Satisfiability Testing. Electronic Notes in Discrete Mathematics (2001)
Arora, S., Safra, S.: Probabilistic checking of proofs: A new characterization of NP. J. ACM 45, 70–122 (1998)
Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for #SAT and bayesian inference. In: FOCS, pp. 340–351 (2003)
Bodlaender, H.L.: A tourist guide through treewidth. Acta Cybernet 11(1-2), 1–21 (1993)
Bodlaender, H.L., Gilbert, J.R., Hafsteinsson, H., Kloks, T.: Approximating treewidth, pathwidth, frontsize, and shortest elimination tree. J. Algorithms 18(2), 238–255 (1995)
Chinn, P.Z., Chvátalová, J., Dewdney, A.K., Gibbs, N.E.: The bandwidth problem for graphs and matrices - A survey. J. Graph Theory 6(3), 223–254 (1982)
Cook, S.A.: Characterizations of pushdown machines in terms of time-bounded computers. J. ACM 18(1), 4–18 (1971)
Cook, S.A.: The complexity of theorem-proving procedures. In: STOC, pp. 151–158 (1971)
Courcelle, B., Makowsky, J.A., Rotics, U.: On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discrete Appl. Math. 108(1-2), 23–52 (2001)
Du, D.-Z., Ko, K.-I.: Theory of Computational Complexity. Wiley-Interscience, New York (2000)
Feige, U.: Approximating the bandwidth via volume respecting embeddings. J. Comput. Syst. Sci 60(3), 510–539 (2000)
Fischer, E., Makowsky, J.A., Ravve, E.R.: Counting truth assignments of formulas of bounded tree-width or clique-width. Discrete Appl. Math. 155(14), 1885–1893 (2007)
Flouris, M., Lau, L.C., Morioka, T., Papakonstantinou, P.A., Penn, G.: Bounded and ordered satisfiability: connecting recognition with Lambek-style calculi to classical satisfiability testing. In: Math. of language 8, pp. 45–56 (2003)
Garey, M.R., Graham, R.L., Johnson, D.S., Knuth, D.E.: Complexity results for bandwidth minimization. SIAM J. Appl. Math. 34(3), 477–495 (1978)
Gottlob, G., Scarcello, F., Sideri, M.: Fixed-parameter complexity in AI and nonmonotonic reasoning. Artificial Intelligence 138(1–2), 55–86 (2002)
Hlineny, P., Oum, S., Seese, D., Gottlob, G.: Width parameters beyond tree-width and their applications. The Computer Journal 8, 216–235 (2007)
Khanna, S., Motwani, R.: Towards a syntactic characterization of PTAS. In: STOC, pp. 329–337. ACM, New York (1996)
Lipton, R.J., Tarjan, R.E.: Applications of a planar separator theorem. SIAM J. of Comp. 9(3), 615–627 (1980)
Nishimura, N., Ragde, P., Szeider, S.: Solving #SAT using vertex covers. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 396–409. Springer, Heidelberg (2006)
Oum, S., Seymour, P.: Approximating clique-width and branch-width. J. Combin. Theory Ser. B 96(4), 514–528 (2006)
Papadimitriou, C.H.: The NP-completeness of the bandwidth minimization problem. Computing 16(3), 263–270 (1976)
Papakonstantinou, P.A., Penn, G., Vahlis, Y.: Polynomial-time and parallel algorithms for fragments of Lambek Grammars (unpublished manuscript)
Robertson, N., Seymour, P.D.: Graph minors I. Excluding a forest. J. of Comb. Theory (Ser. B) 35, 39–61 (1983)
Robertson, N., Seymour, P.D.: Graph minors. II. algorithmic aspects of tree-width. J. of Algorithms 7, 309–322 (1986)
Ruzzo, W.L.: On uniform circuit complexity. J. Comput. System Sci. 22(3), 365–383 (1981) Special issue dedicated to Michael Machtey
Samer, M., Szeider, S.: A fixed-parameter algorithm for #SAT with parameter incidence treewidth. CoRR, abs/cs/061017 (2006) informal publication
Samer, M., Szeider, S.: Algorithms for propositional model counting. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 484–498. Springer, Heidelberg (2007)
Smithline, L.: Bandwidth of the complete k-ary tree. Discrete Math. 142(1-3), 203–212 (1995)
Sudborough, I.H.: On the tape complexity of deterministic context-free languages. J. Assoc. Comput. Mach. 25(3), 405–414 (1978)
Szeider, S.: On fixed-parameter tractable parameterizations of SAT. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 188–202. Springer, Heidelberg (2004)
Valiant, L.G.: The complexity of computing the permanent. Theoret. Comput. Sci. 8(2), 189–201 (1979)
Valiant, L.G., Skyum, S., Berkowitz, S., Rackoff, C.: Fast parallel computation of polynomials using few processors. SIAM J. Comput. 12(4), 641–644 (1983)
Vollmer, H.: Introduction to Circuit Complexity - A Uniform Approach. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Georgiou, K., Papakonstantinou, P.A. (2008). Complexity and Algorithms for Well-Structured k-SAT Instances. In: Kleine Büning, H., Zhao, X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79719-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-79719-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79718-0
Online ISBN: 978-3-540-79719-7
eBook Packages: Computer ScienceComputer Science (R0)