Skip to main content

Research Repository

Advanced Search

Outputs (25)

The limits of tractability in Resolution-based propositional proof systems (2011)
Journal Article
Dantchev, S., & Martin, B. (2012). The limits of tractability in Resolution-based propositional proof systems. Annals of Pure and Applied Logic, 163(3), 656-668. https://doi.org/10.1016/j.apal.2011.11.001

We study classes of propositional contradictions based on the Least Number Principle (LNP) in the refutation system of Resolution and its generalisations with bounded conjunction, Res(k). We prove that any first-order sentence with no finite models t... Read More about The limits of tractability in Resolution-based propositional proof systems.

Sublinear-Time Algorithms for Tournament Graphs (2009)
Presentation / Conference Contribution
Dantchev, S., Friedetzky, T., & Nagel, L. (2009, July). Sublinear-Time Algorithms for Tournament Graphs. Presented at 15th Annual International Conference of Computing and Combinatorics (COCOON 2009), Niagara Falls, New York, USA

We show that a random walk on a tournament on n vertices finds either a sink or a 3-cycle in expected time O (√n ∙ log n ∙ √log*n), that is, sublinear both in the size of the description of the graph as well as in the number of vertices. This result... Read More about Sublinear-Time Algorithms for Tournament Graphs.

Dynamic Neighbourhood Cellular Automata (2009)
Journal Article
Dantchev, S. (2011). Dynamic Neighbourhood Cellular Automata. The Computer Journal, 54(1), 26-30. https://doi.org/10.1093/comjnl/bxp019

We propose a definition of cellular automaton in which each cell can change its neighbourhood during a computation. This is done locally by looking not farther than neighbours of neighbours and the number of links remains bounded by a constant throug... Read More about Dynamic Neighbourhood Cellular Automata.

Tight rank lower bounds for the Sherali–Adams proof system (2009)
Journal Article
Dantchev, S., Martin, B., & Rhodes, M. (2009). Tight rank lower bounds for the Sherali–Adams proof system. Theoretical Computer Science, 410(21-23), 2054-2063. https://doi.org/10.1016/j.tcs.2009.01.002

We consider a proof (more accurately, refutation) system based on the Sherali–Adams (SA) operator associated with integer linear programming. If F is a CNF contradiction that admits a Resolution refutation of width k and size s, then we prove that th... Read More about Tight rank lower bounds for the Sherali–Adams proof system.

Parameterized proof complexity (2007)
Presentation / Conference Contribution
Dantchev, S., Martin, B., & Szeider, S. (2007, October). Parameterized proof complexity. Presented at 48th Annual IEEE Symposium on Foundations of Computer Science, Providence, USA

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 se... Read More about Parameterized proof complexity.

Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems (2007)
Presentation / Conference Contribution
Dantchev, S. (2007, June). Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems. Presented at 39th Annual ACM Symposium on Theory of Computing, San Diego, CA

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 pr... Read More about Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems.

Bounded-degree Forbidden-Pattern Problems are Constraint Satisfaction Problems (2006)
Presentation / Conference Contribution
Dantchev, S., & Madelaine, F. (2006, December). Bounded-degree Forbidden-Pattern Problems are Constraint Satisfaction Problems. Presented at International Computer Science Symposium in Russia., St. Peterburg, Russia

Forbidden Pattern problem (FPP) is a proper generalisation of Constraint Satisfaction Problem (CSP). FPP is related to MMSNP, a logic introduced in relation with CSP by Feder and Vardi. We prove that Forbidden Pattern Problems are Constraint Satisfac... Read More about Bounded-degree Forbidden-Pattern Problems are Constraint Satisfaction Problems.

On the Computational Limits of Infinite Satisfaction. (2005)
Presentation / Conference Contribution
Dantchev, S., & Valencia, F. (2005, March). On the Computational Limits of Infinite Satisfaction. Presented at The 20th Annual ACM Symposium on Applied Computing, Santa Fe, USA

On relativisation and complexity gap for resolution-based proof systems (2003)
Presentation / Conference Contribution
Dantchev, S., & Riis, S. (2003, August). On relativisation and complexity gap for resolution-based proof systems. Presented at 12th Annual Conference of the EACSL Computer Science Logic., Vienna, Austria

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 su... Read More about On relativisation and complexity gap for resolution-based proof systems.