Stålmarck's Method Versus Resolution: a Comparative Theoretical Study

This Master’s thesis presents a comparative analysis of St˚almarck’s proof methodand resolution from a theoretical perspective.We give (to our knowledge) the first complete explicit formal descriptionof the dilemma proof system underlying St˚almarck’s method. Based on thisdescription we prove a number of simulation and separation results betweendifferent subsystems of dilemma (defined by restrictions on possible branchingassumptions and rules for merging the results derived in distinct branches).The key result of the thesis is that dilemma depth translates into resolutionwidth. More precisely, a dilemma refutation in depth d and length L of ak-CNF formula F can be transformed to a resolution refutation of F in widthO (kd) and lengthLkdO(1).From this depth-width relation it follows that for k-CNF formulas withk fixed, resolution p-simulates dilemma restricted to minimum-depth proofs.Furthermore, the running time of the minimum-width proof search algorithmsuggested by Ben-Sasson and Wigderson is shown to be polynomial in the running time of St˚almarck’s method.Finally, using results by Beame et al. we show that if F is a uniformly random3-CNF formula with ∆n clauses on n variables, then with high probability itholds for the dilemma hardness HD (F) that Ωn/∆2+≤ HD (F) ≤ O (n/∆)(where is an arbitrarily small but positive constant)