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
Exact Algorithms for Exact Satisfiability Problems
Linköping University, Department of Computer and Information Science, TCSLAB. Linköping University, The Institute of Technology.
2006 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

This thesis presents exact means to solve a family of NP-hard problems. Starting with the well-studied Exact Satisfiability problem (XSAT) parents, siblings and daughters are derived and studied, each with interesting practical and theoretical properties. While developing exact algorithms to solve the problems, we gain new insights into their structure and mutual similarities and differences.

Given a Boolean formula in CNF, the XSAT problem asks for an assignment to the variables such that each clause contains exactly one true literal. For this problem we present an O(1.1730n) time algorithm, where n is the number of variables. XSAT is a special case of the General Exact Satisfiability problem which asks for an assignment such that in each clause exactly i literals be true. For this problem we present an algorithm which runs in O(2(1-ε) n) time, with 0 < ε < 1 for every fixed i; for i=2, 3 and 4 we have running times in O(1.4511n), O(1.6214n) and O(1.6848n) respectively.

For the counting problems we present an O(1.2190n) time algorithm which counts the number of models for an XSAT instance. We also present algorithms for #2SATw and #3SATw, two well studied Boolean problems. The algorithms have running times in O(1.2561n) and O(1.6737n) respectively.

Finally we study optimisation problems: As a variant of the Maximum Exact Satisfiability problem, consider the problem of finding an assignment exactly satisfying a maximum number of clauses while the rest are left with no true literal. This problem is reducible to #2SATw without the addition of new variables and thus is solvable in time O(1.2561n). Another interesting optimisation problem is to find two XSAT models which differ in as many variables as possible. This problem is shown to be solvable in O(1.8348n) time.

Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2006. , 177 p.
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1013
Keyword [en]
NP-hardness, exact algorithms, satisfiability, exact satisfiability
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-6907ISBN: 91-85523-97-6 (print)OAI: oai:DiVA.org:liu-6907DiVA: diva2:22042
Public defence
2006-06-01, Visionen, Hus B, Campus Valla, Linköpings universitet, Linköping, 13:15 (English)
Opponent
Supervisors
Available from: 2006-06-21 Created: 2006-06-21

Open Access in DiVA

fulltext(946 kB)1546 downloads
File information
File name FULLTEXT01.pdfFile size 946 kBChecksum SHA-1
1292b151f81ac63fa8e93d365f2b878f6d2495fb30a234cd1acd1f79ea6403afcaf59a92
Type fulltextMimetype application/pdf

Authority records BETA

Dahllöf, Vilhelm

Search in DiVA

By author/editor
Dahllöf, Vilhelm
By organisation
TCSLABThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 1546 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1586 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