Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits

Reference:

Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Unrestricted vs restricted cut in a tableau method for Boolean circuits. Annals of Mathematics and Artificial Intelligence, 44(4):373–399, 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 , , an infinite family of circuits is devised for which has polynomial size proofs while in the minimal proofs are of exponential size w.r.t. , implying exponential separation of and w.r.t. .

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.

Keywords:

satisfiability, Boolean circuits, cut rule, proof complexity, DPLL

Suggested BibTeX entry:

@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},
}