All reports by Author Christoph Berkholz:

__
TR17-154
| 12th October 2017
__

Christoph Berkholz#### The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs

__
TR16-203
| 21st December 2016
__

Christoph Berkholz, Jakob NordstrÃ¶m#### Supercritical Space-Width Trade-offs for Resolution

__
TR16-135
| 31st August 2016
__

Christoph Berkholz, Jakob NordstrÃ¶m#### Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps

Christoph Berkholz

We relate different approaches for proving the unsatisfiability of a system of real polynomial equations over Boolean variables. On the one hand, there are the static proof systems Sherali-Adams and sum-of-squares (a.k.a. Lasserre), which are based on linear and semi-definite programming relaxations. On the other hand, we consider polynomial calculus, ... more >>>

Christoph Berkholz, Jakob NordstrÃ¶m

We show that there are CNF formulas which can be refuted in resolution

in both small space and small width, but for which any small-width

proof must have space exceeding by far the linear worst-case upper

bound. This significantly strengthens the space-width trade-offs in

[Ben-Sasson '09]}, and provides one more ...
more >>>

Christoph Berkholz, Jakob NordstrÃ¶m

We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of n-element structures that can be distinguished by a k-variable first-order sentence but where every such sentence requires quantifier depth at least n^?(k/log k). Our trade-offs also apply to first-order counting logic, and ... more >>>