# Does SAT always have short analytic proofs?

By analytic proof, I mean mainly resolution and also other valid syntactical manipulations of the set of clauses, old and new. So this is a search over problem space rather than solution space. The question is:

Is there a family of instances of SAT that doesn't have polynomial-size analytic proofs of their satisfiabilities?

If all families have short analytic proofs, then if we can find them in short time, that means P = NP. But even if there aren't always, there still may be other means to solve SAT in polynomial-time. So this is only one way to attack P vs. NP. But it's curious to know on its own.

• I guess this is open problem since there is no known polynomial way to show that SAT instance is unsatisfiable. Otherwise we'd have NP = coNP proof. But opposite also is unknown as we don't know if NP != coNP. Though, SAT may require exponentially long resolution proof. – rus9384 Mar 12 '18 at 11:20
• @rus9384: You are right: I am asking whether NP = coNP. It's not as hard as P vs. NP, but I didn't realize I was working on an open problem. I thought it was easy. – Zirui Wang Mar 12 '18 at 13:11
• I suggest reading some lecture notes on proof complexity, for example csc.kth.se/~jakobn/teaching/proofcplx11. The pigeonhole principle requires exponentially long Resolution refutations. – Yuval Filmus Mar 12 '18 at 13:44
• The answer might depend on exactly what you mean by "analytic proof". You never define that; you say "resolution and other syntactic manipulations", but you don't define which other manipulations you're willing to allow. The answer might depend on what other manipulations are allowed. Also, it's not clear whether you are asking only about proof of satisfiability (in which case a short such proof always exists) or also about proof of unsatisfiability (which is the interesting case). – D.W. Mar 12 '18 at 19:24
• That doesn't change the fact that it's not possible to "include every possible rule". There are infinitely many schemes of rules. For any scheme of rules you might imagine, I can imagine another rule not in the scheme (and indeed, another scheme not in the scheme). – D.W. Mar 19 '18 at 4:16

It is known that proofs of the unsatisfiability of pigeonhole problems must be at least length $2^{n^\epsilon}$ when the resolution proof system is used. $\epsilon$ depends on the difference between the number of pigeons and the number of holes, but $\epsilon > 0$ always.