Sciweavers

Share
AMAI
2004
Springer

Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits

10 years 1 months ago
Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits
This paper studies the relative proof complexity of variations of a tableau method for Boolean circuit satisfiability checking obtained by restricting the use of the cut rule in several natural ways. The results show that the unrestricted cut rule can be exponentially more effective than any of the considered restrictions. Moreover, there are exponential differences between the restricted versions, too. The results also apply to the Davis-Putnam procedure for conjunctive normal form formulae obtained from Boolean circuits with a standard linear size translation.
Matti Järvisalo, Tommi A. Junttila, Ilkka Nie
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where AMAI
Authors Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä
Comments (0)
books