All reports by Author Sam Buss:

__
TR24-045
| 6th March 2024
__

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria#### Redundancy for MaxSAT

__
TR24-033
| 24th February 2024
__

Sam Buss, Emre Yolcu#### Regular resolution effectively simulates resolution

__
TR24-001
| 2nd January 2024
__

Sam Buss, Neil Thapen#### A Simple Supercritical Tradeoff between Size and Height in Resolution

__
TR22-141
| 20th October 2022
__

Sam Buss, Noah Fleming, Russell Impagliazzo#### TFNP Characterizations of Proof Systems and Monotone Circuits

Revisions: 2

__
TR20-073
| 5th May 2020
__

Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, Dmitry Sokolov#### Lower Bounds on OBDD Proofs with Several Orders

__
TR18-041
| 26th February 2018
__

Sam Buss, Dmitry Itsykson, Alexander Knop, Dmitry Sokolov#### Reordering Rule Makes OBDD Proof Systems Stronger

__
TR16-144
| 15th September 2016
__

Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky#### Expander Construction in VNC${}^1$

Revisions: 2

__
TR15-163
| 11th October 2015
__

James Aisenberg, Maria Luisa Bonet, Sam Buss#### 2-D Tucker is PPA complete

__
TR11-031
| 8th March 2011
__

Sam Buss, Ryan Williams#### Limits on Alternation-Trading Proofs for Time-Space Lower Bounds

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria

The concept of redundancy in SAT lead to more expressive and powerful proof search techniques, e.g. able to express various inprocessing techniques, and to interesting hierarchies of proof systems [Heule et.alâ€™20, Buss-Thapenâ€™19].

We propose a general way to integrate redundancy rules in MaxSAT, that is we define MaxSAT variants of ...
more >>>

Sam Buss, Emre Yolcu

Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with ... more >>>

Sam Buss, Neil Thapen

We describe CNFs in n variables which, over a range of parameters, have small resolution refutations but are such that any small refutation must have height larger than n (even exponential in n), where the height of a refutation is the length of the longest path in it. This is ... more >>>

Sam Buss, Noah Fleming, Russell Impagliazzo

Connections between proof complexity and circuit complexity have become major tools for obtaining lower bounds in both areas. These connections -- which take the form of interpolation theorems and query-to-communication lifting theorems -- translate efficient proofs into small circuits, and vice versa, allowing tools from one area to be applied ... more >>>

Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, Dmitry Sokolov

This paper is motivated by seeking lower bounds on OBDD($\land$, weakening, reordering) refutations, namely OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1-NBP($\land$) refutations based on read-once nondeterministic branching programs. These generalize OBDD($\land$, reordering) refutations. There are polynomial size 1-NBP($\land$) refutations of the pigeonhole principle, hence ... more >>>

Sam Buss, Dmitry Itsykson, Alexander Knop, Dmitry Sokolov

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

Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [Annals of Mathematics, 2002], and show that this analysis can be formalized in the bounded-arithmetic system $VNC^1$ (corresponding to the ``$NC^1$ reasoning''). As a corollary, we prove the ... more >>>

James Aisenberg, Maria Luisa Bonet, Sam Buss

The 2-D Tucker search problem is shown to be PPA-hard under many-one reductions; therefore it is complete for PPA. The same holds for $k$-D Tucker for all $k\ge 2$. This corrects a claim in the literature that the Tucker search problem is in PPAD.

more >>>Sam Buss, Ryan Williams

This paper characterizes alternation trading based proofs that satisfiability is not in the time and space bounded class $\DTISP(n^c, n^\epsilon)$, for various values $c<2$ and $\epsilon<1$. We characterize exactly what can be proved in the $\epsilon=0$ case with currently known methods, and prove the conjecture of Williams that $c=2\cos(\pi/7)$ is ... more >>>