Skip to main content

Research Repository

Advanced Search

All Outputs (13)

The Riis Complexity Gap for QBF Resolution (2024)
Journal Article
Beyersdorff, O., Clymo, J., Dantchev, S., & Martin, B. (2024). The Riis Complexity Gap for QBF Resolution. Journal on Satisfiability, Boolean Modeling and Computation, 15(1), 9-25. https://doi.org/10.3233/sat-231505

We give an analogue of the Riis Complexity Gap Theorem in Resolution for Quantified Boolean Formulas (QBFs). Every first-order sentence ϕ without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like QBF Resolution sys... Read More about The Riis Complexity Gap for QBF Resolution.

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.

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.

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.

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.