Abstract
Recent years have seen remarkable progress in propositional satisfiability (SAT). Despite the worst-case exponential run time of all known algorithms, SAT solvers can currently be used to solve hard benchmark problems.
This PhD dissertation contributes to a better understanding of the techniques, the algorithms and the applications of propositional satisfiability. First, we introduce efficient lazy data structures that, though unable to determine exactly the dynamic size of a clause, are quite accurate at predicting the number of unassigned literals in a clause. In addition, we suggest the use of probing-based preprocessing techniques for manipulating propositional formulas. Furthermore, unrestricted backtracking is proposed as an algorithm that combines the advantages of local search and backtrack search. Finally, we relate hardness with hidden structure in unsatisfiable random 3-SAT formulas, where hardness is measured by the search effort and hidden structure is measured by unsatisfiable cores and strong backdoors.