EDIT: ad hoc speed-ups are excluded.

We have the result that propositional resolution requires exponential time. The resolution result uses the proof of the pigeonhole principle as an example of a proof that takes exponential time.

Let's also say we have a hypothetical algorithm M for SAT that runs in polynomial time. EDIT : M is correct, complete, sound, and general-purpose; it contains no ad hoc speed-up rules for the pigeonhole principle or any other theorem that requires exponential length in resolution. M takes its input in clausal form; we'll set up the input like a resolution proof where the consequent is negated to lead to unsatisfiability if the theorem is true. Now let's consider how the proof of the pigeonhole principle works in algorithm M with a strong condition C added:

C. We are given that M simply transforms one clause (or set of clauses) to another clause (or set of clauses). Every such transformation is logically sound.

Some questions; please point out the most fatal flaws:

  1. Given condition C above, and since M's rule system must be finite, correct, and complete, can we conclude that there is a translation from M's rule system to an equivalent set of expansions based on resolution?
  2. Are we now in a place where we can conclude that M would produce a computation that could be mapped by the translation in point 1 above into an impossible polynomial-time resolution proof of the pigeonhole principle?
  • $\begingroup$ Isn't an M which just returns the clause-set with the empty clause if the input is unsatisfiable a valid solver in this case (i.e., it satisfies C)? Surely this doesn't allow translation to a polynomially sized resolution proof as, as you've said, the pigeon-hole formulas require exponential size resolution proofs. $\endgroup$
    – MGwynne
    Commented Jun 5, 2012 at 7:45
  • $\begingroup$ Please incorporate your edits properly into the question. Keeping a backlog or highlighting new stuff is unnecessary, as we have a complete revision history. $\endgroup$
    – Raphael
    Commented Jun 6, 2012 at 11:19

1 Answer 1

  1. While the deductions made by $M$ can have equivalent (possibly exponentially bigger) resolution proofs, I'm not sure what you mean by translating the rule system of $M$ into resolution form. If $M$ has a rule saying that if the problem is a PHP (pigeonhole principle) problem then output unsat if number of pigeons > number of holes, how would you translate that rule into resolution form?

    Edit: To elaborate on the last point, we know that Extended Resolution (ER) which in a nutshell, allows one to add new variables, has polynomial-size PHP proofs. Now suppose, $M$ uses ER to prove PHP. Such reasoning cannot be "directly" translated into a resolution proof as that would require adding new variables to the formula which is not allowed in pure resolution proofs.

  2. As I mentioned in point 1, you can translate the deductions by $M$ into resolution proofs of those deductions but the resolution proof might be exponentially larger.

  • $\begingroup$ The question has been edited to address this. $\endgroup$
    – ShyPerson
    Commented Jun 5, 2012 at 19:04
  • $\begingroup$ @ShyPerson: For the edited question, if all the deductions that can be made by $M$ can be performed using polynomial-size resolution proofs, then $M$ cannot prove PHP as that would lead to a polynomial-size resolution proof for PHP which is impossible. $\endgroup$
    – Opt
    Commented Jun 5, 2012 at 19:43
  • $\begingroup$ Great! We're extremely close now to the heart of the question. Can we conclude that any rule system obeying the constraints on M must reduce to polynomial-size resolution proofs? $\endgroup$
    – ShyPerson
    Commented Jun 5, 2012 at 21:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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