This thesis 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 thesis 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.

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.

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.

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.

@**mastersthesis**{*JarvisaloMsc*,

**author** = {Matti J{\"a}rvisalo},

**pages** = {v+56},

**school** = {Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science},

**title** = {Proof Complexity of Cut-Based Tableaux for {B}oolean Circuit Satisfiability Checking},

**year** = {2004},

}