Fixed parameter algorithms for satisfiability testing

Fixed-parameter algorithms are a methodology of coping with NP-hardness requiring in addition to the input size $n$ an additional parameter $k$ to be known. The resulting runtime is of the form $f(k) n^c$ where $f(k)$ is normally an exponential function of $k$ and $c$ is a constant not dependent on $k$. The crucial assumption of this methodology is that $k$ is very small compared to $n$. In this case, the hope is that $f(k)$ is small as well and can be considered as a negligible constant. As a result we have an illusion of a polynomial time algorithm solving an NP-hard problem. Problems that can be solved the above way are called fixed-parameter tractable (FPT).

The topic of this talk is fixed-parameter algorithms for satisfiability testing (SAT problem). The talk consists of two main parts. In the first part I will consider a standard setting of the SAT problem, where we are given a CNF at the input and asked to find a satisfying truth assignment to its variables or to report that there is no such truth assignment. A well known way to solve the SAT problem in this setting is to identify a small *backdoor set*, i.e. a set of variables whose assignment makes the residual formula belong to a certain polynomially solvable class. Thus, instead of doing brute-force search on all the variables, this is done only to the variables of the backdoor set. Clearly, we want the backdoor set to be as small as possible. However, this is not an easy task: finding an optimal backdoor set w.r.t. to most polynomially solvable classes of the SAT problem is NP-hard. This is where fixed-parameter algorithms can be applied with the parameter being the size of the resulting backdoor set. I will overview the state of the art of the fixed-parameter computation of small backdoor sets and practical applicability of the existing algorithms.

In the second part of my talk I will consider the setting of SAT problem where the formula is known in advance and the input is a query, e.g. 'Is there a satisfying assignment with a subset $S_1$ of variables set to true and a subset $S_2$ of variables set to false?' This setting has real-world applications related to configuration and verification tasks. The main difficulty is that in these applications the queries have to be answered efficiently. To implement this requirement, the formula is precompiled in the *off-line* phase into a representation that, roughly speaking, explicitly stores all its satisfying assignments, thus allowing the queries to be answered in a polynomial time. The runtime of the off-line preprocessing does not matter, the important requirement is that the resulting representation is space-efficient. The study of such representations is called *knowledge compilation*. In this talk I will overview one particular representation formalism called Decomposable Negation Normal Form (DNNF) whose space complexity is linear in terms of the input size but exponential in terms of the treewidth of the formula.

The talk is designed for audience unfamiliar with the area of parameterized complexity. To make the talk self-contained, I will introduce all the required background in the first 8-10 minutes of the talk.