Predicting Satisfiability at the Phase Transition via End-to-End Learning

Strangely enough, it is possible to use machine learning models to predict the satisfiability status of hard SAT problems with accuracy considerably higher than random guessing. We consider random 3-SAT problems at the solubility phase transition, where exactly 50% of problems are satisfiable and where empirical runtimes of known solution methods scale exponentially with problem size. In this domain, we can, for example, learn computationally efficient models that achieve 84% prediction accuracy on 600-variable problems, which take hours to solve with state-of-the-art methods.

In our first work on this problem (AAAI 2012) we showed that we could make such predictions using simple decision tree models that relied on manually engineered polynomial-time computable features (e.g., linear programming relaxations). We also found that our models could generalize across problem sizes, maintaining high accuracy on large problems even when trained only on very small problems.

More recently (AAAI 2020), we showed that this phenomenon does not depend on access to hand-crafted features. Instead, we achieved even better performance (including generalization across problem size) via end-to-end learning methods: models that map directly from raw problem inputs to predictions and that take only linear time to evaluate. These results leveraged a novel deep network architecture that captures the key structural invariance exhibited by SAT problems--satisfiability status is preserved under variable and clause reorderings.

If time permits, the talk will end with a teaser: a discussion of unpublished theoretical work that establishes a performance gap between (1) learning an objective function from data (e.g., travel times in a road network) and then optimizing (e.g., finding fastest routes); and (2) learning the same function end-to-end (i.e., back-propagating through the optimization problem).

Predicting Satisfiability at the Phase Transition. L. Xu, H. Hoos, K. Leyton-Brown. Conference of the Association for the Advancement of Artificial Intelligence (AAAI), (7 pages), 2012.  PDF
Predicting Propositional Satisfiability via End-to-End Learning. C. Cameron, R. Chen, J. Hartford, K. Leyton-Brown. Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020. PDF  DOI