Generating closed-form formulae that count satisfiable instances of k-SAT

The theory of NP-completeness is fundamental to computational complexity and the SATISFIABILITY problem of Boolean Logic is the seminal NP-complete problem on which the theory is based. While AT-completeness is associated more with the efficiency of deciding whether or not an arbitrary instance is satisfiable, determining the proportion of satisfiable instances of an equivalent problem, 3-SAT, yields important information in regards to this efficiency. Empirical research on the dependence of this proportion on the size of the 3-SAT instance has revealed a "satisfiability" phase transition through which dramatic changes in satisfiability accompany very small changes in problem size. This phenomenon underpins the celebrated threshold conjecture and in this paper we give a new way of attacking the conjecture by describing this transition algebraically. That is, we present and implement an algorithm that, for any given integer n, generates a closed form expression in m, (clause number), and k, (clause size), which counts the proportion of satisfiable instances of 3-SAT. The inherent complexity of the algorithm indicates that generating such a formula for n n greater than or equal to 5 is not feasible, but that, taking the form of a succinct mathematical expression, the algorithm is amenable to further asymptotic analysis. As part of this analysis we show that understanding the threshold amounts to understanding the asymptotics of an alternating sum of k-cylinders. All algorithms and experimentation have been implemented as part of an application package, SATPACK, more details of which appear in an extended version of this paper, (including all references), on the proceedings CD.