| The subject of this dissertation belongs to the area known as classical Propositional Satisfiability. The Propositional Satisfiability Problem (SAT) is the problem of determining whether a propositional formula has a model, that is a truth-value assignment to propositional variables under which the formula evaluates to true. In this dissertation I propose a number of novel methods for solving instances of SAT, and confirm their effectiveness empirically. At the core of the proposed methods are the following observations.;Traditionally, methods for solving SAT in industrial applications are based on the variation of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. An alternative paradigm for solving SAT, the Stochastic Local Search (SLS), has a number of known advantages over the DPLL, and is more effective in certain domains. However, SLS-based methods have been largely disregarded in the industrial applications of SAT, due to their presumed weakness in this domain. In this dissertation, I present evidence that SLS-based methods, when given access to the structure of the underlying problems, can be used for effective solving of SAT in the industrial setting.;The results reported in this dissertation indicate that SLS methods for non-clausal and circuit SAT promise powerful tools in the field of Propositional Satisfiability. This dissertation is a contribution to the study of structural satisfiability - the study of the theory and the applications of structure-based approaches to Propositional Satisfiability.;Instances of SAT are often represented in the form of propositional formulas, or Boolean circuits. While these representations posses vast amount of structure, traditional methods for solving SAT convert the input to a certain normal form (Conjunctive Normal Form, CNF), and, as a result, loose a large amount of this structural information. In this dissertation I propose methods that work directly on the formula or the Boolean circuit representations of SAT, and, therefore, are capable of using the structural information more effectively. I demonstrate empirically, that the structure can be used to significantly accelerate the search for solutions to SAT in the industrial domain. |
