1,720,973 research outputs found
A framework for space complexity in algebraic proof systems
No full textAlgebraic proof systems, such as Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR), refute contradictions using polynomials. Space complexity for such systems measures the number of distinct monomials to be kept in memory while verifying a proof. We introduce a new combinatorial framework for proving space lower bounds in algebraic proof systems. As an immediate application, we obtain the space lower bounds previously provided for PC/PCR [Alekhnovich et al. 2002; Filmus et al. 2012]. More importantly, using our approach in its full potential, we prove Ω(n) space lower bounds in PC/PCR for random k-CNFs (k ≥ 4) in n variables, thus solving an open problem posed in Alekhnovich et al. [2002] and Filmus et al. [2012]. Our method also applies to the Graph Pigeonhole Principle, which is a variant of the Pigeonhole Principle defined over a constant (left) degree expander graph
Total space in resolution
No full textWe show quadratic lower bounds on the total space used in resolution refutations of random k-CNFs over n variables and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the open problem of whether there are families of k-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large widt
Proofs of Space: When Space Is of the Essence
Full text linkProofs of computational effort were devised to control denial of service attacks. Dwork and Naor (CRYPTO ’92), for example, proposed to use such proofs to discourage spam. The idea is to couple each email message with a proof of work that demonstrates the sender performed some computational task. A proof of work can be either CPU-bound or memory-bound. In a CPU-bound proof, the prover must compute a CPU-intensive function that is easy to check by the verifier. A memory-bound proof, instead, forces the prover to access the main memory several times, effectively replacing CPU cycles with memory accesses.
In this paper we put forward a new concept dubbed proof of space. To compute such a proof, the prover must use a specified amount of space, i.e., we are not interested in the number of accesses to the main memory (as in memory-bound proof of work) but rather on the amount of actual memory the prover must employ to compute the proof. We give a complete and detailed algorithmic description of our model. We develop a comprehensive theoretical analysis which uses combinatorial tools from Complexity Theory (such as pebbling games) which are essential in studying space lower bounds
Space proof complexity for random 3-CNFs
Full text linkWe investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF φ in n variables requires, with high probability, distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of φ requires, with high probability, clauses each of width to be kept at the same time in memory. This gives a lower bound for the total space needed in Resolution to refute φ. These results are best possible (up to a constant factor) and answer questions about space complexity of 3-CNFs
Misure di Complessita' delle dimostrazioni per la Risoluzione e il Calcolo dei Polinomi
No full textIn questo lavoro di tesi vengono presentati dei risultati relativi alla Risoluzione e al Calcolo dei Polinomi. In particolare verranno presentati i giochi di Ehrenfreucht-Fraissè come quadro teorico in cui inquadrare le stime conosciute per il width e lo spazio in Risoluzione. Per quanto riguarda il Calcolo dei Polinomi invece verranno presentati dei risultati riguardo il grado e lo spazio
On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares
Full text linkVanishing sums of roots of unity can be seen as a natural generalization of knapsack from Boolean variables to variables taking values over the roots of unity. We show that these sums are hard to prove for polynomial calculus and for sum-of-squares, both in terms of degree and size
SETH and Resolution
No full textThere are unsatisfiable -CNF formulas in n variables such that each regular resolution refutation of those has size at least where where goes to 0 as goes to infinity. The problem of finding -CNF formulas for which we can prove such strong size lower bounds in resolution (or stronger systems) is open. A lower bound of this form for resolution would imply that CDCL solvers cannot disprove the Strong Exponential Time Hypothesis.
In this talk we give a simple proof of the result for regular resolution with the idea in mind to attack the problem for general resolution (or stronger systems).
(Talk based on joint works with Navid Talebanfard)Non UBCUnreviewedAuthor affiliation: UPC Universitat Politècnica de CatalunyaPostdoctora
- …
