Currently, the most effective complete SAT solvers are based on the DPLL algorithm augmented by Clause Learning. These solvers can handle many real-world problems from application areas like verification, diagnosis, planning, and design. Clause Learning works by storing previously computed, intermediate results and then reusing them to prune the future search tree. Without Clause Learning, however, DPLL loses most of its effectiveness on real world problems. Recently there has been some work on obtaining a deeper understanding of the technique of Clause Learning. In this thesis, we contribute to the understanding of Clause Learning, and the Resolution proof system that underlies it, in a number of ways. We characterize Clause Learning as a new, intuitive Resolution refinement which we call CL. We then show that CL proofs can effectively p-simulate general Resolution. Furthermore, this result holds even for the more restrictive class of greedy, unit propagating CL proofs, which more accurately characterize Clause Learning as it is used in practice. This result is surprising and indicates that Clause Learning is significantly more powerful than was previously known. Since Clause Learning makes use of previously derived clauses, it motivates the study of Resolution space. We contribute to this area of study by proving that determining the variable space of a Resolution derivation is PSPACE-complete. The reduction also yields a surprising exponential size/space trade-off for Resolution in which an increase of just 3 units of variable space results in an exponential decrease in proofsize. This result runs counter to the intuitions of many in the SAT-solving community who have generally believed that proof-size should decrease smoothly as available space increases. In order to prove these Resolution results, we need to make use of some intuition regarding the relationship between Black-White Pebbling and Resolution. In fact, determining the complexity of Resolution variable space required us to first prove that Black-White Pebbling is PSPACE-complete. The complexity of the Black-White Pebbling Game has remained an open problem for 30 years and resisted numerous attempts to solve it. Its solution is the primary contribution of this thesis.

Currently, the most effective complete SAT solvers are based on the DPLL algorithm augmented by Clause Learning. These solvers can handle many real-world problems from application areas like verification, diagnosis, planning, and design. Clause Learning works by storing previously computed, intermediate results and then reusing them to prune the future search tree. Without Clause Learning, however, DPLL loses most of its effectiveness on real world problems. Recently there has been some work on obtaining a deeper understanding of the technique of Clause Learning. In this thesis, we contribute to the understanding of Clause Learning, and the Resolution proof system that underlies it, in a number of ways. We characterize Clause Learning as a new, intuitive Resolution refinement which we call CL. We then show that CL proofs can effectively p-simulate general Resolution. Furthermore, this result holds even for the more restrictive class of greedy, unit propagating CL proofs, which more accurately characterize Clause Learning as it is used in practice. This result is surprising and indicates that Clause Learning is significantly more powerful than was previously known. Since Clause Learning makes use of previously derived clauses, it motivates the study of Resolution space. We contribute to this area of study by proving that determining the variable space of a Resolution derivation is PSPACE-complete. The reduction also yields a surprising exponential size/space trade-off for Resolution in which an increase of just 3 units of variable space results in an exponential decrease in proofsize. This result runs counter to the intuitions of many in the SAT-solving community who have generally believed that proof-size should decrease smoothly as available space increases. In order to prove these Resolution results, we need to make use of some intuition regarding the relationship between Black-White Pebbling and Resolution. In fact, determining the complexity of Resolution variable space required us to first prove that Black-White Pebbling is PSPACE-complete. The complexity of the Black-White Pebbling Game has remained an open problem for 30 years and resisted numerous attempts to solve it. Its solution is the primary contribution of this thesis.

We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.

We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of \emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds. A proof system $P$ is \emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution.

We investigate the unprovability of NP$\not\subseteq$P/poly in various fragments of arithmetic. The unprovability is usually obtained by showing hardness of propositional formulas encoding superpolynomial circuit lower bounds. Firstly, we discuss few relevant techniques and known theorems. Namely, natural proofs, feasible interpolation, KPT theorem, iterability, gadget generators etc. Then we prove some original results. We show the unprovability of superpolynomial circuit lower bounds for systems admitting certain forms of feasible interpolation (modulo a hardness assumption) and for systems roughly described as tree-like Frege systems working with formulas using only a small fraction of variables of the statement that is supposed to be proved. These results are obtained by proving the hardness of the Nisan-Wigderson generators in corresponding proof systems.

In the present work, we study the propositional proof complexity. First, we prove an exponential lower bound on the complexity of resolution applying directly Razborov's approximation method, which was previously used only for bounds on the size of monotone circuits. Next, we use the approximation method for a new proof of an exponential lower bound on the complexity of random resolution refutations. That should have further applications in separating some theories in bounded arithmetic. In both cases, we use a problem from the graph theory called Broken Mosquito Screens. Finally, we state a conjecture that the approximation method is applicable even for stronger propositional proof systems, for example Cutting Plane Proofs. Powered by TCPDF (www.tcpdf.org)

In this thesis we explore a number of ways in which combinatorial games can be used to help prove results in the area of propositional proof complexity. The results in this thesis can be divided into two sets, the first being dedicated to the study of Resolution space (memory) requirements, whereas the second is centered on formalizing the notion of `dangerous' reductions. The first group of results investigate Resolution space measures by asking questions of the form, `Given a formula F and integer k, does F have a [Type of Resolution] proof with [Type of Resource] at most k?'. We refer to this as a proof complexity resource problem, and provide comprehensive results for several forms of Resolution as well as various resources. These results include the PSPACE-Completeness of Tree Resolution clause space (and the Prover/Delayer game), the PSPACE-Completeness of Input Resolution derivation total space, and the PSPACE-Hardness of Resolution variable space. This research has theoretical as well as practical motivations: Proof complexity research has focused on the size of proofs, and Resolution space requirements are an interesting new theoretical area of study. In more practical terms, the Resolution proof system forms the underpinnings of all modern SAT-solving algorithms, including clause learning. In practice, the limiting factor on these algorithms is memory space, so there is a strong motivation for better understanding it as a resource. With the second group of results in this thesis we investigate and formalize what it means for a reduction to be `dangerous'. The area of SAT-solving necessarily employs reductions in order to translate from other domains to SAT, where the power of highly-optimized algorithms can be brought to bear. Researchers have empirically observed that it is unfortunately possible for reductions to map easy instances from the input domain to hard SAT instances. We develop a non-Hamiltonicity proof system and combine it with additional results concerning the Prover/Delayer game from the first part of this thesis as well as proof complexity results for intuitionistic logic in order to provide the first formal examples of harmful and beneficial reductions, ultimately leading to the development of a framework for studying and comparing translations from one language to another.

In this thesis we explore a number of ways in which combinatorial games can be used to help prove results in the area of propositional proof complexity. The results in this thesis can be divided into two sets, the first being dedicated to the study of Resolution space (memory) requirements, whereas the second is centered on formalizing the notion of `dangerous' reductions. The first group of results investigate Resolution space measures by asking questions of the form, `Given a formula F and integer k, does F have a [Type of Resolution] proof with [Type of Resource] at most k?'. We refer to this as a proof complexity resource problem, and provide comprehensive results for several forms of Resolution as well as various resources. These results include the PSPACE-Completeness of Tree Resolution clause space (and the Prover/Delayer game), the PSPACE-Completeness of Input Resolution derivation total space, and the PSPACE-Hardness of Resolution variable space. This research has theoretical as well as practical motivations: Proof complexity research has focused on the size of proofs, and Resolution space requirements are an interesting new theoretical area of study. In more practical terms, the Resolution proof system forms the underpinnings of all modern SAT-solving algorithms, including clause learning. In practice, the limiting factor on these algorithms is memory space, so there is a strong motivation for better understanding it as a resource. With the second group of results in this thesis we investigate and formalize what it means for a reduction to be `dangerous'. The area of SAT-solving necessarily employs reductions in order to translate from other domains to SAT, where the power of highly-optimized algorithms can be brought to bear. Researchers have empirically observed that it is unfortunately possible for reductions to map easy instances from the input domain to hard SAT instances. We develop a non-Hamiltonicity proof system and combine it with additional results concerning the Prover/Delayer game from the first part of this thesis as well as proof complexity results for intuitionistic logic in order to provide the first formal examples of harmful and beneficial reductions, ultimately leading to the development of a framework for studying and comparing translations from one language to another.

ropositional proof complexity is the study of the resources that are needed to prove formulas in propositional logic. In this thesis we are concerned with the size and space of proofs, and in particular with the latter. Different approaches to reasoning are captured by corresponding proof systems. The simplest and most well studied proof system is resolution, and we try to get our understanding of other proof systems closer to that of resolution. In resolution we can prove a space lower bound just by showing that any proof must have a large clause. We prove a similar relation between resolution width and polynomial calculus space that lets us derive space lower bounds, and we use it to separate degree and space. For cutting planes we show length-space trade-offs. This is, there are formulas that have a proof in small space and a proof in small length, but there is no proof that can optimize both measures at the same time. We introduce a new measure of space, cumulative space, that accounts for the space used throughout a proof rather than only its maximum. This is exploratory work, but we can also prove new results for the usual space measure. We define a new proof system that aims to capture the power of current SAT solvers, and we show a landscape of length-space trade-offs comparable to those in resolution. To prove these results we build and use tools from other areas of computational complexity. One area is pebble games, very simple computational models that are useful for modelling space. In addition to results with applications to proof complexity, we show that pebble game cost is PSPACE-hard to approximate. Another area is communication complexity, the study of the amount of communication that is needed to solve a problem when its description is shared by multiple parties. We prove a simulation theorem that relates the query complexity of a function with the communication complexity of a composed function. / <p>QC 20170509</p>

Our research is in the general area of String Algorithms and Combinatorics on Words. Specifically, we study a generalization of square-free strings, shuffle properties of strings, and formalizing the reasoning about finite strings. The existence of infinitely long square-free strings (strings with no adjacent repeating word blocks) over a three (or more) letter finite set (referred to as Alphabet) is a well-established result. A natural generalization of this problem is that only subsets of the alphabet with predefined cardinality are available, while selecting symbols of the square-free string. This problem has been studied by several authors, and the lowest possible bound on the cardinality of the subset given is four. The problem remains open for subset size three and we investigate this question. We show that square-free strings exist in several specialized cases of the problem and propose approaches to solve the problem, ranging from patterns in strings to Proof Complexity. We also study the shuffle property (analogous to shuffling a deck of cards labeled with symbols) of strings, and explore the relationship between string shuffle and graphs, and show that large classes of graphs can be represented with special type of strings. Finally, we propose a theory of strings, that formalizes the reasoning about finite strings. By engaging in this line of research, we hope to bring the richness of the advanced field of Proof Complexity to Stringology. / Thesis / Doctor of Philosophy (PhD)