Maximum satisfiability and separator decomposition of graphs

Resource type
Thesis type
(Thesis) M.Sc.
Date created
2009
Authors/Contributors
Author: Wang, Cong
Abstract
The Satisfiability (SAT) problem asks to find a satisfying assignment to a Boolean formula in CNF, while in its optimization version, MAXSAT, the object is to satisfy the maximum number of clauses. Much effort has been dedicated to design efficient solvers for these problems. In this thesis, we focus on designing algorithms for solving MAX2SAT problem where all clauses contain at most two literals. We use graphs to represent Boolean formulas, and consider problem instances with different structural restrictions. We compare two exact algorithms for MAX2SAT of bounded tree width. Based on our observations, we define a new measure, separator width, which can be less than tree width by up to a logarithmic factor. Moreover, we also design an approximation algorithm using the elimination ordering of variables. We show both experimentally and theoretically that our approximation algorithm works well on a large class of graphs, namely, d-degenerate graphs.
Document
Copyright statement
Copyright is held by the author.
Scholarly level
Language
English
Member of collection
Attachment Size
ETD4655.pdf 433.94 KB