Author name cluster

Stefan S. Dantchev

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

FOCS Conference 2007 Conference Paper

Parameterized Proof Complexity

Stefan S. Dantchev
Barnaby Martin
Stefan Szeider

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 CNF formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter (we call such a formula a parameterized contradiction). One could separate the parameterized complexity classes FPT and W(M. Cesati, 2006) by showing that there is no fpt-bounded parameterized proof system, i. e. , that there is no proof system that admits proofs of size f(k)n O(1) where f is a computable function and n represents the size of the propositional formula. By way of a first step, we introduce the system of parameterized tree-like resolution, and show that this system is not fpt-bounded. Indeed we give a general result on the size of shortest tree-like resolution proofs of parameterized contradictions that uniformly encode first-order principles over a universe of size n. We establish a dichotomy theorem that splits the exponential case of Riis's complexity-gap Theorem into two sub-cases, one that admits proofs of size f(k)n O(1) and one that does not. We also discuss how the set of parameterized contradictions may be embedded into the set of (ordinary) contradictions by the addition of new axioms. When embedded into general (DAG-like) resolution, we demonstrate that the pigeonhole principle has a proof of size 2 k n 2. This contrasts with the case of tree-like resolution where the embedded pigeonhole principle falls into the "non-FPT" category of our dichotomy.

Details

STOC Conference 2007 Conference Paper

Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems

Stefan S. Dantchev

We prove a dichotomy theorem for the rank of the uniformly generated(i.e. expressible in First-Order (FO) Logic) propositional tautologiesin both the Lovász-Schrijver (LS) and Sherali-Adams (SA) proofsystems. More precisely, we first show that the propositional translationsof FO formulae that are universally true, i.e. hold in all finiteand infinite models, have LS proofs whose rank is constant, independentlyfrom the size of the (finite) universe. In contrast to that, we provethat the propositional formulae that hold in all finite models butfail in some infinite structure require proofs whose SA rank grows poly-logarithmically with the size of the universe. Up to now, this kind of so-called "Complexity Gap" theorems have been known for Tree-like Resolution and, in somehow restrictedforms, for the Resolution and Nullstellensatz proof systems. As faras we are aware, this is the first time the Sherali-Adams lift-and-projectmethod has been considered as a propositional proof system. An interesting feature of the SA proof system is that it is static and rank-preserving simulates LS, the Lovász-Schrijver proof system without semidefinitecuts.

Details

CSL Conference 2003 Conference Paper

On Relativisation and Complexity Gap

Stefan S. Dantchev
Søren Riis

Abstract We study the proof complexity of Taut, the class of Second-Order Existential (SO∃) logical sentences which fail in all finite models. The Complexity-Gap theorem for Tree-like Resolution says that the shortest Tree-like Resolution refutation of any such sentence Φ is either fully exponential, \(2^{\Omega \left(n\right)}\), or polynomial, \(n^{O\left(1\right)}\), where n is the size of the finite model. Moreover, there is a very simple model-theoretics criteria which separates the two cases: the exponential lower bound holds if and only if Φ holds in some infinite model. In the present paper we prove several generalisations and extensions of the Complexity-Gap theorem. 1 For a natural subclass of Taut, \(Rel\left(Taut\right)\), there is a gap between polynomial Tree-like Resolution proofs and sub-exponential, \(2^{\Omega \left(n^{\varepsilon }\right)}\), general (DAG-like) Resolution proofs, whilst the separating model-theoretic criteria is the same as before. \(Rel\left(Taut\right)\) is the set of all sentences in Taut, relativised with respect to a unary predicate. 2 The gap for stronger systems, \(\textrm{Res}^{*}\left(k\right)\), is between polynomial and \(\exp \left(\Omega \left(\frac{\log k}{k}n\right)\right)\) for every k, 1≤ k ≤ n. \(\textrm{Res}^{*}\left(k\right)\) is an extension of Tree-like Resolution, in which literals are replaced by terms (i. e. conjunctions of literals) of size at most k. The lower bound is tight. 3 There is (as expected) no gap for any propositional proof system (including Tree-like Resolution) if we enrich the language of SO logic by a built-in order.

Details

FOCS Conference 2001 Conference Paper

"Planar" Tautologies Hard for Resolution

Stefan S. Dantchev
Søren Riis

We prove exponential lower bounds on the resolution proofs of some tautologies, based on rectangular grid graphs. More specifically, we show a 2/sup /spl Omega/(n)/ lower bound for any resolution proof of the mutilated chessboard problem on a 2n/spl times/2n chessboard as well as for the Tseitin tautology (G. Tseitin, 1968) based on the n/spl times/n rectangular grid graph. The former result answers a 35 year old conjecture by J. McCarthy (1964).

Details