# Resolution complexity versus a constrained SAT algorithm

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?
• 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. – MGwynne Jun 5 '12 at 7:45
• Please incorporate your edits properly into the question. Keeping a backlog or highlighting new stuff is unnecessary, as we have a complete revision history. – Raphael Jun 6 '12 at 11:19

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.
• @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. – Opt Jun 5 '12 at 19:43