Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with cutting planes:
TR97-032 | 11th July 1997
Jan Johannsen

Lower Bounds for Monotone Real Circuit Depth and Formula Size and Tree-like Cutting Planes

Using a notion of real communication complexity recently
introduced by J. Krajicek, we prove a lower bound on the depth of
monotone real circuits and the size of monotone real formulas for
st-connectivity. This implies a super-polynomial speed-up of dag-like
over tree-like Cutting Planes proofs.

more >>>

TR03-041 | 29th May 2003
Albert Atserias, Maria Luisa Bonet, Jordi Levy

On Chvatal Rank and Cutting Planes Proofs

We study the Chv\'atal rank of polytopes as a complexity measure of
unsatisfiable sets of clauses. Our first result establishes a
connection between the Chv\'atal rank and the minimum refutation
length in the cutting planes proof system. The result implies that
length lower bounds for cutting planes, or even for ... more >>>

TR07-010 | 4th January 2007
Arist Kojevnikov

Improved Lower Bounds for Resolution over Linear Inequalities

Revisions: 1

We continue a study initiated by Krajicek of
a Resolution-like proof system working with clauses of linear
inequalities, R(CP). For all proof systems of this kind
Krajicek proved an exponential lower bound that depends
on the maximal absolute value of coefficients in the given proof and
the maximal clause width.

... more >>>

TR07-078 | 11th August 2007
Ran Raz, Iddo Tzameret

Resolution over Linear Equations and Multilinear Proofs

We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. ... more >>>

TR12-124 | 29th September 2012
Massimo Lauria

A rank lower bound for cutting planes proofs of Ramsey Theorem

Ramsey Theorem is a cornerstone of combinatorics and logic. In its
simplest formulation it says that there is a function $r$ such that
any simple graph with $r(k,s)$ vertices contains either a clique of
size $k$ or an independent set of size $s$. We study the complexity
of proving upper ... more >>>

TR13-128 | 16th September 2013
Pavel Hrubes

A note on semantic cutting planes

We show that the semantic cutting planes proof system has feasible interpolation via monotone real circuits. This gives an exponential lower bound on proof length in the system.

We also pose the following problem: can every multivariate non-decreasing function be expressed as a composition of non-decreasing functions in two ... more >>>

TR14-138 | 29th October 2014
Nicola Galesi, Pavel Pudlak, Neil Thapen

The space complexity of cutting planes refutations

We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of inequalities that need to be kept on a blackboard while verifying it. We show that any ... more >>>

TR16-010 | 28th January 2016
Alexander Razborov

On the Width of Semi-Algebraic Proofs and Algorithms

In this paper we initiate the study of width in semi-algebraic proof systems
and various cut-based procedures in integer programming. We focus on two
important systems: Gomory-Chv\'atal cutting planes and
Lov\'asz-Schrijver lift-and-project procedures. We develop general methods for
proving width lower bounds and apply them to random $k$-CNFs and several ... more >>>

TR17-037 | 25th February 2017
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

Understanding Cutting Planes for QBFs

We define a cutting planes system CP+$\forall$red for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while ... more >>>

TR17-151 | 8th October 2017
Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, Robert Robere

Stabbing Planes

We introduce and develop a new semi-algebraic proof system, called Stabbing Planes that is in the style of DPLL-based modern SAT solvers. As with DPLL, there is only one rule: the current polytope can be subdivided by
branching on an inequality and its "integer negation.'' That is, we can (nondeterministically ... more >>>

TR18-041 | 26th February 2018
Sam Buss, Dmitry Itsykson, Alexander Knop, Dmitry Sokolov

Reordering Rule Makes OBDD Proof Systems Stronger

Atserias, Kolaitis, and Vardi [AKV04] showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD($\land$, weakening), simulates CP* (Cutting Planes with unary coefficients). We show that OBDD($\land$, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring ... more >>>

ISSN 1433-8092 | Imprint