Satisfiability as a Classification Problem

Given a Boolean formula, the classic satisfiability problem is to decide whether there is a truth assignment to its variables such that the formula evaluates to true. The satisfiability problem was the first decision problem proven to be NP-Complete. Therefore, it is very unlikely that there exists an algorithm for solving the satisfiability problem that has good worst-case performance. However, the satisfiability problem is ubiquitous in artificial intelligence. In this paper, we view the satisfiability problem as a classification task. Based on easy to compute structural features of instances of large satisfiability problems we use a variety of standard classifier learners to classify previously unseen instances of the satisfiability problem as either satisfiable or unsatisfiable. We show that standard learning techniques can very reliably perform this task, with accuracy in excess of 99% for hard 3-SAT problems, and usually in excess of 90% for large industrial benchmarks. These results are surprising, and suggest that machine learning techniques can be very effective at revealing the significant structural characteristics that are important in satisfiability testing.