Unrestricted vs restricted cut in a tableau method for Boolean circuits

ISSN： 1012-2443

Source： Annals of Mathematics and Artificial Intelligence, Vol.44, Iss.4, 2005-08, pp. : 373-399

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

This paper studies the relative efficiency of variations of a tableau method for Boolean circuit satisfiability checking. The considered method is a nonclausal 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 $\{\mathcal{C}_{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. 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.