@techreport{
    HUT-TCS-A90,
    author = {J{\"a}rvisalo, Matti},
    optmonth = "March",
    title = "Proof Complexity of Cut-Based Tableaux for {B}oolean Circuit Satisfiability Checking",
    url = "http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A90.shtml",
    abstract = "This report deals with propositional satisfiability checking. Most successful satisfiability checkers are based on the Davis--Putnam method and assume that the input formulae are in conjunctive normal form (CNF). In this work an alternative approach is considered. A tableaux--based method for a more general formula representation called Boolean circuits is introduced. The method can be seen as a generalisation of the Davis--Putnam method to Boolean circuits. \par The effectiveness of the tableau method is investigated. In particular, the role of the important splitting / cut rule is considered. The effect that restrictions on the use of the cut rule have on proof complexity, i.e., on the size of proofs producible, is studied. \par It is shown that restricting the application of the cut rule in any of the natural locality based ways considered causes an exponential increase in the proof complexity. Moreover, there are exponential differences between the proof complexity of all the restricted methods. The results rely on the resolution-boundedness of the methods and on properties of certain circuit families such as a Boolean circuit representation of the well-known pigeon-hole principle. \par The results apply to the Davis-Putnam method for formulae in CNF obtained from Boolean circuits using Tseitin's translation. Thus it is shown that locality based cut restrictions, such as splitting on the input gates only, increase the size of proofs exponentially in the worst-case in Davis-Putnam based satisfiability checkers.",
    year = "2004",
    number = "A90",
    institution = "Helsinki University of Technology, Laboratory for Theoretical Computer Science",
    note = "ISBN 951-22-7020-X",
    flags = "SERIES-A SA-53695 copy",
    address = "Espoo, Finland",
    keywords = "propositional satisfiability, satisfiability checking, Boolean circuits, cut rule, proof complexity, polynomial simulation, resolution, Davis-Putnam method",
    onlinenote = "Reprint of Master's thesis.",
    type = "Research Report",
    pages = "45"
}