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:

• 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?

• 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?

-
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.

-
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.

StackExchange Computer Science Q#2230, answer score: 5