Predicting Propositional Satisfiability via End-to-End Learning

Authors

  • Chris Cameron University of British Columbia
  • Rex Chen University of British Columbia
  • Jason Hartford University of British Columbia
  • Kevin Leyton-Brown University of British Columbia

DOI:

https://doi.org/10.1609/aaai.v34i04.5733

Abstract

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. Existing methods have relied on extensive, manual feature engineering and computationally complex features (e.g., based on linear programming relaxations). We show for the first time that even better performance can be achieved by end-to-end learning methods — i.e., models that map directly from raw problem inputs to predictions and take only linear time to evaluate. Our work leverages deep network models which capture a key invariance exhibited by SAT problems: satisfiability status is unaffected by reordering variables and clauses. We showed that end-to-end learning with deep networks can outperform previous work on random 3-SAT problems at the solubility phase transition, where: (1) exactly 50% of problems are satisfiable; and (2) empirical runtimes of known solution methods scale exponentially with problem size (e.g., we achieved 84% prediction accuracy on 600-variable problems, which take hours to solve with state-of-the-art methods). We also showed that deep networks can generalize across problem sizes (e.g., a network trained only on 100-variable problems, which typically take about 10 ms to solve, achieved 81% accuracy on 600-variable problems).

Downloads

Published

2020-04-03

How to Cite

Cameron, C., Chen, R., Hartford, J., & Leyton-Brown, K. (2020). Predicting Propositional Satisfiability via End-to-End Learning. Proceedings of the AAAI Conference on Artificial Intelligence, 34(04), 3324-3331. https://doi.org/10.1609/aaai.v34i04.5733

Issue

Section

AAAI Technical Track: Machine Learning