A Second Order Parameter for 3SAT

No. 1: Agents, AI in Art and Entertainment, Knowledge Representation, and Learning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 13

Game-Tree Search

The 3-satisfiability problem (3SAT) has had a central role in the study of complexity. It was recently found that 3SAT instances transition sharply from satisfiable to nonsatisfiable as the ratio of clauses to variables increases. Because this phase transition is so sharp, the ratio - an order parameter - can be used to predict satisfiability. This paper describes a second order parameter for 3SAT. Like the classical order parameter, it can be computed in linear time, but it analyzes the structure of the problem instance more deeply. We present an analytical method for using this new order parameter in conjunction with the classical one to enhance satisfiability prediction accuracy. The assumptions of the method are verified by rigorous statistical testing. The method significantly increases the satisfiability prediction accuracy over using the classical order parameter alone. Hardness - i.e. how long it takes to determine satisfiability - results for one complete and one incomplete algorithm from the literature are also presented as a function of the two order parameters. The importance of new order parameters lies in the fact that they refine the locating of satisfiable vs. nonsatisfiable and hard vs. easy formulas in the space of all problem instances by adding a new dimension in the analysis.