SAT approach for decomposition methods

Abstract

We are always trying to nd the best way to solve any computational problem. But, sometimes the most natural way to solve a given problem may not be very practical. Computer scientists have been trying to nd practical ways for solving hard problems. One of the major technology, that was developed to solve hard problems, is decompositions. Decompositions allow one to decompose a given problem instance in small parts. There are various techniques that use decompositions to solve a problem, but these techniques rely heavily on the quality of the decompositions. In this thesis, we develop SAT-based techniques to nd \good" decompositions. Satis ability (SAT) is one of the most central problem in computer science and SAT-solvers, tools that can solve this problem, have improved drastically over the last years. Current SAT-solvers can solve some SAT instances, of several MB in size, in a matter of milliseconds. A SAT- encoding is the transformation of a computational problem to SAT. We make use of the speed and eciency of the SAT based techniques for nding good decompositions. In this thesis we develop SAT-encodings for nding good decompositions. One of the major hurdle for SAT-encodings is the size of the SAT formula. Most of the SAT-encodings are at least cubic is the size of problem instance, which puts a hard limit on the size of the problem instance that can be solved. We overcome this restriction by developing a new SAT-based local improvement technique, where given a decomposition we try to improve parts of it using SAT-encodings. We propose a new characterization for branch decompositions and used it for a SAT-encoding for nding branchwidth. We develop local improvement approach for nding better branch decompositions, which we later used for tree decompositions as well. We develop two dierent characterizations for special tree decomposition and path decomposition, and compare them empirically. We also develop an SMT-encoding for nding fractional hypertree decompositions.