2
$\begingroup$

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.

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – rus9384 Mar 12 '18 at 11:20
  • $\begingroup$ @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. $\endgroup$ – Zirui Wang Mar 12 '18 at 13:11
  • $\begingroup$ 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. $\endgroup$ – Yuval Filmus Mar 12 '18 at 13:44
  • 1
    $\begingroup$ 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). $\endgroup$ – D.W.♦ Mar 12 '18 at 19:24
  • 1
    $\begingroup$ 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). $\endgroup$ – D.W.♦ Mar 19 '18 at 4:16
2
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Resolution is not everything, otherwise you will be able to conclude NP != coNP. $\endgroup$ – Zirui Wang Mar 16 '18 at 12:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.