Learning to Rank the Initial Branching Order of SAT Solvers

This paper proposes using graph neural networks to predict initial branching orders for CDCL SAT solvers, demonstrating significant speedups on random and pseudo-industrial benchmarks while noting that the approach struggles with complex industrial instances due to the solver's dynamic heuristics overriding the predictions.

The Gist

Imagine you are trying to solve a massive, incredibly complex maze. You have a robot (the SAT Solver) whose job is to find the exit. The robot is very smart and follows a set of rules to navigate, but sometimes it gets stuck in dead ends or takes a very long, winding path because it doesn't know which turn to take first.

This paper is about giving that robot a map before it even starts walking. Specifically, it's about teaching an AI to guess the very first few turns the robot should take to solve the maze faster.

Here is the breakdown of the paper using simple analogies:

1. The Problem: The Robot's "Guessing Game"

In the world of computer science, there are problems called SAT problems (Boolean Satisfiability). Think of these as giant logic puzzles with thousands of switches (variables) that can be either ON or OFF. The goal is to find a combination of switches that makes the whole puzzle work.

The robot (the SAT solver) tries to solve this by making a guess, checking if it works, and if it fails, it backtracks and tries a different guess. The biggest question is: "Which switch should I flip first?"

If the robot picks a "bad" switch to start with, it might wander through thousands of dead ends. If it picks a "good" switch, it might solve the puzzle in seconds. The paper asks: Can we teach an AI to predict the best starting switches?

2. The Solution: The "Smart Map" (Graph Neural Network)

The authors built a special type of AI called a Graph Neural Network (GNN).

• The Input: They turn the logic puzzle into a picture (a graph) where the switches and the rules connecting them are dots and lines.
• The Training: They taught the AI by showing it thousands of puzzles and telling it, "If you start with these switches, you solve it fast."
• The Output: When given a new puzzle, the AI looks at the picture and says, "Start with Switch A, then Switch B, then Switch C."

3. How Did They Teach the AI? (The Three "Labeling" Methods)

To teach the AI, they needed to know what the "perfect" starting order was. Since they didn't have a magic crystal ball, they tried three different ways to figure it out:

• Method A: The "Conflict Detective" (Conflict Labeling)
  They let the robot solve the puzzle normally and watched which switches caused the most arguments (conflicts). They told the AI: "The switches that cause the most fights are the most important to solve first." It's like a detective saying, "The person who argues the most is likely the key to the mystery."
• Method B: The "First Step" Experiment (First Variable Labeling)
  They forced the robot to start with every possible switch, one by one, and saw which one led to the fastest solution. They told the AI: "Start with the switch that, when tried first, gets you out of the maze quickest."
• Method C: The "Evolutionary" Approach (Genetic Labeling)
  They used a computer program that acted like natural selection. It created random orders of switches, kept the ones that worked best, mixed them up, and tried again, slowly evolving a "perfect" order over many generations.

4. The Results: Speeding Up the Robot

The team tested this "Smart Map" on two different robots (MiniSat and CaDiCaL).

• The Good News: On smaller, simpler puzzles (like a maze with 100 rooms), the AI was amazing. It helped the robots solve problems 50% faster or more. It was like giving the robot a flashlight that showed the exit immediately.
• The Surprise: The AI learned the patterns so well that it could even help solve puzzles that were 10 times bigger than the ones it was trained on. It generalized its knowledge, like a student who learns the rules of chess and can play against a grandmaster they've never seen before.

5. The Bad News: Why It Fails on Giant Mazes

When they tried this on huge, real-world industrial puzzles (like designing a microchip or verifying a complex software system), the speedup disappeared.

Why?

1. The Robot Overwrites the Map: The robots have their own built-in "instincts" (heuristics) that are very strong. As soon as the robot starts moving, its own instincts quickly ignore the AI's "Smart Map" and start making its own guesses. It's like giving a GPS to a driver who refuses to look at the screen and just drives by instinct.
2. Too Much Noise: The real-world puzzles are so complex and messy that the AI couldn't find a clear pattern to learn. The "map" it drew was too blurry to be useful.

The Big Takeaway

This paper is a proof-of-concept. It shows that AI can learn to give a head-start to logic solvers, making them much faster on many types of problems.

However, it also highlights a challenge: AI needs to work with the solver's existing rules, not just try to replace them. If the AI's advice is ignored after the first step, the speedup is lost. The authors suggest that future work needs to find a way to keep the AI's advice relevant throughout the whole solving process, not just at the very beginning.

In short: We taught an AI to pick the best starting moves for a logic puzzle. It worked great on small puzzles and even some medium ones, but on the hardest, real-world puzzles, the robot's own instincts took over too quickly. It's a promising start, but the race isn't over yet!

Technical Summary

Here is a detailed technical summary of the paper "Learning to Rank the Initial Branching Order of SAT Solvers".

1. Problem Statement

The Boolean Satisfiability problem (SAT) is a fundamental NP-complete problem central to formal verification and automated theorem proving. While modern Conflict-Driven Clause Learning (CDCL) solvers (e.g., CaDiCaL, MiniSat) are highly efficient, they rely on fixed, handcrafted heuristics (like VSIDS or VMTF) to guide the search. These static heuristics often fail to effectively navigate the combinatorial search space for complex or specific problem instances.

The specific problem addressed in this paper is the initial branching order. In backtracking SAT solvers, the order in which variables are selected for branching significantly impacts solving time. While neural networks have been used to predict satisfiability or guide search dynamically, they are often computationally expensive to run during the search. The authors propose a hybrid approach: using a Graph Neural Network (GNN) as a preprocessing step to predict a high-quality initial branching order, thereby "warming up" the solver before it begins its standard rule-based search.

2. Methodology

The proposed pipeline involves three main stages: Labeling, Graph Representation & Training, and Inference/Integration.

A. Labeling Strategies (Generating Ground Truth)

To train the GNN, the authors needed a method to determine the "optimal" branching order for a given SAT instance. They proposed and compared three labeling methods:

1. Conflict Labeling: Solves the instance once and ranks variables based on the total number of conflicts they participated in. The assumption is that early branching on high-conflict variables (potential "backdoor" variables) speeds up resolution.
2. First Variable Labeling: For each variable, the solver is forced to branch on it first (with the rest of the order randomized) multiple times. Variables are scored by the average number of propagations required. This isolates the individual contribution of a variable.
3. Genetic Labeling: Treats ordering as an optimization problem. It starts with random permutations and uses a genetic algorithm (hill-climbing via random swaps) to find the order that minimizes propagations.

B. Graph Representation

SAT instances are converted into tripartite graphs for the GNN:

• Nodes: Variables ($x_i$) and Clauses ($c_j$).
• Edges: Connect variables to clauses, weighted to indicate if the variable appears negated or positive.
• Meta-node: A central node connected to all clause nodes to facilitate faster message passing.
• Features: Node features include one-hot encodings of the variable's degree quartile relative to other nodes.

C. Model Architecture and Loss

• Architecture: The authors utilize a GNN architecture similar to NeuroBack (Wang et al., 2024), which employs attention mechanisms while maintaining linear memory complexity.
• Task Formulation: The problem is framed as a Learning to Rank task.
• Loss Function: LambdaRank is used. This loss function prioritizes correctly ranking the most relevant variables (those at the top of the optimal order) higher than less relevant ones, reflecting the tree-like nature of SAT search where early decisions have the most impact.

D. Solver Integration

Since standard CDCL solvers do not natively accept a pre-defined variable order, the authors modified MiniSat and CaDiCaL to accept the GNN's output:

• The GNN outputs a score for each variable.
• These scores are used to initialize the activity levels (used in the VSIDS heuristic) and, for CaDiCaL, the VMTF queue.
• This allows the solver to start with the GNN's suggested order before its internal heuristics take over.

3. Key Contributions

1. Empirical Verification of Initial Order Impact: The authors demonstrated that the choice of the first variable to branch on has a massive impact on solving time (speedups of up to 2,200% on small random instances), validating the premise that initial ordering is a learnable and critical factor.
2. Three Labeling Methods: They introduced and compared Conflict, First Variable, and Genetic labeling strategies, analyzing their learnability and effectiveness as training targets.
3. GNN-Initialized Hybrid Solver: They successfully implemented a pipeline where a GNN predicts an initial branching order, integrated seamlessly into state-of-the-art solvers without requiring continuous neural inference during the search.
4. Generalization Analysis: They showed that models trained on small instances (20–40 variables) can generalize to significantly larger instances (up to 5–10x larger) on random benchmarks.

4. Results

Random 3-CNF Benchmarks

• Performance: The GNN-initialized solvers achieved significant speedups (up to 50% reduction in solving time) on random instances with 200 variables or fewer.
• Generalization: Models trained on small instances (20–40 vars) generalized well to larger instances (up to 250 vars).
• Labeling Comparison: All three labeling methods yielded similar performance improvements, though Conflict Labeling showed slightly lower Spearman correlation with the ground truth on SAT instances compared to First Variable and Genetic methods.

Pseudo-Industrial Benchmarks (G4SATBench)

• Easier Instances: On "medium" difficulty instances, the GNN provided a 10–20% reduction in propagations.
• Hard Instances: On "hard" instances (requiring $>10^5$ propagations), the speedup vanished. The predictive power of the GNN degraded significantly (Spearman correlation dropped to near zero for Genetic labeling), likely due to the noise in labels for large variable sets.

Industrial Benchmarks (SAT Competition 2024)

• Performance: On real-world industrial instances, the GNN approach failed to provide significant speedups over the default solvers.
• Observation: The GNN's suggested order was effectively overwritten by the solver's dynamic heuristics almost immediately.

5. Significance and Discussion

Why it works (and where it fails):
The paper identifies two primary reasons for the performance decay on complex instances:

1. Dynamic Overwriting: In difficult problems with long solving times, the solver's internal dynamic heuristics (VSIDS/VMTF) rapidly overwrite the static initialization provided by the GNN. The "warm start" advantage is lost before it can influence the search trajectory.
2. Complexity: Industrial instances are structurally complex, making it difficult for the GNN to predict a globally optimal initial order.

Significance:

• Hybrid Approach: This work advances the field of "hybrid SAT solvers" by demonstrating that a single, non-invasive preprocessing step can yield benefits without the computational overhead of running a neural network at every search step.
• Underexplored Area: It highlights initial branching order as a critical, yet underexplored, intersection between neural networks and classical solvers.
• Future Direction: The results suggest that for hybrid solvers to succeed on industrial problems, future work must either focus on dynamic re-intervention (reminding the solver of the order) or developing GNNs capable of predicting orders that are robust against the solver's own heuristics.

In conclusion, while the approach yields substantial gains on generated and pseudo-industrial benchmarks, the current limitations in handling large-scale industrial problems point toward the need for more robust integration strategies between neural guidance and rule-based heuristics.