STOC
2012
ACM
12 years 2 months ago
2012
ACM
We give the first time-space tradeoff lower bounds for Resolution proofs that apply to superlinear space. In particular, we show that there are formulas of size N that have Reso...
CADE
2011
Springer
13 years 12 days ago
2011
Springer
This paper describes two algorithms for the compression of propositional resolution proofs. The first algorithm, RecyclePivotsWithIntersection, performs partial regularization, re...
CC
2010
Springer
13 years 7 months ago
2010
Springer
We show a general reduction that derives lower bounds on degrees of polynomial calculus proofs of tautologies over any field of characteristic other than 2 from lower bounds for r...
FOCS
1998
IEEE
14 years 4 months ago
1998
IEEE
We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential sepa...
STOC
1999
ACM
14 years 4 months ago
1999
ACM
The width of a Resolution proof is defined to be the maximal number of literals in any clause of the proof. In this paper, we relate proof width to proof length (ϭsize), in both g...
FOCS
1999
IEEE
14 years 4 months ago
1999
IEEE
This paper is concerned with the complexity of proofs and of searching for proofs in two propositional proof systems: Resolution and Polynomial Calculus (PC). For the former syste...
SAT
2009
Springer
14 years 7 months ago
2009
Springer
We use the notion of boundary points to study resolution proofs. Given a CNF formula F, a lit(x)-boundary point is a complete assignment falsifying only clauses of F having the sam...