Skip to main content

Research Repository

Advanced Search

Dr Stefan Dantchev's Outputs (24)

Depth lower bounds in Stabbing Planes for combinatorial principles (2024)
Journal Article
Dantchev, S., Galesi, N., Ghani, A., & Martin, B. (2024). Depth lower bounds in Stabbing Planes for combinatorial principles. Logical Methods in Computer Science, 20(1), 1-19. https://doi.org/10.46298/lmcs-20%281%3A1%292024

Stabbing Planes (also known as Branch and Cut) is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prov... Read More about Depth lower bounds in Stabbing Planes for combinatorial principles.

Sherali-Adams and the binary encoding of combinatorial principles (2020)
Presentation / Conference Contribution
Dantchev, S., Ghani, A., & Martin, B. (2020, May). Sherali-Adams and the binary encoding of combinatorial principles. Presented at LATIN 2020, São Paulo, Brazil

We consider the Sherali-Adams ( SA ) refutation system together with the unusual binary encoding of certain combinatorial principles. For the unary encoding of the Pigeonhole Principle and the Least Number Principle, it is known that linear rank is r... Read More about Sherali-Adams and the binary encoding of combinatorial principles.

Resolution and the binary encoding of combinatorial principles (2019)
Presentation / Conference Contribution
Dantchev, S., Galesi, N., & Martin, B. (2019). Resolution and the binary encoding of combinatorial principles. In A. Shpilka (Ed.), 34th Computational Complexity Conference (CCC 2019) (6:1-6:25). https://doi.org/10.4230/lipics.ccc.2019.6

Res(s) is an extension of Resolution working on s-DNFs. We prove tight n (k) lower bounds for the size of refutations of the binary version of the k-Clique Principle in Res(o(log log n)). Our result improves that of Lauria, Pudlák et al. [27] who pro... Read More about Resolution and the binary encoding of combinatorial principles.

Simplicial Complex Entropy (2017)
Presentation / Conference Contribution
Dantchev, S., & Ivrissimtzis, I. (2016, June). Simplicial Complex Entropy. Presented at 9th International Conference on Mathematical Methods for Curves and Surfaces, Tønsberg, Norway

We propose an entropy function for simplicial complices. Its value gives the expected cost of the optimal encoding of sequences of vertices of the complex, when any two vertices belonging to the same simplex are indistinguishable. We focus on the com... Read More about Simplicial Complex Entropy.

Relativization makes contradictions harder for Resolution (2013)
Journal Article
Dantchev, S., & Martin, B. (2014). Relativization makes contradictions harder for Resolution. Annals of Pure and Applied Logic, 165(3), 837-857. https://doi.org/10.1016/j.apal.2013.10.009

We provide a number of simplified and improved separations between pairs of Resolution-with-bounded-conjunction refutation systems, Res(d), as well as their tree-like versions, Res∗(d). The contradictions we use are natural combinatorial principles:... Read More about Relativization makes contradictions harder for Resolution.

Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems (2012)
Journal Article
Dantchev, S., & Martin, B. (2013). Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems. Computational Complexity, 22(1), 191-213. https://doi.org/10.1007/s00037-012-0049-1

We prove a dichotomy theorem for the rank of propositional contradictions, uniformly generated from first-order sentences, in both the Lovász-Schrijver (LS) and Sherali-Adams (SA) refutation systems. More precisely, we first show that the proposition... Read More about Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems.

Cutting Planes and the Parameter Cutwidth (2012)
Journal Article
Dantchev, S., & Martin, B. (2012). Cutting Planes and the Parameter Cutwidth. Theory of Computing Systems, 51(1), 50-64. https://doi.org/10.1007/s00224-011-9373-0

We introduce the parameter cutwidth for the Cutting Planes (CP) system of Gomory and Chvátal. We provide linear lower bounds on cutwidth for two simple polytopes. Considering CP as a propositional refutation system, one can see that the cutwidth of a... Read More about Cutting Planes and the Parameter Cutwidth.

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). Parameterized proof complexity. In 48th Annual IEEE Symposium on Foundations of Computer Science, FOCS '07, 21-23 October 2007, Providence, RI ; proceedings (150-160). https://doi.org/10.1109/focs.2007.53

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). Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems. In STOC '07 : proceedings of the 39th Annual ACM Symposium on Theory of Computing : San Diego, California, USA, June 11-13, 2007 (311-317). https://doi.org/10.1145/1250790.1250837

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 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.

Improved sorting-based procedure for integer programming (2002)
Journal Article
Dantchev, S. (2002). Improved sorting-based procedure for integer programming. Mathematical Programming, 92(2), 297-300. https://doi.org/10.1007/s101070100245

Recently, Cornuéjols and Dawande have considered a special class of 0-1 programs that turns out to be hard for existing IP solvers. One of them is a sorting-based algorithm, based on an idea of Wolsey. In this paper, we show how to improve both the r... Read More about Improved sorting-based procedure for integer programming.

Planar tautologies hard for resolution (2001)
Presentation / Conference Contribution
Dantchev, S., & Riis, S. (2001). Planar tautologies hard for resolution. In 42nd IEEE Symposium on Foundations of Computer Science, FOCS 2001, 14-17 October 2001, Las Vegas, Nevada ; proceedings (220-229). https://doi.org/10.1109/sfcs.2001.959896

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... Read More about Planar tautologies hard for resolution.

Tree resolution proofs of the weak pigeon-hole principle (2001)
Presentation / Conference Contribution
Dantchev, S., & Riis, S. (2001). Tree resolution proofs of the weak pigeon-hole principle. In 16th Annual IEEE Conference on Computational Complexity, 18-21 June 2001, Chicago, Illinois ; proceedings (69-77). https://doi.org/10.1109/ccc.2001.933873

We prove that any optimal tree resolution proof of PHPn m is of size 2&thetas;(n log n), independently from m, even if it is infinity. So far, only a 2Ω(n) lower bound has been known in the general case. We also show that any, not necessarily optimal... Read More about Tree resolution proofs of the weak pigeon-hole principle.