טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentMagid Avi
SubjectStructural Properties of Formulas for which SAT Problem
is Easy
DepartmentDepartment of Quality Assurance and Reliability
Supervisor Professor Emeritus Johann Makowsky
Full Thesis textFull thesis text - English Version


Abstract

The satisfiability (SAT) problem is a core of a large infinite family of computationally intractable NP-complete problems. Since SAT is NP-complete, it is unlikely that any general SAT algorithm has a fast worst-case time behavior. However, it is known that for many cases there is a polynomial time (in the input formula's size) algorithm that solves this problem.

The issue of dealing effectively with the SAT problem is popular in diverse fields due to both the existence of natural SAT encodings for many relevant problems, and the availability of powerful SAT solvers. Such solvers have been successfully used to build tools for planning, knowledge representation, automatic theorem proving and formal verification.

We classify the efficiently solvable classes of SAT into two categories - Clausal properties (e.g. Horn formulas, 2-SAT formulas) and Structural properties (e.g. balanced formulas, formulas of bounded treewidth).

We distinguish between clausal properties and structural properties, in terms of polynomial solvable subsets of formula instances, and explore how we can combine them to obtain a new polynomial solvable subset of formula instances.

We introduce some polynomial solvable classes of SAT known from the literature such as the Horn class, the 2-SAT class, the balanced formulas class and the formulas of a bounded treewidth class. We distinguish between clausal properties and structural properties by using Schaefer dichotomy theorem, and by showing as an example that balanced formulas and formulas of a bounded treewidth are not clausal properties. We examine the relations between some easy classes and between some easy classes and known algorithms for solving SAT such as Eyal Amir and Sheila McIlraith's algorithm and the algorithms for solving SAT of a formula given its backdoor set. We show that the subset of formulas which can be given as a primal graph such that each internal node of its tree decomposition is small and each leaf node is either small or polynomially solvable, is a polynomial solvable class of SAT. We show that by providing a polynomial time algorithm for solving SAT in this case. We also show that the algorithm we provided does not perform well for the subset of formulas which can be given as a primal graph such that each node of its tree decomposition is either small or polynomially solvable. Finally, we provide a polynomial time algorithm for solving SAT for a formula which has a mixed disjoint strong backdoor set of size at most k.