PhD-defence Magnus Wahlström
Title:Algorithms, Measures, and Upper Bounds for Satisfiability and
The topic of exact, exponential-time algorithms for NP-hard problems
has received a lot of attention, particularly with the focus of
producing algorithms with stronger theoretical guarantees, e.g. upper
bounds on the running time on the form O(c^n) for some c. Better
methods of analysis may have an impact not only on these bounds, but
on the nature of the algorithms as well.
The most classic method of analysis of the running time of DPLL-style
("branching" or "backtracking") recursive algorithms consists of
counting the number of variables that the algorithm removes at every
step. Notable improvements include Kullmann's work on complexity
measures, and Eppstein's work on solving multivariate recurrences
through quasiconvex analysis. Still, one limitation that remains
Eppstein's framework is that it is difficult to introduce
(non-trivial) restrictions on the applicability of a possible
We introduce two new kinds of complexity measures, representing two
ways to add such restrictions on applicability to the analysis.
In the first measure, the execution of the algorithm is viewed as
moving between a finite set of states (such as the presence or absence
of certain structures or properties), where the current state decides
which branchings are applicable, and each branch of a branching
contains information about the resultant state. In the second measure,
it is instead the relative sizes of the modelled attributes (such as
the average degree or other concepts of density) that controls the
applicability of branchings.
We adapt both measures to Eppstein's framework, and use these tools to
provide algorithms with stronger bounds for a number of problems.
The problems we treat are satisfiability for sparse formulae, exact
3-satisfiability, 3-hitting set, and counting models for 2- and
3-satisfiability formulae, and in every case the bound we prove is
stronger than previously known bounds.