Satisfiability, branch-width and Tseitin tautologies

For a CNF τ, let w_b(τ) be the branch-width of its underlying hypergraph. In this paper we design an algorithm for solving SAT in time n^O(1)2^O(w(b)(τ)). This in particular implies a polynomial algorithm for testing satisfiability on instances with tree-width O(log n). Our algorithm is a modification of the width based automated theorem prover (WBATP) which is a popular (at least on the theoretical level) heuristic for finding resolution refutations of unsatisfiable CNFs. We show that instead of the exhaustive enumeration of all provable clauses, one can do a better search based on the Robertson-Seymour algorithm for approximating the branch-width of a graph. We call the resulting procedure Branch-Width Based Automated Theorem Prover (BWBATP). As opposed to WBATP, it always produces regular refutations. Perhaps more importantly, the running time of our algorithm is bounded in terms of a clean combinatorial characteristic that can be efficiently approximated, and that the algorithm also produces, within the same time, a satisfying assignment if τ happens to be satisfiable. In the second part of the paper we investigate the behavior of BWBATP on the Well-studied class of Tseitin tautologies. We argue that in this case BWBATP is better than WBATP. Namely, we show that its running time on any Tseitin tautology τ is |τ|^O(1). 2^O(w(τ├O)) as opposed to the obvious bound n^O(w(τ├O)) provided by WBATP. This in particular implies that Resolution is automatizable on those Tseitin tautologies for which we know the relation w(τ├φ) ≤ O(log S(τ)). We identify one such subclass and prove partial results toward establishing this relation for larger classes of graphs.