⚙️ Machine Learning based Parallel SAT

This page showcases how the reasoning and learning research group @ Georgia Tech led by Professor Vijay Ganesh is advancing parallel SAT solving with machine learning, symbolic deductive feedback, and high-performance cube-and-conquer strategies.

Vijay Ganesh's Homepage

Neurosymbolic AI for Mathematics NeuroSymbolic AI for Software Engineering AI for Scientific Discovery

---

AlphaMapleSAT: Machine Learning Guided Parallel SAT Solving

Authors: Piyush Jha^†,1, Zhengyu Li^†,1, Zhengyang (John) Lu², Curtis Bright³, Vijay Ganesh¹

Affiliations: ¹Georgia Institute of Technology, USA  |  ²University of Waterloo, Canada  |  ³University of Windsor, Canada

^† Equal contributions

TL;DR: AlphaMapleSAT integrates Monte Carlo Tree Search-guided cubing with symbolic deductive feedback—leveraging Boolean constraint propagation—to focus cube-and-conquer exploration on promising branches. This reduces wasted work on hard combinatorial SAT benchmarks and achieves up to 8× wall-clock speedups over state-of-the-art baselines.

Project Page