Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits (2005)
AUTHORS:
Järvisalo Matti
,
Junttila Tommi
,
Niemelä Ilkka
JOURNAL:
Annals of Mathematics and Artificial Intelligence
VOLUME:
44
PAGES:
373--399
URL:
http://www.tcs.hut.fi/~mjj/publications_by_type.shtml
@article{ JJN:AMAI05, author = {J{\"a}rvisalo, Matti and Junttila, Tommi and Niemel{\"a}, Ilkka}, optmonth = "August", title = "Unrestricted vs Restricted Cut in a Tableau Method for {B}oolean Circuits", url = "http://www.tcs.hut.fi/~mjj/publications_by_type.shtml", journal = "Annals of Mathematics and Artificial Intelligence", number = "4", 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 $\{\Circuit_n\}$ 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$. \par 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.", volume = "44", flags = "SA-53695 public copy", year = "2005", keywords = "satisfiability, Boolean circuits, cut rule, proof complexity, DPLL", onlinenote = "See URL above for a preliminary version", pages = "373--399" }