All reports by Author Eli Ben-Sasson:

__
TR17-134
| 8th September 2017
__

Eli Ben-Sasson, Iddo Bentov, Ynon Horesh, Michael Riabzev#### Fast Reed-Solomon Interactive Oracle Proofs of Proximity

__
TR16-156
| 12th October 2016
__

Eli Ben-Sasson, Alessandro Chiesa, Michael Forbes, Ariel Gabizon, Michael Riabzev, Nicholas Spooner#### On Probabilistic Checking in Perfect Zero Knowledge

Revisions: 1

__
TR16-149
| 23rd September 2016
__

Eli Ben-Sasson, iddo Ben-Tov, Ariel Gabizon, Michael Riabzev#### A security analysis of Probabilistically Checkable Proofs

Comments: 1

__
TR16-073
| 7th May 2016
__

Eli Ben-Sasson, iddo Ben-Tov, Ariel Gabizon, Michael Riabzev#### Improved concrete efficiency and security analysis of Reed-Solomon PCPPs

Revisions: 1
,
Comments: 1

__
TR16-046
| 23rd March 2016
__

Eli Ben-Sasson, Alessandro Chiesa, Ariel Gabizon, Michael Riabzev, Nicholas Spooner#### Short Interactive Oracle Proofs with Constant Query Complexity, via Composition and Sumcheck

Revisions: 2

__
TR16-001
| 9th January 2016
__

Eli Ben-Sasson, Alessandro Chiesa, Ariel Gabizon, Madars Virza#### Quasi-Linear Size Zero Knowledge from Linear-Algebraic PCPs

Revisions: 1

__
TR15-209
| 29th December 2015
__

Eli Ben-Sasson, Gal Maor#### On the information leakage of public-output protocols

__
TR15-139
| 25th August 2015
__

Eli Ben-Sasson, Gal Maor#### Lower bound for communication complexity with no public randomness

__
TR15-094
| 10th June 2015
__

Eli Ben-Sasson, iddo Ben-Tov, Ivan Bjerre Damgard, Yuval Ishai, Noga Ron-Zewi#### On Public Key Encryption from Noisy Codewords

__
TR14-017
| 9th February 2014
__

Eli Ben-Sasson, Emanuele Viola#### Short PCPs with projection queries

__
TR13-085
| 13th June 2013
__

Eli Ben-Sasson, Yohay Kaplan, Swastik Kopparty, Or Meir, Henning Stichtenoth#### Constant rate PCPs for circuit-SAT with sublinear query complexity

__
TR12-159
| 20th November 2012
__

Eli Ben-Sasson, Michael Viderman#### A Combinatorial Characterization of smooth LTCs and Applications

__
TR12-148
| 7th November 2012
__

Eli Ben-Sasson, Ariel Gabizon, Yohay Kaplan, Swastik Kopparty, Shubhangi Saraf#### A new family of locally correctable codes based on degree-lifted algebraic geometry codes

Revisions: 1

__
TR12-135
| 26th October 2012
__

Eli Ben-Sasson, Noga Ron-Zewi, Madhur Tulsiani, Julia Wolf#### Sampling-based proofs of almost-periodicity results and algorithmic applications

Revisions: 2

__
TR12-049
| 27th April 2012
__

Eli Ben-Sasson, Noga Ron-Zewi, Madhu Sudan#### Sparse affine-invariant linear codes are locally testable

__
TR12-045
| 22nd April 2012
__

Eli Ben-Sasson, Alessandro Chiesa, Daniel Genkin, Eran Tromer#### On the Concrete-Efficiency Threshold of Probabilistically-Checkable Proofs

Revisions: 3

__
TR11-157
| 25th November 2011
__

Eli Ben-Sasson, Shachar Lovett, Noga Ron-Zewi#### An additive combinatorics approach to the log-rank conjecture in communication complexity

Revisions: 1

__
TR11-129
| 22nd September 2011
__

Eli Ben-Sasson, Ariel Gabizon#### Extractors for Polynomials Sources over Constant-Size Fields of Small Characteristic

__
TR11-079
| 9th May 2011
__

Eli Ben-Sasson, Elena Grigorescu, Ghid Maatouk, Amir Shpilka, Madhu Sudan#### On Sums of Locally Testable Affine Invariant Properties

__
TR11-070
| 1st May 2011
__

Eli Ben-Sasson, Michael Viderman#### Composition of semi-LTCs by two-wise Tensor Products

__
TR10-200
| 14th December 2010
__

Eli Ben-Sasson, Michael Viderman#### Towards lower bounds on locally testable codes via density arguments

__
TR10-199
| 14th December 2010
__

Eli Ben-Sasson, Ghid Maatouk, Amir Shpilka, Madhu Sudan#### Symmetric LDPC codes are not necessarily locally testable

__
TR10-144
| 20th September 2010
__

Eli Ben-Sasson, Noga Ron-Zewi#### From Affine to Two-Source Extractors via Approximate Duality

Revisions: 1

__
TR10-125
| 11th August 2010
__

Eli Ben-Sasson, Jakob Nordström#### Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

__
TR10-123
| 4th August 2010
__

Eli Ben-Sasson#### Limitation on the rate of families of locally testable codes

Revisions: 1

__
TR10-108
| 9th July 2010
__

Eli Ben-Sasson, Madhu Sudan#### Limits on the rate of locally testable affine-invariant codes

__
TR10-085
| 20th May 2010
__

Eli Ben-Sasson, Jan Johannsen#### Lower bounds for width-restricted clause learning on small width formulas

__
TR10-068
| 15th April 2010
__

Shir Ben-Israel, Eli Ben-Sasson, David Karger#### Breaking local symmetries can dramatically reduce the length of propositional refutations

__
TR10-044
| 12th March 2010
__

Eli Ben-Sasson, Swastik Kopparty#### Affine Dispersers from Subspace Polynomials

__
TR10-004
| 6th January 2010
__

Eli Ben-Sasson, Michael Viderman#### Low Rate Is Insufficient for Local Testability

Revisions: 3

__
TR09-126
| 26th November 2009
__

Eli Ben-Sasson, Venkatesan Guruswami, Tali Kaufman, Madhu Sudan, Michael Viderman#### Locally Testable Codes Require Redundant Testers

Revisions: 3

__
TR09-047
| 20th April 2009
__

Eli Ben-Sasson, Jakob Nordström#### A Space Hierarchy for k-DNF Resolution

Comments: 1

__
TR09-034
| 25th March 2009
__

Eli Ben-Sasson, Jakob Nordström#### Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs

Comments: 1

__
TR09-007
| 9th January 2009
__

Eli Ben-Sasson, Michael Viderman#### Tensor Products of Weakly Smooth Codes are Robust

__
TR09-002
| 23rd November 2008
__

Eli Ben-Sasson, Jakob Nordström#### Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution

__
TR07-127
| 22nd November 2007
__

Arie Matsliah, Eli Ben-Sasson, Prahladh Harsha, Oded Lachish#### Sound 3-query PCPPs are Long

__
TR04-060
| 22nd July 2004
__

Eli Ben-Sasson, Madhu Sudan#### Simple PCPs with Poly-log Rate and Query Complexity

__
TR04-046
| 4th June 2004
__

Eli Ben-Sasson, Madhu Sudan#### Robust Locally Testable Codes and Products of Codes

__
TR04-021
| 23rd March 2004
__

Eli Ben-Sasson, Oded Goldreich, Prahladh Harsha, Madhu Sudan, Salil Vadhan#### Robust PCPs of Proximity, Shorter PCPs and Applications to Coding

__
TR04-016
| 3rd March 2004
__

Michael Alekhnovich, Eli Ben-Sasson#### Linear Upper Bounds for Random Walk on Small Density Random 3CNFs

__
TR03-019
| 3rd April 2003
__

Eli Ben-Sasson, Oded Goldreich, Madhu Sudan#### Bounds on 2-Query Codeword Testing.

Revisions: 1

__
TR03-006
| 23rd January 2003
__

Eli Ben-Sasson, Prahladh Harsha, Sofya Raskhodnikova#### 3CNF Properties are Hard to Test

__
TR03-004
| 24th December 2002
__

Eli Ben-Sasson, Prahladh Harsha#### Lower Bounds for Bounded-Depth Frege Proofs via Buss-Pudlack Games

__
TR02-003
| 24th December 2001
__

Eli Ben-Sasson, Yonatan Bilu#### A Gap in Average Proof Complexity

__
TR01-031
| 5th April 2001
__

Eli Ben-Sasson, Nicola Galesi#### Space Complexity of Random Formulae in Resolution

__
TR00-023
| 11th May 2000
__

Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson#### Pseudorandom Generators in Propositional Proof Complexity

__
TR00-005
| 17th January 2000
__

Eli Ben-Sasson, Russell Impagliazzo, Avi Wigderson#### Near-Optimal Separation of Treelike and General Resolution

__
TR99-040
| 20th October 1999
__

Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson#### Space Complexity in Propositional Calculus

__
TR99-022
| 14th June 1999
__

Eli Ben-Sasson, Avi Wigderson#### Short Proofs are Narrow - Resolution made Simple

Eli Ben-Sasson, Iddo Bentov, Ynon Horesh, Michael Riabzev

The family of Reed-Solomon (RS) codes plays a prominent role in the construction of quasilinear probabilistically checkable proofs (PCPs) and interactive oracle proofs (IOPs) with perfect zero knowledge and polylogarithmic verifiers. The large concrete computational complexity required to prove membership in RS codes is one of the biggest obstacles to ... more >>>

Eli Ben-Sasson, Alessandro Chiesa, Michael Forbes, Ariel Gabizon, Michael Riabzev, Nicholas Spooner

We present the first constructions of *single*-prover proof systems that achieve *perfect* zero knowledge (PZK) for languages beyond NP, under no intractability assumptions:

1. The complexity class #P has PZK proofs in the model of Interactive PCPs (IPCPs) [KR08], where the verifier first receives from the prover a PCP and ... more >>>

Eli Ben-Sasson, iddo Ben-Tov, Ariel Gabizon, Michael Riabzev

Probabilistically Checkable Proofs (PCPs) [Babai et al. FOCS 90; Arora et al. JACM 98] can be used to construct asymptotically efficient cryptographic zero knowledge arguments of membership in any language in NEXP, with minimal communication complexity and computational effort on behalf of both prover and verifier [Babai et al. STOC ... more >>>

Eli Ben-Sasson, iddo Ben-Tov, Ariel Gabizon, Michael Riabzev

A Probabilistically Checkable Proof of Proximity (PCPP) for a linear code $C$, enables to determine very efficiently if a long input $x$, given as an oracle, belongs to $C$ or is far from $C$.

PCPPs are often a central component of constructions of Probabilistically Checkable Proofs (PCP)s [Babai et al. ...
more >>>

Eli Ben-Sasson, Alessandro Chiesa, Ariel Gabizon, Michael Riabzev, Nicholas Spooner

We study *interactive oracle proofs* (IOPs) (Ben-Sasson, Chiesa, Spooner '16), which combine aspects of probabilistically checkable proofs (PCPs) and interactive proofs (IPs). We present IOP constructions and general techniques that enable us to obtain tradeoffs in proof length versus query complexity that are not known to be achievable via PCPs ... more >>>

Eli Ben-Sasson, Alessandro Chiesa, Ariel Gabizon, Madars Virza

The seminal result that every language having an interactive proof also has a zero-knowledge interactive proof assumes the existence of one-way functions. Ostrovsky and Wigderson (ISTCS 1993) proved that this assumption is necessary: if one-way functions do not exist, then only languages in BPP have zero-knowledge interactive proofs.

Ben-Or et ... more >>>

Eli Ben-Sasson, Gal Maor

In this paper three complexity measures are studied: (i) internal information, (ii) external information, and (iii) a measure called here "output information". Internal information (i) measures the counter-party privacy-loss inherent in a communication protocol. Similarly, the output information (iii) measures the reduction in input-privacy that is inherent when the output ... more >>>

Eli Ben-Sasson, Gal Maor

We give a self contained proof of a logarithmic lower bound on the communication complexity of any non redundant function, given that there is no access to shared randomness. This bound was first stated in Yao's seminal paper [STOC 1979], but no full proof appears in the literature.

Our proof ... more >>>

Eli Ben-Sasson, iddo Ben-Tov, Ivan Bjerre Damgard, Yuval Ishai, Noga Ron-Zewi

Several well-known public key encryption schemes, including those of Alekhnovich (FOCS 2003), Regev (STOC 2005), and Gentry, Peikert and Vaikuntanathan (STOC 2008), rely on the conjectured intractability of inverting noisy linear encodings. These schemes are limited in that they either require the underlying field to grow with the security parameter, ... more >>>

Eli Ben-Sasson, Emanuele Viola

We construct a PCP for NTIME(2$^n$) with constant

soundness, $2^n \poly(n)$ proof length, and $\poly(n)$

queries where the verifier's computation is simple: the

queries are a projection of the input randomness, and the

computation on the prover's answers is a 3CNF. The

previous upper bound for these two computations was

more >>>

Eli Ben-Sasson, Yohay Kaplan, Swastik Kopparty, Or Meir, Henning Stichtenoth

The PCP theorem (Arora et. al., J. ACM 45(1,3)) says that every NP-proof can be encoded to another proof, namely, a probabilistically checkable proof (PCP), which can be tested by a verifier that queries only a small part of the PCP. A natural question is how large is the blow-up ... more >>>

Eli Ben-Sasson, Michael Viderman

The study of locally testable codes (LTCs) has benefited from a number of nontrivial constructions discovered in recent years. Yet we still lack a good understanding of what makes a linear error correcting code locally testable and as a result we do not know what is the rate-limit of LTCs ... more >>>

Eli Ben-Sasson, Ariel Gabizon, Yohay Kaplan, Swastik Kopparty, Shubhangi Saraf

We describe new constructions of error correcting codes, obtained by "degree-lifting" a short algebraic geometry (AG) base-code of block-length $q$ to a lifted-code of block-length $q^m$, for arbitrary integer $m$. The construction generalizes the way degree-$d$, univariate polynomials evaluated over the $q$-element field (also known as Reed-Solomon codes) are "lifted" ... more >>>

Eli Ben-Sasson, Noga Ron-Zewi, Madhur Tulsiani, Julia Wolf

We give new combinatorial proofs of known almost-periodicity results for sumsets of sets with small doubling in the spirit of Croot and Sisask [Geom. Funct. Anal. 2010], whose almost-periodicity lemma has had far-reaching implications in additive combinatorics. We provide an alternative (and $L^p$-norm free) point of view, which allows for ... more >>>

Eli Ben-Sasson, Noga Ron-Zewi, Madhu Sudan

We show that sparse affine-invariant linear properties over arbitrary finite fields are locally testable with a constant number of queries. Given a finite field ${\mathbb{F}}_q$ and an extension field ${\mathbb{F}}_{q^n}$, a property is a set of functions mapping ${\mathbb{F}}_{q^n}$ to ${\mathbb{F}}_q$. The property is said to be affine-invariant if it ... more >>>

Eli Ben-Sasson, Alessandro Chiesa, Daniel Genkin, Eran Tromer

Probabilistically-Checkable Proofs (PCPs) form the algorithmic core that enables succinct verification of long proofs/computations in many cryptographic constructions, such as succinct arguments and proof-carrying data.

Despite the wonderful asymptotic savings they bring, PCPs are also the infamous computational bottleneck preventing these cryptographic constructions from being used in practice. This reflects ... more >>>

Eli Ben-Sasson, Shachar Lovett, Noga Ron-Zewi

For a {0,1}-valued matrix $M$ let CC($M$) denote the deterministic communication complexity of the boolean function associated with $M$. The log-rank conjecture of Lovasz and Saks [FOCS 1988] states that CC($M$) is at most $\log^c({\mbox{rank}}(M))$ for some absolute constant $c$ where rank($M$) denotes the rank of $M$ over the field ... more >>>

Eli Ben-Sasson, Ariel Gabizon

Let $F$ be the field of $q$ elements, where $q=p^{\ell}$ for prime $p$. Informally speaking, a polynomial source is a distribution over $F^n$ sampled by low degree multivariate polynomials. In this paper, we construct extractors for polynomial sources over fields of constant size $q$ assuming $p \ll q$.

More generally, ... more >>>

Eli Ben-Sasson, Elena Grigorescu, Ghid Maatouk, Amir Shpilka, Madhu Sudan

Affine-invariant properties are an abstract class of properties that generalize some

central algebraic ones, such as linearity and low-degree-ness, that have been

studied extensively in the context of property testing. Affine invariant properties

consider functions mapping a big field $\mathbb{F}_{q^n}$ to the subfield $\mathbb{F}_q$ and include all

properties that form ...
more >>>

Eli Ben-Sasson, Michael Viderman

In this paper we obtain a composition theorem that allows us to construct locally testable codes (LTCs) by repeated two-wise tensor products. This is the First composition theorem showing that repeating the two-wise tensor operation any constant number of times still results in a locally testable code, improving upon previous ... more >>>

Eli Ben-Sasson, Michael Viderman

The main open problem in the area of locally testable codes (LTCs) is whether there exists an asymptotically good family of LTCs and to resolve this question it suffices to consider the case of query complexity $3$. We argue that to refute the existence of such an asymptotically good family ... more >>>

Eli Ben-Sasson, Ghid Maatouk, Amir Shpilka, Madhu Sudan

Locally testable codes, i.e., codes where membership in the code is testable with a constant number of queries, have played a central role in complexity theory. It is well known that a code must be a "low-density parity check" (LDPC) code for it to be locally testable, but few LDPC ... more >>>

Eli Ben-Sasson, Noga Ron-Zewi

Two-source and affine extractors and dispersers are fundamental objects studied in the context of derandomization. This paper shows how to construct two-source extractors and dispersers for arbitrarily small min-entropy rate in a black-box manner from affine extractors with sufficiently good parameters. Our analysis relies on the study of approximate duality, ... more >>>

Eli Ben-Sasson, Jakob Nordström

For current state-of-the-art satisfiability algorithms based on the DPLL procedure and clause learning, the two main bottlenecks are the amounts of time and memory used. In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There ... more >>>

Eli Ben-Sasson

This paper describes recent results which revolve around the question of the rate attainable by families of error correcting codes that are locally testable. Emphasis is placed on motivating the problem of proving upper bounds on the rate of these codes and a number of interesting open questions for future ... more >>>

Eli Ben-Sasson, Madhu Sudan

A linear code is said to be affine-invariant if the coordinates of the code can be viewed as a vector space and the code is invariant under an affine transformation of the coordinates. A code is said to be locally testable if proximity of a received word

to the code ...
more >>>

Eli Ben-Sasson, Jan Johannsen

It has been observed empirically that clause learning does not significantly improve the performance of a SAT solver when restricted

to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from ...
more >>>

Shir Ben-Israel, Eli Ben-Sasson, David Karger

This paper shows that the use of ``local symmetry breaking'' can dramatically reduce the length of propositional refutations. For each of the three propositional proof systems known as (i) treelike resolution, (ii) resolution, and (iii) k-DNF resolution, we describe families of unsatisfiable formulas in conjunctive normal form (CNF) that are ... more >>>

Eli Ben-Sasson, Swastik Kopparty

{\em Dispersers} and {\em extractors} for affine sources of dimension $d$ in $\mathbb F_p^n$ --- where $\mathbb F_p$ denotes the finite field of prime size $p$ --- are functions $f: \mathbb F_p^n \rightarrow \mathbb F_p$ that behave pseudorandomly when their domain is restricted to any particular affine space $S \subseteq ... more >>>

Eli Ben-Sasson, Michael Viderman

Locally testable codes (LTCs) are error-correcting codes for which membership of a given word in the code can be tested probabilistically by examining it in very few locations.

Kaufman and Sudan \cite{KS07} proved that sparse, low-bias linear codes are locally testable (in particular sparse random codes are locally testable).

Kopparty ...
more >>>

Eli Ben-Sasson, Venkatesan Guruswami, Tali Kaufman, Madhu Sudan, Michael Viderman

Locally testable codes (LTCs) are error-correcting codes for which membership, in the code, of a given word can be tested by examining it in very few locations. Most known constructions of locally testable codes are linear codes, and give error-correcting codes

whose duals have (superlinearly) {\em many} small weight ...
more >>>

Eli Ben-Sasson, Jakob Nordström

The k-DNF resolution proof systems are a family of systems indexed by

the integer k, where the kth member is restricted to operating with

formulas in disjunctive normal form with all terms of bounded arity k

(k-DNF formulas). This family was introduced in [Krajicek 2001] as an

extension of the ...
more >>>

Eli Ben-Sasson, Jakob Nordström

For current state-of-the-art satisfiability algorithms based on the

DPLL procedure and clause learning, the two main bottlenecks are the

amounts of time and memory used. Understanding time and memory

consumption, and how they are related to one another, is therefore a

question of considerable practical importance. In the field of ...
more >>>

Eli Ben-Sasson, Michael Viderman

We continue the study of {\em robust} tensor codes and expand the

class of base codes that can be used as a starting point for the

construction of locally testable codes via robust two-wise tensor

products. In particular, we show that all unique-neighbor expander

codes and all locally correctable codes, ...
more >>>

Eli Ben-Sasson, Jakob Nordström

A number of works have looked at the relationship between length and space of resolution proofs. A notorious question has been whether the existence of a short proof implies the existence of a proof that can be verified using limited space.

In this paper we resolve the question by answering ... more >>>

Arie Matsliah, Eli Ben-Sasson, Prahladh Harsha, Oded Lachish

We initiate the study of the tradeoff between the {\em length} of a

probabilistically checkable proof of proximity (PCPP) and the

maximal {\em soundness} that can be guaranteed by a $3$-query

verifier with oracle access to the proof. Our main observation is

that a verifier limited to querying a short ...
more >>>

Eli Ben-Sasson, Madhu Sudan

We give constructions of PCPs of length n*polylog(n) (with respect

to circuits of size n) that can be verified by making polylog(n)

queries to bits of the proof. These PCPs are not only shorter than

previous ones, but also simpler. Our (only) building blocks are

Reed-Solomon codes and the bivariate ...
more >>>

Eli Ben-Sasson, Madhu Sudan

We continue the investigation of locally testable codes, i.e.,

error-correcting codes for whom membership of a given word in the

code can be tested probabilistically by examining it in very few

locations. We give two general results on local testability:

First, motivated by the recently proposed notion of robust

probabilistically ...
more >>>

Eli Ben-Sasson, Oded Goldreich, Prahladh Harsha, Madhu Sudan, Salil Vadhan

We continue the study of the trade-off between the length of PCPs

and their query complexity, establishing the following main results

(which refer to proofs of satisfiability of circuits of size $n$):

We present PCPs of length $\exp(\tildeO(\log\log n)^2)\cdot n$

that can be verified by making $o(\log\log n)$ Boolean queries.

more >>>

Michael Alekhnovich, Eli Ben-Sasson

We analyze the efficiency of the random walk algorithm on random 3CNF instances, and prove em linear upper bounds on the running time

of this algorithm for small clause density, less than 1.63. Our upper bound matches the observed running time to within a multiplicative factor. This is the ...
more >>>

Eli Ben-Sasson, Oded Goldreich, Madhu Sudan

We present upper bounds on the size of codes that are locally

testable by querying only two input symbols. For linear codes, we

show that any $2$-locally testable code with minimal distance

$\delta n$ over a finite field $F$ cannot have more than

$|F|^{3/\delta}$ codewords. This result holds even ...
more >>>

Eli Ben-Sasson, Prahladh Harsha, Sofya Raskhodnikova

For a boolean formula \phi on n variables, the associated property

P_\phi is the collection of n-bit strings that satisfy \phi. We prove

that there are 3CNF properties that require a linear number of queries,

even for adaptive tests. This contrasts with 2CNF properties

that are testable with O(\sqrt{n}) ...
more >>>

Eli Ben-Sasson, Prahladh Harsha

We present a simple proof of the bounded-depth Frege lower bounds of

Pitassi et. al. and Krajicek et. al. for the pigeonhole

principle. Our method uses the interpretation of proofs as two player

games given by Pudlak and Buss. Our lower bound is conceptually

simpler than previous ones, and relies ...
more >>>

Eli Ben-Sasson, Yonatan Bilu

We present the first example of a natural distribution on instances

of an NP-complete problem, with the following properties.

With high probability a random formula from this

distribution (a) is unsatisfiable,

(b) has a short proof that can be found easily, and (c) does not have a short

(general) resolution ...
more >>>

Eli Ben-Sasson, Nicola Galesi

We study the space complexity of refuting unsatisfiable random $k$-CNFs in

the Resolution proof system. We prove that for any large enough $\Delta$,

with high probability a random $k$-CNF over $n$ variables and $\Delta n$

clauses requires resolution clause space of

$\Omega(n \cdot \Delta^{-\frac{1+\epsilon}{k-2-\epsilon}})$,

for any $0<\epsilon<1/2$. For constant $\Delta$, ...
more >>>

Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson

We call a pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ {\em

hard} for a propositional proof system $P$ if $P$ can not efficiently

prove the (properly encoded) statement $G_n(x_1,\ldots,x_n)\neq b$ for

{\em any} string $b\in\{0,1\}^m$. We consider a variety of

``combinatorial'' pseudorandom generators inspired by the

Nisan-Wigderson generator on the one hand, and ...
more >>>

Eli Ben-Sasson, Russell Impagliazzo, Avi Wigderson

We present the best known separation

between tree-like and general resolution, improving

on the recent $\exp(n^\epsilon)$ separation of \cite{BEGJ98}.

This is done by constructing a natural family of contradictions, of

size $n$, that have $O(n)$-size resolution

refutations, but only $\exp (\Omega(n/\log n))$-size tree-like refutations.

This result ...
more >>>

Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson

We study space complexity in the framework of

propositional proofs. We consider a natural model analogous to

Turing machines with a read-only input tape, and such

popular propositional proof systems as Resolution, Polynomial

Calculus and Frege systems. We propose two different space measures,

corresponding to the maximal number of bits, ...
more >>>

Eli Ben-Sasson, Avi Wigderson

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 general Resolution, and its tree-like

variant. The following consequences of these relations reveal width as ...
more >>>