A complexity index for satisfiability problems

This paper associates a linear programming problem (LP) to any conjunctive normal form p, and shows that the optimum value Z(p) of this LP measures the complexity of the corresponding SAT (Boolean satisfiability) problem. More precisely, there is an algorithm for SAT that runs in polynomial time on the class of satisfiability problems satisfying Z(p) \leq 1 + \frac{c \log n}{n} for a fixed constant c, where n is the number of variables. In contrast, for any fixed \beta < 1, SAT is still NP-complete when restricted to the class of CNFs for which Z(p) \leq 1 + (1/n^\beta ).