Proof Complexity of Cut-Based Tableaux for Boolean Circuit Satisfiability Checking

Reference:

Matti Järvisalo. Proof complexity of cut-based tableaux for Boolean circuit satisfiability checking. Research Report A90, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, March 2004.

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.

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.

Keywords:

propositional satisfiability, satisfiability checking, Boolean circuits, cut rule, proof complexity, polynomial simulation, resolution, Davis–Putnam method

Suggested BibTeX entry:

@techreport{HUT-TCS-A90,
    address = {Espoo, Finland},
    author = {Matti J{\"a}rvisalo},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {March},
    number = {A90},
    pages = {45},
    title = {Proof Complexity of Cut-Based Tableaux for {B}oolean Circuit Satisfiability Checking},
    type = {Research Report},
    year = {2004},
}