Mathematics desk
< October 27	<< Sep \| October \| Nov >>	October 29 >

Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is an archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

October 28

Resolution Lower Bound Example

I am looking for an example of a 3-CNF formula, $\varphi$ , and a clause $C$ with at most 3 variables, that can be derived from $\varphi$ using resolution, and any resolution derivation of $C$ from $\varphi$ must derive also some 5-variable clause (in some derivation step).

For example, any derivation of $C=(b+c+d)$ from $\varphi =(a+b+c)({\bar {a}}+d+e)(b+c+{\bar {e}})$ must derive also some 4-variable clause (i.e, must derive either $(b+c+d+e)$ or $({\bar {a}}+d+b+c)$ ). עברית (talk) 14:46, 28 October 2017 (UTC)[reply]

Try

C=(c+d+e)

and

\varphi =(b+h+i)(c+f+{\bar {h}})(d+e+{\bar {f}})(c+g+{\bar {i}})(d+e+{\bar {g}})({\bar {b}}+c+j)(d+e+{\bar {j}}).

Not my area of expertise and I only checked by hand so there could have been errors, but allowing only clauses with 4 or fewer variables seems to only lead to dead ends no matter which order you eliminate the variables. No real methodology here, just took an expression with a 5 term clause, where the expression resolves to a 3 term clause, then added more variables to get an expression with only 3 term clauses, then checked for alternate derivations with no 5 term clauses. Seems like with a bit more systematic approach you could generate expressions which require clauses of arbitrary length. --RDBury (talk) 06:55, 29 October 2017 (UTC)[reply]