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.

• Type: Conference
• Year: 2004
• Where: AMAI
• Authors: Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä
• Keywords: AMAI 2004, Artificial Intelligence, Boolean Circuits, Cut Rule, Unrestricted Cut Rule