Complexity and algorithms for well-structured k-SAT instances

Konstantinos Georgiou, Periklis A. Papakonstantinou

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Scopus citations

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].

Original languageEnglish (US)
Title of host publicationTheory and Applications of Satisfiability Testing - SAT 2008 - 11th International Conference, SAT 2008, Proceedings
Pages105-118
Number of pages14
DOIs
StatePublished - 2008
Externally publishedYes
Event11th International Conference on Theory and Applications of Satisfiability Testing, SAT 2008 - Guangzhou, China
Duration: May 12 2008May 15 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4996 LNCS

Other

Other11th International Conference on Theory and Applications of Satisfiability Testing, SAT 2008
Country/TerritoryChina
CityGuangzhou
Period5/12/085/15/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Complexity and algorithms for well-structured k-SAT instances'. Together they form a unique fingerprint.

Cite this