\documentclass{article} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{latexsym} \usepackage{graphics,color} \usepackage{enumerate} \setlength{\oddsidemargin}{.25in} \setlength{\evensidemargin}{.25in} \setlength{\textwidth}{6in} \setlength{\topmargin}{-0.5in} \setlength{\textheight}{8.5in} \newcommand{\header}{ \renewcommand{\thepage}{\arabic{page}} \noindent \begin{center} \framebox{ \vbox{ \hbox to 5.78in {\bf 6.841/18.405J: Advanced Complexity \hfill Monday, April 28th, 2003} \vspace{2mm} \hbox to 5.78in { {\Large \hfill Lecture 20: Proof Complexity, part I\hfill} } \vspace{2mm} \hbox to 5.78in { {\it Instructor: Eli Ben-Sasson \hfill Scribe: Samuel Fiorini} } } } \end{center} \vspace*{3mm} } \newtheorem{theorem}{Theorem} \newtheorem{claim}{Claim} \newtheorem{definition}{Definition} \newcommand{\qed}{\mbox{}\nolinebreak\hfill\rule{2mm}{2mm}\medbreak\par} \begin{document} \header \section{Introduction} Suppose we are given a Boolean circuit ${\cal C}(x_1,\ldots,x_n)$ (later $\mathcal{C}$ will be a CNF formula). Then any satisfying assignment $\alpha \in \{0,1\}^n$ is a short proof of the claim $$ \exists \alpha \in \{0,1\}^n: {\cal C}(\alpha)=1. $$ Hence the language SAT has short membership proofs. By definition, any language in NP has short membership proofs. However if we were to prove the claim $$ \forall \alpha \in \{0,1\}^n: {\cal C}(\alpha)=0, $$ then the simplest way would be to enumerate all possible assignments $\alpha \in \{0,1\}^n$. In other words, we can easily find exponential size membership proofs for co-SAT. Therefore a natural question is: ``given a circuit ${\cal C} \in$ co-SAT, what is the size of a shortest proof that ${\cal C} \in$ co-SAT?''. This is a central question in proof complexity. Let us now formally define proof systems. \medskip \noindent \textbf{Definition}. A \emph{proof system} $P$ (for \emph{co-SAT}) is a 2-tape Turing Machine $P(.,.)$ such that \begin{enumerate} \item (efficiency) $P$ runs in polynomial time in both inputs, \item (soundness and completeness) ${\cal C} \in$ co-SAT iff there exists a string $\pi$ such that $P({\cal C},\pi) = 1$. \end{enumerate} \medskip Observe that proof systems are not allowed to use randomness or interaction, and the size of the proof $\pi$ is not required to be polynomial in the size of the circuit ${\cal C}$. Adding this latter requirement gives the notion of `super' proof systems: \medskip \noindent \textbf{Definition}. A proof system $P$ is called \emph{super} if there exists a positive integer $k$ with the following property. For all circuits ${\cal C} \in$ co-SAT, there exists a proof $\pi_{\cal C}$ such that $|\pi_{\cal C}| \leq |{\cal C}|^k$ and $P({\cal C},\pi_{\cal C})=1$. \medskip The main open question of proof complexity can be now stated as~: ``does there exist a super proof system?''. This question is actually equivalent to NP $=?$ co-NP. \begin{theorem}[Cook,Reckhow] There exists a super proof system iff NP $=$ co-NP. \end{theorem} \noindent\textbf{Proof}. Assume there exists a super proof system. Then there exists a polynomial size proof that ${\cal C}$ is unsatisfiable for every circuit ${\cal C} \in$ co-SAT. Therefore co-SAT $\in$ NP, hence co-NP $\subseteq$ NP. Similarly it implies that SAT $\in$ co-NP, hence NP $\subseteq$ co-NP. Conversely, if co-NP = NP, then co-SAT $\in$ NP and there exists a verifier $V(.,.)$ for co-SAT that runs in polynomial time in the first input. Hence $V$ yields a super proof system. \qed The motivations of proof complexity include: \begin{enumerate} \item \emph{Circuit design}: suppose that we would like to verify that a circuit ${\cal C}$ computes a given function $f$ (e.g., that a certain chip really computes the product of two numbers). We would like to have an algorithm based on some proof system that could prove statements of the form $f \equiv \mathcal{C}$ as efficiently as possible. \item \emph{The \emph{NP $\nsubseteq$ P/poly} question}: empirically it seems to be a difficult question. But can we prove that there is something inherently difficult in it? It turns out that finite versions of this statement can be shown to be hard to prove for some fixed proof system. \item \emph{Automated theorem proving and related questions}: for instance, suppose there exists a short proof for a given statement, can we efficiently find such a proof? \item \emph{Analysis of algorithms for NP-complete problems}: the execution of such an algorithm (even if it is exponential) can be used to prove that a certain circuit in co-SAT is not satisfiable. Therefore lower bounds on the length of a proof give rise to lower bounds on the running time of the algorithm. \end{enumerate} \section{Resolution} >From now on, we restrict circuit $\mathcal{C}$ to be a CNF formula. Recall that a \emph{literal} is either a variable $x$ or its negation $\overline{x}$, a \emph{clause} is a disjunction of literals (sometimes encoded as a set of literals), and a \emph{CNF formula} is conjuction of clauses (which can also be encoded as a set of clauses). The resolution mechanism starts with the set of clauses of a given CNF formula and sequentially derives new clauses from previous clauses until it shows that, in a satisfying assignment, a certain variable has to be set to 0 and 1 at the same time. This proves the unsatisfiability of the formula. Let $\mathcal{C}$ be a CNF formula over the variables $x_1$, $x_2$, \ldots, $x_n$, a resolution proof uses the two following rules to generate new clauses: \begin{enumerate} \item \emph{Resolution Rule:} From any two clauses of the form $C \vee x_k$ and $D \vee \overline{x_k}$, derive $C \vee D$. This is often written $$ \begin{array}{r@{\hspace{-1em}}c@{\hspace{-1em}}l} C \vee x_k &&D \vee \overline{x_k}\\ \hline &C \vee D \end{array} $$ \item \emph{Weakening Rule:} From clause ${\cal C}$, derive clause ${\cal C} \vee \ell$, where $\ell$ is any literal. $$ \begin{array}{c} C\\ \hline C \vee \ell \end{array} $$ \end{enumerate} The weakening rule is not necessary to enforce the completeness of resolution, but it turns out to be useful in proofs. A \emph{resolution proof} (or \emph{refutation}) of \emph{length} $s$ for $\mathcal{C}$ is a sequence $\pi = (L_1,\ldots,L_s)$ of \emph{lines} such that \begin{enumerate}[(i)] \item each line is a clause, \item the last line $L_s$ is the empty clause $\emptyset$ (which is unsatisfiable by definition), \item each line $L_i$ is either an \emph{axiom} (that is, an element of $\mathcal{C}$) or derived from previous lines via the resolution or weakening rule. \end{enumerate} \noindent \textbf{Example.} Consider the CNF formula $\mathcal{C}$ on variables $x_1$, \ldots, $x_n$ with clauses $C_0 = \{x_1,x_2,\ldots,x_n\}$, $C_1 = \{\overline{x_1}\}$, $C_2 = \{\overline{x_2}\}$, \ldots, $C_n = \{\overline{x_n}\}$. We can prove that $\mathcal{C}$ is unsatisfiable by resolution as follows. First, apply the weakening rule to $C_0$ and $C_1$ to obtain the clause $\{x_2,x_3,\ldots,x_n\}$. Then apply the weakening rule to this new clause and $C_2$ to obtain the clause $\{x_3,x_4,\ldots,x_n\}$. Continue in a similar fashion until you infer the empty clause. The corresponding resolution proof is $\pi = (L_1,\ldots,L_{2n+1})$ with $$ L_i = \left\{ \begin{array}{ll} C_{i-1} &\textrm{if } 1 \le i \le n+1,\\ \{x_1,x_2,\ldots,x_n\} \setminus \{x_1,\ldots,x_{i-n-1}\} &\textrm{if } n+2 \le i \le 2n+1. \end{array} \right. $$ \begin{center} \input{l20-tree-like.pstex_t} \end{center} A resolution proof gives rise to a DAG (Directed Acyclic Graph) called the \emph{proof-DAG}. The nodes of the DAG are the lines of the proof, and a node has one edge coming in from each one of the premises it was derived from. Thus, the \emph{sources} of the proof-DAG are the axioms, and the DAG has a single sink node, which is labeled $\emptyset$. We allow to label more than one node with the same axiom. A proof is said to be tree-like if its DAG is a tree. For instance, the above proof is tree-like. In general, resolution proofs are not necessarily tree-like. Although there are contradictions $\mathcal{C}$ which admit small (linear length) resolution proofs but need long (exponential length) tree-like resolution proofs, tree-like resolution is very interesting from a theoretical and practical point of view. For instance, most known SAT algorithms (such as the DLL and DP algorithms) use tree-like resolution. \section{Complexity measures} Let $\mathcal{C}$ be a CNF formula. Then we define $$ \begin{array}{rcl} S_R(\mathcal{C}) &=& \textrm{min size of a resolution proof for } \mathcal{C},\\ S_T(\mathcal{C}) &=& \textrm{min size of a tree-like resolution proof for } \mathcal{C},\\ \textrm{width}(\mathcal{C}) &=& \displaystyle \min_{\pi\, \mathrm{proof}\, \mathrm{for}\, \mathcal{C}} (\textrm{max width of a line in } \pi), \end{array} $$ where the \emph{size} of a proof is the number of symbols in it (this measure is polynomially related to the length for resolution proofs), the \emph{width} of a clause is the number of literals in it. By convention, all above quantities equal $\infty$ if $\mathcal{C}$ is satisfiable. At first sight, it may seem that $S_T(\mathcal{C})$ and $S_R(\mathcal{C})$ are the most interesting parameters, but it turns out that $\textrm{width}(\mathcal{C})$ is also very interesting in that lower bounds on $\textrm{width}(\mathcal{C})$ are often easier to obtain and yield lower bounds on $S_T(\mathcal{C})$ and $S_R(\mathcal{C})$. \section{Completeness of proof by resolution} \begin{theorem} A CNF formula is unsatisfiable if and only if it admits a resolution proof. \end{theorem} \noindent \textbf{Proof.} The backwards implication follows directly from the soundness of the resolution and weakening rules, so let's do the forward implication. Let $\mathcal{C}$ be a CNF formula on variables $x_1$, \ldots, $x_n$. If $n = 0$ then $\mathcal{C}$ has only one clause, namely the empty clause, so it has a one line resolution proof. Now assume that $n \ge 1$ and every unsatisfiable CNF formula with $n-1$ variables has a resolution proof. We will construct a CNF formula $\mathcal{C}'$ such that (i) $\mathcal{C}'$ has $n-1$ variables, (ii) $\mathcal{C}'$ is derived from $\mathcal{C}$ by the resolution rule (we won't use the weakening rule), and (iii) $\mathcal{C}'$ is unsatisfiable. Let $$ \mathcal{C}' = \bigwedge_{\alpha \in \{0,1\}^{n-1}} C'_{\alpha} $$ for some clauses $C'_\alpha$ to be determined. Fix $\alpha \in \{0,1\}^{n-1}$. Because $\mathcal{C}$ is unsatisfiable, it must possess clauses $C_0$ and $C_1$ such that $C_0(\alpha,0) = C_1(\alpha,1) = 0$. \begin{enumerate}[{Case} 1.] \item If $x_n$ is not a literal of $C_0$ then we set $C'_\alpha = C_0$ ($\overline{x_n}$ cannot be a literal of $C_0$). \item If $\overline{x_n}$ is not a literal of $C_1$ then we set $C'_\alpha = C_1$ ($x_n$ cannot be a literal of $C_1$). \item Otherwise $C_0 = C'_0 \vee x_n$ and $C_1 = C'_1 \vee \overline{x_n}$ for some clauses $C'_0$ and $C'_1$ on $x_1$, \ldots, $x_{n-1}$. We then derive $C'_\alpha = C'_0 \vee C'_1$ by one application of the resolution rule. \end{enumerate} This concludes the construction of $\mathcal{C}'$. By induction, we know that $\mathcal{C}'$ has a resolution proof $\pi'$. We can find a proof for $\mathcal{C}$, for instance, by inserting in $\pi'$ all the axioms of $\mathcal{C}$ and then the clauses of $\mathcal{C}'$ which are derived from two axioms of $\mathcal{C}$ by the resolution rule. \qed \noindent \textbf{Example}. For $i \in {1, \ldots, n}$ and $\alpha \in \{0,1\}^n$, let $\ell_{\alpha,i} = x_i$ if $\alpha_i = 0$ and $\ell_{\alpha,i} = \overline{x_i}$ if $\alpha_i = 1$. Then define $$ C_\alpha = \bigvee_{i=1}^n \ell_{\alpha,i} \qquad \textrm{and} \qquad \mathcal{C} = \bigwedge_{\alpha \in \{0,1\}^n} C_\alpha. $$ The `universal formula' $\mathcal{C}$ has $2^n$ clauses, each of width $n$. Each of its clauses $C_\alpha$ satisfies all assignments except $\alpha$. It follows that $\mathcal{C}$ has no resolution proof of length less than $2^n$. \medskip The above formula has no short resolution proof in terms of $n$, but is itself very long. Can we find short CNF formulas that have long resolution proofs~? Random CNF formula have been proved to be hard for resolution, but there are also explicit examples of CNF formulas which require long resolution proofs, as we will see now. \section{Formulas which are hard for resolution} The \emph{pigeonhole principle} says that it is impossible to squeeze $n+1$ pigeons in $n$ holes if no two pigeons fit in one hole. We can express the pigeonhole principle by a CNF formula $\textrm{PHP}_n$ as follows. $\textrm{PHP}_n$ lies and says ``there is a way to squeeze $n+1$ pigeons in $n$ holes''. For each pigeon $i \in \{1,\ldots,n+1\}$ and hole $j \in \{1,\ldots,n\}$, formula $\textrm{PHP}_n$ has a variable $x_{ij}$. The interpretation of $x_{ij}$ is: $x_{ij} = 1$ if pigeon $i$ is in hole $j$. Then we can express ``pigeon $i$ occupies at least one hole'' by a clause $P_i = \bigvee_{j=1}^n x_{ij}$ and ``pigeons $i$ and $i'$ are not both in hole $j$'' by a clause $H_{i,i',j} = \overline{x_{ij}} \vee \overline{x_{i'j}}$. Then $$ \textrm{PHP}_n = \left(\bigwedge_{1 \le i \le n+1} P_i \right) \wedge \left(\bigwedge_{1 \le i \neq i' \le n+1 \atop 1 \le j \le n} H_{i,i',j}\right) $$ expresses what we want. \begin{theorem}[Haken 1989] $S_R(\textrm{PHP}_n) = 2^{\Omega(n)}$. \end{theorem} So $\textrm{PHP}_n$ is indeed hard for resolution. But there are more CNF formulas which are hard for resolution: \begin{theorem}[Raz 2002] Resolution cannot efficiently prove statements of the type ``function $f$ is not in P$/$poly''. \end{theorem} There are two ways to interprete this results: (i) it is hard to prove circuit lower bounds, (ii) resolution is weak. (Interestingly, Ran Raz derived the latter result from a lower bound on the minimum length of a resolution proof for the \emph{weak pigeonhole principle}.) This is related to work by Razborov and Rudich on `natural proofs'. They showed that all known circuit lower bounds have certain `natural' properties, and that the existence of hard functions contradicts the existence of natural proofs of general circuit lower bounds. Thus, a circuit lower bound for arbitrary circuits might require some totally new proof techniques. The ultimate goal in this direction, which currently seems well beyond our reach, is to prove the \emph{independence} of the claim P $\neq$ NP from some strong first order theory, such as ZFC. \section{Two techniques for obtaining lower bounds} In the next lecture, we will prove lower bounds for the resolution proof system. Given a CNF formula $\mathcal{C}$, we want to know what is it about the structure of $\mathcal{C}$ that makes it hard to prove for a fixed proof system like resolution. There are two general approaches: \begin{enumerate} \item investigate the combinatorics of DAG-proofs; \item use the interpolation method. \end{enumerate} The interpolation method implements a natural idea that fails at some point: connect CNF formulas to circuits and use circuit lower bounds. The basic argument here is ``if this CNF formula has a short proof, then some function can be computed by a small circuit''. Consider an unsatisfiable CNF formula $\mathcal{C}$ of the form $\mathcal{C} = \mathcal{C}_0(x,y) \wedge \mathcal{C}_1(x,z)$. Kraj\'\i \v{c}ek's theorem says that if we have a short resolution proof for $\mathcal{C}$ then there exists a small circuit that determines which one of $\mathcal{C}_0$ or $\mathcal{C}_1$ is not satisfiable when the $x$ variables have been fixed to some given truth values. \begin{theorem}[Kraj\'\i \v{c}ek's interpolation theorem] If $\mathcal{C} = \mathcal{C}_0(x,y) \wedge \mathcal{C}_1(x,z)$ has a resolution proof of length $s$ (so, in particular, $\mathcal{C}$ is unsatisfiable), then there exists a circuit $S(x)$ of size at most $s$ that computes, for each $\alpha \in \{0,1\}^{|x|}$, an index $i = S(\alpha)$ with the following property: if $i=0$ then $\mathcal{C}_0(\alpha,y)$ is unsatisfiable; if $i=1$ then $\mathcal{C}_1(\alpha,z)$ is unsatisfiable. \end{theorem} Note that the interpolation method fails for proof systems which are stronger than resolution. \end{document}