We present a list of parameterized problems together with a complexity classification of whether they allow a fixed-parameter tractable reduction to SAT or not. These parameterized problems are based on problems whose complexity lies at the second level of the Polynomial Hierarchy or higher. The list will be updated as ... more >>>

So-called ordered variants of the classical notions of pathwidth and treewidth are introduced and proposed as proof theoretically meaningful complexity measures for the directed acyclic graphs underlying proofs. The ordered pathwidth of a proof is shown to be roughly the same as its formula space. Length-space lower bounds for R(k)-refutations ... more >>>

We investigate the parameterized complexity of deciding whether a constraint network is $k$-consistent. We show that, parameterized by $k$, the problem is complete for the complexity class co-W[2]. As secondary parameters we consider the maximum domain size $d$ and the maximum number $\ell$ of constraints in which a variable occurs. ... more >>>

We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixed-parameter tractable. We consider proofs that witness that a given propositional formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter. One could separate the ... more >>>

Clique-width is a graph parameter that measures in a certain sense the
complexity of a graph. Hard graph problems (e.g., problems
expressible in Monadic Second Order Logic with second-order
quantification on vertex sets, that includes NP-hard problems) can be
solved efficiently for graphs of certified small clique-width. It is
widely ... more >>>

Clique-width is a graph parameter, defined by a composition mechanism
for vertex-labeled graphs, which measures in a certain sense the
complexity of a graph. Hard graph problems (e.g., problems
expressible in Monadic Second Order Logic, that includes NP-hard
problems) can be solved efficiently for graphs of certified small
clique-width. It ... more >>>

The deficiency of a propositional formula F in CNF with n variables
and m clauses is defined as m-n. It is known that minimal
unsatisfiable formulas (unsatisfiable formulas which become
satisfiable by removing any clause) have positive deficiency.
Recognition of minimal unsatisfiable formulas is NP-hard, and it was
shown recently ... more >>>