liu.seSearch for publications in DiVA
Change search

Cite
Citation style
• apa
• harvard1
• ieee
• modern-language-association-8th-edition
• vancouver
• oxford
• Other style
More styles
Language
• de-DE
• en-GB
• en-US
• fi-FI
• nn-NO
• nn-NB
• sv-SE
• Other locale
More languages
Output format
• html
• text
• asciidoc
• rtf
An algorithm for the sat problem for formulae of linear length
Linköping University, Department of Computer and Information Science, TCSLAB - Theoretical Computer Science Laboratory. Linköping University, The Institute of Technology.
2005 (English)In: Algorithms – ESA 2005: 13th Annual European Symposium, Palma de Mallorca, Spain, October 3-6, 2005. / [ed] Gerth S. Brodal and Stefano Leonardi, Berlin/Heidelberg: Springer , 2005, Vol. 3669, p. 107-118Conference paper, Published paper (Other academic)
##### Abstract [en]

We present an algorithm that decides the satisfiability of a CNF formula where every variable occurs at most k times in time O(2N(1&#x2212;c/(k+1)+O(1/k2)))" role="presentation" style="box-sizing: border-box; display: inline; line-height: normal; letter-spacing: normal; word-spacing: normal; word-wrap: normal; white-space: nowrap; float: none; direction: ltr; max-width: none; max-height: none; min-width: 0px; min-height: 0px; border: 0px; padding: 0px; margin: 0px; position: relative;">O(2N(1−c/(k+1)+O(1/k2)))O(2N(1−c/(k+1)+O(1/k2))) for some c (that is, O(α N ) with α< 2 for every fixed k). For k ≤ 4, the results coincide with an earlier paper where we achieved running times of O(20.1736 N ) for k = 3 and O(20.3472N ) for k = 4 (for k ≤ 2, the problem is solvable in polynomial time). For k>4, these results are the best yet, with running times of O(20.4629N ) for k = 5 and O(20.5408N ) for k = 6. As a consequence of this, the same algorithm is shown to run in time O(20.0926L ) for a formula of length (i.e.total number of literals) L. The previously best bound in terms of L is O(20.1030L ). Our bound is also the best upper bound for an exact algorithm for a 3satformula with up to six occurrences per variable, and a 4sat formula with up to eight occurrences per variable.

##### Place, publisher, year, edition, pages
Berlin/Heidelberg: Springer , 2005. Vol. 3669, p. 107-118
##### Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 3669
##### National Category
Engineering and Technology
##### Identifiers
DOI: 10.1007/11561071ISBN: 978-3-540-29118-3 (print)OAI: oai:DiVA.org:liu-14398DiVA, id: diva2:23419
##### Conference
13th Annual European Symposium, Palma de Mallorca, Spain, October 3-6, 2005.
Available from: 2007-04-16 Created: 2007-04-16 Last updated: 2018-02-02
##### In thesis
1. Algorithms, measures and upper bounds for satisfiability and related problems
Open this publication in new window or tab >>Algorithms, measures and upper bounds for satisfiability and related problems
2007 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

The topic of exact, exponential-time algorithms for NP-hard problems has received a lot of attention, particularly with the focus of producing algorithms with stronger theoretical guarantees, e.g. upper bounds on the running time on the form O(c^n) for some c. Better methods of analysis may have an impact not only on these bounds, but on the nature of the algorithms as well.

The most classic method of analysis of the running time of DPLL-style ("branching" or "backtracking") recursive algorithms consists of counting the number of variables that the algorithm removes at every step. Notable improvements include Kullmann's work on complexity measures, and Eppstein's work on solving multivariate recurrences through quasiconvex analysis. Still, one limitation that remains in Eppstein's framework is that it is difficult to introduce (non-trivial) restrictions on the applicability of a possible recursion.

We introduce two new kinds of complexity measures, representing two ways to add such restrictions on applicability to the analysis. In the first measure, the execution of the algorithm is viewed as moving between a finite set of states (such as the presence or absence of certain structures or properties), where the current state decides which branchings are applicable, and each branch of a branching contains information about the resultant state. In the second measure, it is instead the relative sizes of the modelled attributes (such as the average degree or other concepts of density) that controls the applicability of branchings.

We adapt both measures to Eppstein's framework, and use these tools to provide algorithms with stronger bounds for a number of problems. The problems we treat are satisfiability for sparse formulae, exact 3-satisfiability, 3-hitting set, and counting models for 2- and 3-satisfiability formulae, and in every case the bound we prove is stronger than previously known bounds.

##### Place, publisher, year, edition, pages
Linköping, Sweden: Department of Computer and Information Science, Linköpings universitet, 2007. p. 234
##### Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1079
##### Keywords
Exact algorithms, upper bounds, algorithm analysis, satisfiability
##### National Category
Computer Sciences
##### Identifiers
urn:nbn:se:liu:diva-8714 (URN)978-91-85715-55-8 (ISBN)
##### Supervisors
Available from: 2007-04-16 Created: 2007-04-16 Last updated: 2018-01-13

#### Open Access in DiVA

No full text in DiVA

Publisher's full textLink to Ph.D. thesis

#### Authority records BETA

Wahlström, Magnus

#### Search in DiVA

##### By author/editor
Wahlström, Magnus
##### By organisation
TCSLAB - Theoretical Computer Science LaboratoryThe Institute of Technology
##### On the subject
Engineering and Technology

doi
isbn
urn-nbn

#### Altmetric score

doi
isbn
urn-nbn
Total: 59 hits

Cite
Citation style
• apa
• harvard1
• ieee
• modern-language-association-8th-edition
• vancouver
• oxford
• Other style
More styles
Language
• de-DE
• en-GB
• en-US
• fi-FI
• nn-NO
• nn-NB
• sv-SE
• Other locale
More languages
Output format
• html
• text
• asciidoc
• rtf