On the Value of Multiple Read/Write Streams for Approximating Frequency Moments (2009)
We consider the read/write streams model, an extension of the standard data stream model in which an algorithm can create and manipulate multiple read/write streams in addition to its input data...
Optimal bounds for decision problems on the CRCW PRAM (2009)
Abstract. Optimal Q(logn/log logn) lower bounds on the time for CRCW PRAMS with polynomially bounded numbers of processors or memory cells to compute parity and a number of related problems are...
Longest Common Subsequences in Sets of Permutations (2009)
Beame, Paul, Blais, Eric, Huynh-Ngoc, Dang-Trinh
The sequence a_1,...,a_m is a common subsequence in the set of permutations S = {p_1,...,p_k} on [n] if it is a subsequence of p_i(1),...,p_i(n) and p_j(1),...,p_j(n) for some distinct p_i, p_j in S....
THE RESOLUTION COMPLEXITY OF INDEPENDENT SETS AND VERTEX COVERS IN RANDOM GRAPHS (2008)
Paul Beame, Russell Impagliazzo, Ashish Sabharwal
Abstract. We consider the problem of providing a resolution proof of the statement that a given graph with n vertices and average degree roughly ∆ does not contain an independent set of size k. For...
Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind
We consider extensions of the DPLL approach to satisfiability testing that add a version of memoization, in which formulas that the algorithm has previously shown to be unsatisfiable are remembered...
Abstract Exponential Lower Bounds for the Pigeonhole Principle * (2008)
Paul Beame, Russell Impagliazzo, Jan Krajiek, Toniann Pitassi, Pavel Pudlii. K, Alan Woods
In this paper we prove an exponential lower bound on the size of bounded-depth Frege proofs for the pigeon-hole principle (PHP). We also obtain an ~(log log rz)-depth lower bound for any...
Paul Beame, Toniann Pitassi, Nathan Segerlind, Avi Wigderson
Abstract. We prove that two-party randomized communication complexity satisfies a strong direct product property, so long as the communication lower bound is proved by a “corruption ” or...
Abstract Improving Efficiency of Symbolic Model Checking for State-Based System Requirements (2008)
William Chan, Richard J. Anderson, Paul Beame, David Notkin
We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques...
Paul Beame, Russell Impagliazzo, Ashish Sabharwal
Abstract. We consider the problem of providing a resolution proof of the statement that a given graph with n vertices and average degree roughly ∆ does not contain an independent set of size k. For...
Abstract Parallel Algorithms for Arrangements (2008)
Richard Anderson, Paul Beame, Erik Brisson
We give the first efficient parallel algorithms for solving the arrangement problem. We give a de-terministic algorithm for the CREW PRAM which runs in nearly optimal bounds of O(log n log * n) time...
Paul Beame, Russell Impagliazzo, Toniann Pitassi
Abstract. We consider the problem of determining, given a graph G with speci ed nodes s and t, whether or not there is a path of at most k edges in G from s to t. We show that solving this problem on...
Abstract Improving Efficiency of Symbolic Model Checking for State-Based System Requirements (2008)
William Chan, Richard J. Anderson, Paul Beame, David Notkin
We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques...
William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, William E. Warner
Symbolic model checking is a powerful formal-verification technique for reactive systems. In this paper we address the problem of symbolic model checking for software specifications written as...
Abstract The Relative Complexity of NP Search Problems (2008)
Paul Beame, Stephen Cookt, Jeff Edmonds, Russell Impagliazzo
Papadimitriou introduced several classes of NP search prob-lemsbased on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
Abstract Optimal Bounds for the Predecessor Problem (2008)
We obtain matching upper and lower bounds for the amount of time to find the predecessor of a given element among the elements of a fixed efficiently stored set. Our algorithms are for the unit-cost...
A Sharp Threshold in Proof Complexity Yields Lower Bounds for (2008)
Satisfiability Search Dimitris, Dimitris Achlioptas, Michael Molloy, Paul Beame
Let F (#n, #n) denote a random CNF formula consisting of #n randomly chosen 2-clauses and #n randomly chosen 3-clauses, for some arbitrary constants #, # 0. It is well-known that, with probability...
Project Supervisor: Dr. Manindra Agrawal AWARDS AND ACHIEVEMENTS (2008)
Ashish Sabharwal, Supervisors Profs, Carla P. Gomes, Bart Selman, Advisors Profs, Paul Beame, ...
All India 24 th Rank in IIT Entrance Examination (over 60,000 candidates) 1994
Project Supervisor: Dr. Manindra Agrawal AWARDS AND ACHIEVEMENTS (2008)
Ashish Sabharwal, Supervisors Profs, Carla P. Gomes, Bart Selman, Advisors Profs, Paul Beame, ...
All India 24 th Rank in IIT Entrance Examination (over 60,000 candidates) 1994
Multiparty Communication Complexity and Threshold Circuit Size of AC 0 (2008)
We prove an nΩ(1) /2O(k) lower bound on the randomized k-party communication complexity of read-once depth 4 AC0 functions in the number-on-forehead (NOF) model for up to Θ(log n) players. These...
Paul Beame, Paul Beame, Allan Borodin, Allan Borodin, Prabhakar Raghavan, Prabhakar Raghavan, ...
We prove time-space tradeoffs for traversing undirected graphs, using a variety of structured models that are all variants of Cook and Rackoff 's "Jumping Automata for Graphs"....
Paul Beame, Allan Borodin, Prabhakar Raghavan, Walter L. Ruzzo, Martin Tompa
We prove a time-space tradeoff for traversing undirected graphs, using a structured model that is a nonjumping variant of Cook and Rackoff's "Jumping Automata for Graphs". 3
Paul Beame, Michael Saks, Jayram S. Thathachar
We obtain the first non-trivial time-space tradeo # lower bound for functions f: {0,
Paul Beame, Michael Saks, Jayram S. Thathachar
We obtain the first non-trivial time-space tradeo # lower bound for functions f: {0,
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
Bounded-depth Frege lower bounds for weaker pigeonhole principles (2007)
Paul Beame, Toniann Pitassi, Ran Raz, Ashish Sabharwal
We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle PHP m n where m = (1 + 1=polylog n)n. This lower bound qualitatively matches the known...
Dimitris Achlioptas, Paul Beame, Michael Molloy
sharp threshold in proof complexity yields lower bounds for
Dimitris Achlioptas, Paul Beame, Michael Molloy
sharp threshold in proof complexity yields lower bounds for
Paul Beame, Richard Karp, Michael Saks
Abstract. We consider several problems related to the use of resolution-based methods for determining whether a given boolean formula in conjunctive normal form is satisable. First, building on work...
Lower bounds for randomized read/write stream algorithms (2007)
Motivated by the capabilities of modern storage architectures, we consider the following generalization of the data stream model where the algorithm has sequential access to multiple streams. Unlike...
List Decoding and Property Testing of Error Correcting Codes (2007)
Atri Rudra, Atri Rudra, Atri Rudra, Venkatesan Guruswami, Paul Beame, Venkatesan Guruswami, ...
This is to certify that I have examined this copy of a doctoral dissertation by
Separating deterministic from nondeterministic NOF multiparty communication complexity (2007)
Paul Beame, Matei David, Toniann Pitassi
Abstract. We solve some fundamental problems in the number-onforehead (NOF) k-party communication model. We show that there exists a function which has at most logarithmic communication complexity...
Atri Rudra, Atri Rudra, Atri Rudra, Venkatesan Guruswami, Paul Beame, Venkatesan Guruswami, ...
This is to certify that I have examined this copy of a doctoral dissertation by
Lower bounds for randomized read/write stream algorithms (2007)
Motivated by the capabilities of modern storage architectures, we consider the following generalization of the data stream model where the algorithm has sequential access to multiple streams. Unlike...
Paul Beame, Nathan Segerlind, Toniann Pitassi, Avi Wigderson
We prove that two-party randomized communication complexity satisfies a strong direct product property, so long as the communication lower bound is proved by a “corruption ” or “one-sided...
Paul Beame, Nathan Segerlind, Toniann Pitassi
bounds for Lovász-Schrijver systems and beyond follow
Heuristics for fast exact model counting (2005)
Tian Sang, Paul Beame, Henry Kautz
Abstract. An important extension of satisfiability testing is model-counting, a task that corresponds to problems such as probabilistic reasoning and computing the permanent of a Boolean matrix. We...
We prove that corruption, one of the most powerful measures used to analyze 2-party randomized communication complexity, satisfies a strong direct sum property under rectangular distributions. This...
Paul Beame, Toniann Pitassi, Nathan Segerlind
Abstract. We prove that an ω(log 3 n) lower bound for the three-party numberon-the-forehead (NOF) communication complexity of the set-disjointness function implies an n ω(1) size lower bound for...
Project Supervisor: Dr. Manindra Agrawal AWARDS AND ACHIEVEMENTS (2005)
Ashish Sabharwal, Supervisors Profs, Carla P. Gomes, Bart Selman, Advisors Profs, Paul Beame, ...
an extensive background in Theoretical Computer Science. I am interested in developing scalable and robust
Project Supervisor: Dr. Manindra Agrawal AWARDS AND ACHIEVEMENTS (2005)
Ashish Sabharwal, Supervisors Profs, Carla P. Gomes, Bart Selman, Advisors Profs, Paul Beame, ...
an extensive background in Theoretical Computer Science. I am interested in developing scalable and robust
Towards understanding and harnessing the potential of clause learning (2004)
Paul Beame, Henry Kautz, Ashish Sabharwal
Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant real-world problems, such as...
Combining component caching and clause learning for effective model counting (2004)
Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, Toniann Pitassi
Exponential Bounds for DPLL below the Satisfiability Threshold (2004)
Dimitris Achlioptas, Paul Beame, Michael Molloy
We prove that for every k 4 there exists a constant r k such that a random k-CNF formula F with n variables and #r k n# clauses is satisfiable with high probability, but every backtracking extension...
Exponential bounds for DPLL below the satisfiability threshold (2004)
Dimitris Achlioptas, Paul Beame, Michael Molloy
Abstract For each k * 4, we give rk? 0 such that a random k-CNF formula F with n variables and brknc clauses is satisfiable with high probability, but ordered-dll takes exponential time on F with...
Towards understanding and harnessing the potential of clause learning (2004)
Paul Beame, Henry Kautz, Ashish Sabharwal
Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant real-world problems, such as...
Exponential bounds for DPLL below the satisfiability threshold (2004)
Dimitris Achlioptas, Paul Beame, Michael Molloy
Abstract For each k> = 4, we give rk> 0 such that a random k-CNF formula F with n variables and brknc clausesis satisfiable with high probability, but ordered-dlltakes exponential time on F...
Combining component caching and clause learning for effective model counting (2004)
Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, Toniann Pitassi
Towards understanding and harnessing the potential of clause learning (2004)
Paul Beame, Henry Kautz, Ashish Sabharwal
Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant real-world problems, such as...
Exponential bounds for DPLL below the satisfiability threshold (2004)
Dimitris Achlioptas, Paul Beame, Michael Molloy
For each k ≥ 4, we give rk> 0 such that a random k-CNF formula F with n variables and ⌊rkn ⌋ clauses is satisfiable with high probability, but ordered-dll takes exponential time on F with...
Frank Mcsherry, Frank Mcsherry, Anna Karlin, Dimitris Achlioptas, Paul Beame, Anna Karlin, ...
Reading Committee: Date: and that any and all revisions required by the final examining committee have been made.
Memoization and DPLL: Formula caching proof systems (2003)
A fruitful connection between algorithm design and proof complexity is the formalization of the ¤¦¥¨§© § approach to satisfiability testing in terms of tree-like resolution proofs. We consider...
Understanding the power of clause learning (2003)
Paul Beame, Henry Kautz, Ashish Sabharwal
Efficient implementations of DPLL with the addition of clause learning are the fastest complete satisfiability solvers and can handle many significant real-world problems, such as verification,...
Understanding the power of clause learning (2003)
Paul Beame, Henry Kautz, Ashish Sabharwal
Efficient implementations of DPLL with the addition of clause learning are the fastest complete satisfiability solvers and can handle many significant real-world problems, such as verification,...
Using problem structure for efficient clause learning (2003)
Ashish Sabharwal, Paul Beame, Henry Kautz
Abstract. DPLL based clause learning algorithms for satisfiability testing are known to work very well in practice. However, like most branch-and-bound techniques, their performance depends heavily...
Memoization and DPLL: Formula Caching Proof Systems (2003)
Paul Beame Computer, Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind
A fruitful connection between algorithm design and proof complexity is the formalization of the DPLL approach to satisfiability testing in terms of tree-like resolution proofs. We consider extensions...
Using problem structure for efficient clause learning (2003)
Ashish Sabharwal, Paul Beame, Henry Kautz
Abstract. DPLL based clause learning algorithms for satisfiability testing are known to work very well in practice. However, like most branch-and-bound techniques, their performance depends heavily...
The Resolution Complexity of Random Graph k-Colorability (2003)
Paul Beame, Joseph Culberson, David Mitchell, Cristopher Moore
We consider the resolution proof complexity of propositional formulas which encode random instances of graph k-colorability. We obtain a tradeoff between the graph density and the resolution proof...
Paul Beame, David Mitchell, Joseph Culberson, Cristopher Moore
We consider the resolution proof complexity of propositional formulas which encode random instances of graph k-colorability. We obtain a tradeoff between the graph density and the resolution proof...
Optimal bounds for the predecessor problem and related problems (2002)
We obtain matching upper and lower bounds for the amount of time to find the predecessor of a given element among the elements of a fixed compactly stored set. Our algorithms are for the unit-cost...
Time-space tradeoffs, multiparty communication complexity, and nearest-neighbor problems (2002)
We extend recent techniques for time-space tradeoff lower bounds using multiparty communication complexity ideas. Using these arguments, for inputs from large domains we prove larger tradeoff lower...
The efficiency of resolution and Davis-Putnam procedures (2002)
Paul Beame, Richard Karp, Toniann Pitassi, Michael Saks
We consider several problems related to the use of resolution-based methods for determining whether a given boolean formula in conjunctive normal form is satisfiable. First, building on work of...
Optimal Bounds for the Predecessor Problem and Related Problems (2002)
We obtain matching upper and lower bounds for the amount of time to find the predecessor of a given element among the elements of a fixed efficiently stored set. Our algorithms are for the unit-cost...
Bounded-depth frege lower bounds for weaker pigeonhole principles (2002)
Joshua Buresh-oppenheim, Paul Beame, Toniann Pitassi, Ran Raz
Abstract. We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle P HP m n where m = (1 + 1/polylog n)n. This lower bound qualitatively matches...
A sharp threshold in proof complexity (2001)
Dimitris Achlioptas, Paul Beame, Michael Molloy
We give the rst example of a sharp threshold in proof complexity. More precisely, we show that for any > 0 and > 2:28, random formulas consisting of (1 )n 2clauses and n 3-clauses, which are...
A sharp threshold in proof complexity (2001)
Dimitris Achlioptas, Paul Beame, Michael Molloy
We give the first example of a sharp threshold in proof complexity. More precisely, we show that for any sufficiently small > 0 and > 2:28, random formulas consisting of (1 )n 2-clauses and n...
Optimal Bounds for the Predecessor Problem and Related Problems (2001)
We obtain matching upper and lower bounds for the amount of time to find the predecessor of a given element among the elements of a fixed compactly stored set. Our algorithms are for the unit-cost...
Resolution complexity of independent sets in random graphs (2001)
Paul Beame, Russell Impagliazzot
beame @ cs. was hington.edu We consider the problem of providing a resolution proof of the statement that a given graph with n ver-tices and An edges does not contain an independent set of size k....
Optimizing symbolic model checking for statecharts (2001)
William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, Senior Member, ...
AbstractÐSymbolic model checking based on binary decision diagrams is a powerful formal verification technique for reactive systems. In this paper, we present various optimizations for improving the...
A sharp threshold in proof complexity (2001)
Dimitris Achlioptas, Paul Beame, Michael Molloy
We give the first example of a sharp threshold in proof complexity. More precisely, we show that for any sufficiently small � and � � �, random formulas consisting of 2-clauses and 3-clauses,...
Super-linear time-space tradeoff lower bounds for randomized computation (2000)
Paul Beame, Michael Saks, Xiaodong Sun, Erik Vee
problems
Super-Linear Time-Space Tradeoff Lower Bounds for Randomized Computation (2000)
Paul Beame, Michael Saks, Xiaodong Sun, Erik Vee
We prove the first time-space lower bound tradeo#s for randomized computation of decision problems where computation error is allowed. Our techniques are an extension of those used by Ajtai [4, 5] in...
Optimal bounds for the predecessor problem (1999)
We obtain matching upper and lower bounds for the amount of time to find the predecessor of a given element among the elements of a fixed efficiently stored set. Our algorithms are for the unit-cost...
ªDecoupling Synchronization from Logic for Efficient Symbolic Model Checking of Statecharts,º (1999)
William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, William E. Warner
Symbolic model checking is a powerful formal-verification technique for reactive systems. In this paper we address the problem of symbolic model checking for software specifications written as...
William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, William E. Warner
Symbolic model checking is a powerful formal-verification technique for reactive systems. In this paper we address the problem of symbolic model checking for software specifications written as...
Model checking large software specifications (1998)
William Chan, Student Member, Richard J. Anderson, Paul Beame, Steve Burns, David Notkin, ...
Abstract—In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has...
Model checking large software specifications (1998)
Richard J. Anderson, Paul Beame, Steve Burns, William Chan, Francesmary Modugno, David Notkin, ...
In this paper we present our results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system. Symbolic model checking has been highly...
Time-space tradeoffs for branching programs (1998)
Paul Beame, Michael Saks, Jayram S. Thathachar
We obtain the first non-trivial time-space tradeoff lower bound for functions f: f0; 1g
The Relative Complexity of NP Search Problems (1998)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
Improving Efficiency of Symbolic Model Checking for State-Based System Requirements (1998)
William Chan, Richard J. Anderson, Paul Beame, David Notkin
We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques...
Decoupling Synchronization from Logic for Efficient Symbolic Model Checking of Statecharts (1998)
William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, William E. Warner
Symbolic model checking is a powerful formal-verification technique for reactive systems. In this paper we address the problem of symbolic model checking for software specifications written as...
Model Checking Large Software Specifications (1998)
William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, ...
In this paper we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly...
Improving Efficiency of Symbolic Model Checking for State-Based System Requirements (1998)
William Chan, Richard J. Anderson, Paul Beame, David Notkin
We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques...
Model checking large software specifications (1998)
William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, ...
Abstract—In this paper we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been...
Model checking large software specifications (1998)
Pdchard J. Anderson, Paul Beame, Steve Burns, William Chan, David Notkin, Jon D. Reese
In this paper we present our results and experiences of using symbolic model checking to study the specification of an air-craft collision avoidance system. Symbolic model checking has been highly...
On the complexity of unsatisfiability proofs for random k-cnf formulas (1998)
Paul Beame, Richard Karpf, Toniann Pitas, Ivlichael Sal
WC study the complexity of proving unsatisfiability for random k-CNP formulas with clause density A = m/n where 111 is number of clauses and n is the number of variables. We prove the first...
Time-space tradeoffs for branching programs (1998)
We obtain the first non-trivial time-space tradeoff lower bound for functions f: f0; 1g n! f0; 1g on general branching programs by exhibiting a Boolean function f that requires exponential size to be...
On Searching Sorted Lists: A Near-Optimal Lower Bound (1997)
We obtain improved lower bounds for a class of static and dynamic data structure problems that includes several problems of searching sorted lists as special cases. These lower bounds nearly match...
William Chan, Richard Anderson, Paul Beame, David Notkin
Abstract. We extend the conventional BDD-based model checking algorithms to verify systems with non-linear arithmetic constraints. We represent each constraint as a BDD variable, using the...
On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas (1997)
Paul Beame, Richard Karp, Toniann Pitassi, Michael Saks
We study the complexity of proving unsatisfiability for random k-CNF formulas with clause density D = m=n where m is number of clauses and n is the number of variables. We prove the first nontrivial...
Time-Space Tradeoffs for Undirected Graph Traversal by Graph Automata (1997)
Paul Beame, Allan Borodin, Prabhakar Raghavan, Walter L. Ruzzo, Martin Tompa
We investigate time-space tradeoffs for traversing undirected graphs, using a variety of structured models that are all variants of Cook and Rackoff's "Jumping Automata for Graphs"....
The Relative Complexity of NP Search Problems (1997)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
More on the Relative Strength of Counting Principles (1997)
this paper we attempt to give as complete a presentation as possible. We now outline the structure of the argument, giving references for the key techniques. We use the notion of a k-evaluation due...
William Chan, Richard Anderson, Paul Beame, David Notkin
We extend the conventional BDD-based model checking algorithms to verify systems with non-linear arithmetic constraints. We represent each constraint as a BDD variable, using the information from a...
Lower bounds on Hilbert's Nullstellensatz and propositional proofs (1996)
Paul Beame, Russell Impagliazzo, Jan Krajlcek, Toniann Pitassi, Pavel Pudlak
The so-called weak form of Hilbert's Nullstellensatz says that a system of algebraic equations over a field, Qj(x) = 0, does not have a solution in the algebraic closure if and only if 1 is in...
Simplified and Improved Resolution Lower Bounds (1996)
Paul Beame Computer, Paul Beame, Toniann Pitassi
We give simple new lower bounds on the lengths of Resolution proofs for the pigeonhole principle and for randomly generated formulas. For random formulas, our bounds significantly extend the range of...
Lower bounds on Hilbert's Nullstellensatz and propositional proofs (1996)
Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, Pavel Pudlák
The so called weak form of the Hilbert's Nullstellensatz says that a system of algebraic equations over a field, Q i (x) = 0, does not have a solution in the algebraic closure iff 1 is in the...
An Exponential Separation between the Parity Principle and the Pigeonhole Principle (1996)
The combinatorial parity principle states that there is no perfect matching on an odd number of vertices. This principle generalizes the pigeonhole principle, which states that for a fixed...
Model Checking Large Software Specifications (1996)
Richard J. Anderson, Paul Beame, Steve Burns, William Chan, Francesmary Modugno, David Notkin, ...
In this paper we present our results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system. Symbolic model checking has been highly...
Lower bounds on Hilbert's Nullstellensatz and propositional proofs (1996)
Paul Beame, Russell Impagliazzo, Toniann Pitassi
The so called weak form of the Hilbert's Nullstellensatz says that a system of algebraic equations over a field, Q i (¯x) = 0, does not have a solution in the algebraic closure iff 1 is in the...
Lower bounds on Hilbert's Nullstellensatz and propositional proofs (1996)
Paul Beame, Russell Impagliazzo, Toniann Pitassi
The weak form of the Hilbert's Nullstellensatz says that a system of algebraic equations over a field, Q i (¯x) = 0, does not have a solution in the algebraic closure iff 1 is in the ideal...
Simplified and Improved Resolution Lower Bounds (1996)
We give simple new lower bounds on the lengths of Resolution proofs for the pigeonhole principle and for randomly generated formulas. For random formulas, our bounds significantly extend the range of...
Model Checking Large Software Specifications (1996)
Richard J. Anderson, Paul Beame, Steve Burns, William Chan, Francesmary Modugno, David Notkin, ...
In this paper we present our results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system. Symbolic model checking has been highly...
Model Checking Large Software Specifications (1996)
Richard Anderson, Paul Beame, Steve Burns, William Chan, Francesmary Modugno, David Notkin, ...
In this paper we present our results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system. Symbolic model checking has been highly...
Improved Depth Lower Bounds for Small Distance Connectivity (1995)
Paul Beame Computer, Paul Beame, Russell Impagliazzo, Toniann Pitassi
We consider the problem of determining, given a graph G and specified nodes s and t, whether or not there is a path of at most k edges in G from s to t. We show that solving this problem on...
Improved Depth Lower Bounds for Small Distance Connectivity (1995)
Paul Beame Computer, Paul Beame, Russell Impagliazzo, Toniann Pitassi
We consider the problem of determining, given a graph G and specified nodes s and t, whether or not there is a path of at most k edges in G from s to t. We show that solving this problem on...
The Relative Complexity of NP Search Problems (1995)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
Improved Depth Lower Bounds for Small Distance Connectivity (1995)
Paul Beame, Russell Impagliazzo, Toniann Pitassi
We consider the problem of determining, given a graph G and specified nodes s and t, whether or not there is a path of at most k edges in G from s to t. We show that solving this problem on...
The Relative Complexity of NP Search Problems (1995)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
Communication-space tradeoffs for unrestricted protocols (1994)
Paul Beame, Martin Tompa, Peiyuan Yan
This paper introduces communicating branching programs, and develops a general technique for demonstrating communication-space tradeoffs for pairs of communicating branching programs. This technique...
An Exponential Separation between the Matching Principle and the Pigeonhole Principle (1993)
Paul Beame, Paul Beame, Toniann Pitassi, Toniann Pitassi
The combinatorial matching principle states that there is no perfect matching on an odd number of vertices. This principle generalizes the pigeonhole principle, which states that for a fixed...
Time-Space Tradeoffs for Undirected Graph Traversal (1993)
Paul Beame, Paul Beame, Allan Borodin, Allan Borodin, Prabhakar Raghavan, Prabhakar Raghavan, ...
We prove time-space tradeoffs for traversing undirected graphs, using a variety of structured models that are all variants of Cook and Rackoff 's "Jumping Automata for Graphs". Our...
The relative complexity of NP search problems (1993)
Paul Beame, Stephen Cook Y, Jeff Edmonds Z, Russell Impagliazzo X, Toniann Pitassi
Research supported by NSF grants CCR-8858799 and CCR-9303017
Information Broadcasting by Exclusive-Read Prams (1992)
We consider the problem of copying information stored initially in a single memory cell by Exclusive Read Exclusive Write Parallel Random Access Machines (EREW PRAMs). We prove lower bounds for this...
A General Sequential Time-Space Tradeoff for Finding Unique Elements (1991)
An optimal R(n2) lower bound is shown for the time-space product of any R-way branching program that determines those values which occur exactly once in a list of n integers in the range [l, R] where...
Time-space tradeoffs for undirected graph traversal (1990)
Paul Beame, Allan Borodin, Prabhakar Raghavan, Walter L. Ruzzo, Martin Tompa
We prove time-space tradeoffs for traversing undi-rected graphs. One of these is a quadratic lower bound on a deterministic model that closely matches the recent probabilistic upper bound of Broder,...
Time-space tradeoffs for undirected graph traversal (1990)
Paul Beame, Allan Borodin, Prabhakar Raghavan, Walter L. Ruzzo, Martin Tompa
Abstract. We prove a time-space tradeoff for traversing undirected graphs, using a structured model that is a nonjumping variant of Cook and Rackoff’s “jumping automata for graphs.”
Time-space tradeoffs for undirected graph traversal (1990)
Paul Beame, Allan Borodin, Prabhakar Raghavan, Walter L. Ruzzo, Martin Tompa
We investigate time-space tradeoffs for traversing undirected graphs, using a variety of structured models that are all variants of Cook and Rackoff's ``Jumping Automata for Graphs.' '...
Random routing in constant degree networks / (1982)
Thèse (MSc.) - University of Toronto, 1982.
Separating the Power of EREW and CREW PRAMs with Small Communication Width
Paul Beame, Faith E. Fich, Rakesh K. Sinha
We prove that evaluating a Boolean decision tree of height h requires\Omega h m+log 3 h ) time on any EREW PRAM with communication width m and any number of processors. Since this function can be...