Do we know something about this refutation method for SAT?

Question

Let we have a formula $\varphi(x_1,x_2...x_k)$. Now we apply a refutation method: $\varphi(x_1,x_2...x_k)\Leftrightarrow(\varphi(x_1=1,x_2...x_k)\lor\varphi(x_1=0,x_2...x_k))$. Latter formula seems to be longer, but no, good algorithm reduces number of literal occurences. On each step we can modify the formula without changing it's solution space. This gives much more power than resolution has. For example, Tseytin contradiction can be refuted this way in linear time using deterministic algorithm.

But what is the worst case for this algorithm?

Example:

$$\varphi=(x\lor y\lor z)(x\lor\overline y\lor t)(x\lor\overline z\lor\overline v)(\overline x\lor\overline t\lor\overline v)(\overline x\lor\overline z\lor v)(y\lor\overline z\lor v)(\overline y\lor\overline t\lor\overline v)\land(\overline y\lor z\lor t)$$

Step 1. Getting rid of $t$.

Putting $t$. Affected remaining clauses: $(\overline x\lor\overline v)(\overline y\lor\overline v)$. Reducing them: $\overline v\lor \overline x\overline y$.

Putting $\overline t$. Affected remaining clauses: $(x\lor\overline y)(\overline y\lor z)$. Reducing them: $\overline y\lor xz$.

Combining them using OR: $\overline v\lor\overline y\lor xz$.

Step 2. Getting rid of $y$.

Putting $y$. Affected subformula: $\overline v\lor xz$.

Putting $\overline y$. Affected subformula: $(x\lor z)(\overline z\lor v)$.

Combining them: $\overline v\lor xz\lor(x\lor z)(\overline z\lor v)$. Reduction: $x\lor z\lor\overline v$.

Step 3. Getting rid of $x$.

Putting $x$. Affected subformula: $\overline z\lor v$.

Putting $\overline x$. Affected subformula: $(z\lor \overline v)(\overline z\lor\overline v)$. Reduction: $\overline v$.

Combining them: $1$.

All clauses are covered, formula is satisfiable.

But what would be the hardest case for this and is it possible to break exponential bound using this method? Is this method general enough (we can modify formula by any ways until solution space is unchanged and this is checkable in polynomial time) that saying it requires superpolynomial time (for unsatisfiable formula) will imply $\mathsf{NP\ne coNP}$?

Note that for unsatisfiable formula it's possible to non-deterministically ignore some clauses if refutation can be done without their usage.

Answer 1

As far as I can tell the earliest mention of the procedure you outline, later described in the literature as variable elimination by clause distribution, was in the paper "ZRes: The old Davis-Putnam procedure meets ZBDD" by Philippe Chatalic and Laurent Simon. The procedure was described again, along with other formula simplification techniques, in "Effective Preprocessing in SAT through Variable and Clause Elimination" by Niklas Eén and Armin Biere.

The procedure was shown to be a workable way to improve SAT solver performance if care is taken to minimize clause growth as the implicants of removed terms are distributed, or to use data structures that efficiently manage large clause sets.

Answer 2

The worst case is exponential. Each time you apply your method to a single variable, you are potentially doubling the size of the formula. You might need to apply this to each of the $k$ variables, so the size of the formula might blow up by a factor of $2^k$. In other words, the running time of this algorithm could potentially be exponential.

What you have described is basically a variation on the DPLL algorithm. The DPLL algorithm picks an variable, say $x_1$, sets it first to true, simplifies, and tests satisfiability of that; then sets it to false, simplifies, and tests satisfiability of that. That's very similar to what you are doing. An important choice here is exactly what simplification we do; you didn't describe that explicitly, but you can find a description of the specific simplifications that are done in the DPLL algorithm can be found in any good reference on DPLL. DPLL is probably better than your method because it separately simplifies $\phi(0,x_2,\dots,x_k)$ and simplifies $\phi(1,x_2,\dots,x_k)$, which is potentially easier than simplifying the combined formula $\phi(0,x_2,\dots,x_k) \lor \phi(1,x_2,\dots,x_k)$ (depending on what simplification rules you use).