Keywords
AI, Satisfiability, Machine Learning, Constraint

Technologies
Python, PyTorch, MiniSat, NetworkX

This project investigates whether machine learning can improve the efficiency of SAT solvers by predicting which variables are most important to branch on early in the solving process. The objective was to design and evaluate a Graph Neural Network (GNN) capable of learning meaningful variable rankings directly from the structure of Boolean formulas expressed in Conjunctive Normal Form (CNF).

An end-to-end pipeline was developed, beginning with parsing CNF instances and representing them as Variable Incidence Graphs. Structural features were extracted for each variable. A lightweight Multi-Layer Perceptron was first implemented as a baseline, followed by a GNN model that leverages graph structure to improve predictions.

Results show that the GNN achieves a strong correlation with true variable importance, demonstrating its ability to learn useful heuristics. These predicted rankings can be integrated into SAT solvers to reduce conflicts and decisions, offering potential speed improvements. The project highlights the promise of combining graph-based learning with combinatorial optimisation to enhance solver performance in real-world applications.