@article{JJN:AMAI05,
    author = {Matti J{\"a}rvisalo and Tommi Junttila and Ilkka Niemel{\"a}},
    journal = {Annals of Mathematics and Artificial Intelligence},
    number = {4},
    pages = {373--399},
    title = {Unrestricted vs Restricted Cut in a Tableau Method 
	     for {B}oolean Circuits},
    volume = {44},
    year = {2005},
} 

Abstract:

This paper studies the relative efficiency of variations of a tableau 
method for Boolean circuit satisfiability checking. The considered 
method is a non-clausal generalisation of the 
Davis-Putnam-Logemann-Loveland (DPLL) procedure to Boolean circuits. The 
variations are obtained by restricting the use of the cut (splitting) 
rule in several natural ways. It is shown that the more restricted 
variations cannot polynomially simulate the less restricted ones. For 
each pair of methods T, T', an infinite family of circuits is devised for 
which T has polynomial size proofs while in T' the minimal proofs are of 
exponential size w.r.t. n, implying exponential separation of T and T' 
w.r.t. n.

The results also apply to DPLL for formulas in conjunctive normal form 
obtained from Boolean circuits by using Tseitin's translation. Thus DPLL 
with the considered cut restrictions, such as allowing splitting only on 
the variables corresponding to the input gates, cannot polynomially 
simulate DPLL with unrestricted splitting.