@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.