liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
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
Counting models for 2sat and 3sat formulae
Linköping University, Department of Computer and Information Science, TCSLAB. Linköping University, The Institute of Technology.
Linköping University, Department of Computer and Information Science, TCSLAB. Linköping University, The Institute of Technology.
Linköping University, Department of Computer and Information Science, TCSLAB. Linköping University, The Institute of Technology.
2005 (English)In: Theoretical Computer Science, ISSN 0304-3975, Vol. 332, no 1-3, 265-291 p.Article in journal (Refereed) Published
Abstract [en]

We here present algorithms for counting models and max-weight models for 2SAT and 3SAT formulae. They use polynomial space and run in O(1.2561n) and O(1.6737n) time, respectively, where n is the number of variables. This is faster than the previously best algorithms for counting non-weighted models for 2SAT and 3SAT, which run in O(1.3247n) and O(1.6894n) time, respectively. In order to prove these time bounds, we develop new measures of formula complexity, allowing us to conveniently analyze the effects of certain factors with a large impact on the total running time. We also provide an algorithm for the restricted case of separable 2SAT formulae, with fast running times for well-studied input classes. For all three algorithms we present interesting applications, such as computing the permanent of sparse 0/1 matrices.

Place, publisher, year, edition, pages
2005. Vol. 332, no 1-3, 265-291 p.
Keyword [en]
Counting models; Satisfiability; Exponential-time algorithms; Exact algorithms; Upper bounds
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-14396DOI: 10.1016/j.tcs.2004.10.037OAI: oai:DiVA.org:liu-14396DiVA: diva2:23417
Available from: 2007-04-16 Created: 2007-04-16 Last updated: 2017-02-23
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. 234 p.
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1079
Keyword
Exact algorithms, upper bounds, algorithm analysis, satisfiability
National Category
Computer Science
Identifiers
urn:nbn:se:liu:diva-8714 (URN)978-91-85715-55-8 (ISBN)
Public defence
2007-04-27, Visionen, B-huset, Linköpings universitet, Linköping, 13:15 (English)
Opponent
Supervisors
Available from: 2007-04-16 Created: 2007-04-16 Last updated: 2014-04-24

Open Access in DiVA

No full text

Other links

Publisher's full textLink to Ph.D. thesis

Authority records BETA

Dahllöf, WilhelmJonsson, PeterWahlström, Magnus

Search in DiVA

By author/editor
Dahllöf, WilhelmJonsson, PeterWahlström, Magnus
By organisation
TCSLABThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 110 hits
CiteExportLink to record
Permanent link

Direct link
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