Let $F = C_1 \wedge C_2\; \wedge ... \wedge\; C_m$ be a unsatisfiable $k$-CNF on variables $x_1,...,x_n$, where $k$ is constant.

Let $x_j\rightarrow x_j^1\wedge x_j^2$ be a substitution that replaces each variable $x_j$ in with the conjunction $x_j^1\wedge x_j^2$, where $x_j^1$ and $x_j^2$ are two new variables. Let $G$ be the formula which is obtained from $F$ by applying the substitution above to all variables, and then converting it back to a CNF formula.

Clearly, $F$ is unsatisfiable if and only if $G$ is unsatisfiable. Additionally, $G$ is a $O(k)$-CNF with at most $2^{k}\cdot m$ clauses, since intuitively each clause of F is expanded into at most $2^{k}$ clauses.

Question: Suppose we have a resolution refutation $P$ for $F$ of size $s$. Can $P$ be converted into a resolution refutation for $G$ of size $s^{O(1)}$?

I feel that there might be a standard trick for getting such conversion but I couldn't find any reference. The idea I had in mind was to apply the substitution on each clause appearing in the proof, and then use the fact that resolution is implicationally complete. But this would only work for refutations of small width, since each clause of width $r$ may be get expanded into up to 2^r clauses.

References or suggestions are very welcome.

  • 1
    $\begingroup$ Check papers by Nordstrom on space complexity of resolution. It is more common to use xor in place of and. The idea goes back to Sherstov AFAIK and is called lifting in Boolean function analysis and communication complexity. $\endgroup$ – Kaveh Aug 1 '15 at 15:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.