Maximum satisfiability and separator decomposition of graphs

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.