We changed our privacy policy. Read more.
19

The most natural restriction on the proof DAG is that it be a tree – that is, any "lemma" (intermediate conclusion) is not used more than once. This property is called being "tree-like". General resolution is exponentially more powerful than tree-like resolution, as shown for example by Ben-Sasson, Impagliazzo and Wigderson. The concept has also been ...


19

The basic sum-of-squares proof system, introduced under the name of Positivstellensatz refutations by Grigoriev and Vorobjov, is a “static” proof system for showing that a set of polynomial equations and inequations $$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ where $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$, has no common solution in $\...


14

1, 2, 4) The best known lower bounds on extended Frege are the same as for Frege: linear number of lines, and quadratic size. This applies e.g. to the tautologies $\neg^{2n}\top$ (basically, any tautology that is not a substitution instance of a shorter tautology, and whose sum of lengths of all subformulas is quadratic). This is proved in Krajíček’s Bounded ...


12

It depends on what kind of a "beginner" level you wish to have. I don't think there is a real good undergraduate level text on proof complexity (this is probably true for most specialized sub-areas in complexity). But for a beginner (graduate level) sources, I would recommend, something like understanding well the basic exponential size lower bound on ...


12

SOS can be considered as a proof system where lines are of the form $p(\vec{x}) \geq 0$ where $p(\vec{x})$ is a polynomial in variables $\vec{x}$. The inference rules are: $\over x^2-x \geq 0$ $\over x-x^2 \geq 0$ $\over p(\vec{x})^2\geq 0$ $p(\vec{x}) \geq 0 \over p(\vec{x})x \geq 0$ $p(\vec{x}) \geq 0 \over p(\vec{x})(1-x) \geq 0$ $p_1(\vec{x}) \geq 0, \...


10

How about the edge coloring number in a dense graph (aka Chromatic index)? You are given the adjacency matrix of an $n$ vertex graph ($n^2$ bit input), but the natural witness describing the coloring has size $n^2\log n$. Of course, there might be shorter proofs for class 1 graphs in Vizing's theorem. See also this possibly related question


9

Natural examples of propositional proof systems that do not fall under this definition are algebraic proof systems where the lines in the proof are arbitrary polynomials (not necessarily fully expanded). To verify the correctness of such proofs, among other things one has to test the identity of polynomials, which is not known to be possible in deterministic ...


8

Here is an example, which appears a natural problem. Instance: Positive integers, $d_1,\ldots,d_n$ and $k$, all bounded from above by $n$. Question: Does there exist a $k$-colorable graph with degree sequence $d_1,\ldots,d_n$ ? Here the input can be described with $O(n\log n)$ bits, but the witness may require $\Omega(n^2)$ bits. Remark: I do not have ...


8

I came along some quite natural NP-complete problems that seemingly require long witnesses. The problems, parameterized by integers $C$ and $D$ are as follows: Input: A one-tape TM $M$ Question: Is there some $n\in\mathbb{N}$, such that $M$ makes more than $Cn+D$ steps on some input of length $n$? Sometimes the complement of the problem is easier to state: ...


8

Müller and Szeider study Resolution proofs where the proof DAG has bounded tree-width or bounded path-width (for suitable extensions of these graph complexity measures to directed graphs.) They show that the path-width of the DAG is essentially the same as the space complexity of the proof, and define a generalized notion of proof space which is equivalent ...


7

First, ER p-simulates SR: for example, ER is p-equivalent to the extended Frege proof system (EF) which is p-equivalent to the substitution Frege proof system (SF), and it is easy to see that SF p-simulates SR (the symmetry rule amounts to substitution of a special kind). On the other hand, Urquhart [1] proves an exponential lower bound on SR refutations of ...


6

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity class $\mathsf{P/poly}$. We have to look at their uniform counterparts: E.g. the proof complexity counterpart for $\mathsf{P}$ are bounded arithmetic theories ...


6

I find these introductory lecture notes easy to read: Paul Beame's IAS Lectures


6

For the more algebraic side of proof complexity I recommend starting with Pitassi's 1996 survey paper: T. Pitassi. Algebraic propositional proof systems, in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Volume 31, Descriptive Complexity and Finite Models, Immerman and Kolaitis (Eds.), pp. 215-244, 1996. For a quick overview you ...


6

Maybe this is a silly "reason/explanation", but for many NP-Complete problems, a solution is a subset of the input (knapsack, vertex cover, clique, dominating set, independent set, max cut, subset sum, ...) or a permutation of or assignment to a subset of the input (Hamiltonian path, traveling salesman, SAT, graph isomorphism, graph coloring, ...). We could ...


6

$f$ is not a prover, it's a proof-checker. $w$ is the proof. And the polynomial is a polynomial of the length of the proof, which could be much larger than the length of the thing being proved. If you have a proof system for which checking whether something really is a proof (or figuring out what it's a proof of) takes more than polynomial time, then your ...


6

For strong enough proof systems the graph representation of a proof in the system seems less consequential, since (as Joshua Grochow already commented), DAG-like and tree-like Frege proofs are polynomially equivalent (see Krajicek's 1995 monograph for a proof of this fact). For weaker proof systems such as resolution, tree-like is exponentially weaker than ...


6

With the caveat that I am posting this quickly in a sleep-deprived state, I think the answer is "no" to all three questions. Take the pigeonhole principle formulas PHP^m_n for m pigeons and n holes. The miniminal length of a resolution refutation for m = n+1 is exp(Omega(n)) by Haken. However, Buss and Pitassi proved that for m = exp(\sqrt(n log n)) pigeons ...


6

For each of these proof systems we know that there are some formulas where the shortest proof needs to have exponential length. Some of the earliest examples are an exponential lower bound for the pigeonhole principle in polynomial calculus (Razborov '98, IPS '99), and an exponential lower bound for the clique-colouring formula in cutting planes (Pudlák '99)....


5

The most recent and up-to-date general-purpose proof complexity survey is probably that of Nathan Segerlind: Nathan Segerlind: The Complexity of Propositional Proofs. Bulletin of Symbolic Logic 13(4): 417-481, 2007 (http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps). And now, warnings for two shameless self plugs… An even more recent survey, but ...


4

In Cook-Reckhow propositional proof systems proof checkers have to run in polynomial time w.r.t. the size of their input. The size of the input is the size of the proof. This is generally not a restriction: if we have a proof verifier algorithm $Q$ that does not run in polynomial time we can define a new proof verifier algorithm $Q'$ which accepts the ...


3

The statement is false for any polynomial time recognizable family of tautologies: the proof system will simply check if the formula is one of them and accept if it is. Proof length of them will be O(1). So I don't think any explicit example is known. Recall that we don't even know if SAT $\notin$ DTime(O(n)) so we also don't know if SAT$\notin$ coNTime(O(n)...


3

Here is a recent one: http://link.springer.com/chapter/10.1007%2F978-3-319-09284-3_17 You can get the fulltext here: http://arxiv.org/abs/1402.2184 It uses some state-of-the-art SAT solvers (see http://fmv.jku.at/lingeling/) to solve a member of a family of problems called "Erdős Discrepancy Conjecture". They encoded the problem as SAT instances and the SAT ...


3

As for your first question, Allender states (in Amplifying Lower Bounds by Means of Self-Reducibility) that no natural NP-complete problem is known to lie outside of NTIME(n). This means that all known natural NP-complete sets have linear size witnesses.


3

You have a non-deterministic algorithm deciding the problem. If you want to think of it as a proof system for $EQUIV$, then the proof of $(u,v) \in EQUIVE$ is just the string representing the computation of your algorithm on $(u,v)$. The proof checker just checks that the given string is in fact an accepting computation of your algorithm on $(u,v)$. Use ...


3

First, Kaveh is correct that the verification for IPS is randomized, so all it would show is $\mathsf{NP} \subseteq \mathsf{coAM}$ (not $\mathsf{NP} = \mathsf{coNP}$). However, this alone would still be enough to collapse the polynomial hierarchy. Second, I think the actual thing you are missing here is that the IPS proofs they give have size polynomial in ...


2

I think what you are missing is probably the complexity of the proof verification algorithm for IPS. It is generally true that if we have a Cook-Reckhow proof system and have short proofs for a coNP-complete problem (e.g. TAUT) then that would imply NP=coNP. But not every proof system is a Cook-Reckhow proof system, e.g. it can be the case that the proofs ...


2

Kaveh's response exemplifies well the Cook-Reckhow notion of an abstract proof system. Nonetheless, for comparison, I point to a recent preprint of mine and Damien Pous: A cut-free cyclic proof system for Kleene Algebra Here we give a more traditional bona fide proof system for equivalence of regular expressions by allowing non-wellfounded reasoning in ...


2

Your question is like asking what is the class of formulas for the problem SAT? In the definition of SAT it is fixed to some fixed class, say those based on $\{\lnot, \land, \lor\}$ but it doesn't really matter usually whether we talk about formulas based on $\{\lnot, \land, \lor\}$ or $\{\bot, \to \}$ or any other complete set of Boolean connectives. ...


2

Assume that you have an algorithm $A$ which satisfies soundness and completeness. You can define a new proof checker which is sound, complete, and runs in polynomial time: it checks if a given $\pi$ is a accepting computation history of $A$ which can be done in polynomial time (in fact $AC^0_2$). The take away is if a proof system is not polynomial time ...


Only top voted, non community-wiki answers of a minimum length are eligible