# 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
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8848277926445007, "perplexity": 853.4321514781698}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 20, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-43/segments/1570987822098.86/warc/CC-MAIN-20191022132135-20191022155635-00325.warc.gz"}