Return to search

Exact Algorithms for Exact Satisfiability Problems

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.

Identiferoai:union.ndltd.org:UPSALLA1/oai:DiVA.org:liu-6907
Date January 2006
CreatorsDahllöf, Vilhelm
PublisherLinköpings universitet, TCSLAB, Linköpings universitet, Tekniska högskolan, Institutionen för datavetenskap
Source SetsDiVA Archive at Upsalla University
LanguageEnglish
Detected LanguageEnglish
TypeDoctoral thesis, monograph, info:eu-repo/semantics/doctoralThesis, text
Formatapplication/pdf
Rightsinfo:eu-repo/semantics/openAccess
RelationLinköping Studies in Science and Technology. Dissertations, 0345-7524 ; 1013

Page generated in 0.002 seconds