TLDR: ImitSAT is a new branching policy for SAT solvers that uses imitation learning. It learns from ‘KeyTraces,’ which are condensed expert solver runs that capture only the essential, conflict-free decisions. By treating branching as a sequence prediction problem, ImitSAT, powered by a Transformer model, significantly reduces propagation counts and runtime, outperforming existing learning-based methods and demonstrating strong generalization across various SAT problem types.
The Boolean Satisfiability Problem, or SAT, is a fundamental challenge in computer science and artificial intelligence. It asks whether a given logical formula can be made true by assigning true or false values to its variables. Modern solutions to SAT problems largely rely on a framework called Conflict-Driven Clause Learning (CDCL). While CDCL solvers have become incredibly powerful, their efficiency heavily depends on how they make ‘branching’ decisions – essentially, which variable to try assigning a value to next. Poor decisions can lead to exponentially longer solving times, primarily by increasing the number of ‘propagations’ (deductions made from current assignments), which consume the majority of a solver’s runtime.
Traditional branching strategies are often hand-crafted and struggle to adapt to diverse problem structures. Recent attempts to integrate machine learning have shown promise but also faced limitations. For instance, methods like SATformer influence variable activities only at the start, while Graph-Q-SAT uses reinforcement learning, which can be unstable due to sparse rewards and requires extensive exploration. These approaches often don’t fully leverage the rich history of a CDCL solver’s execution.
Introducing ImitSAT: Learning from Expert Traces
A new research paper, BOOLEAN SATISFIABILITY VIA IMITATION LEARNING, introduces ImitSAT, a novel branching policy for CDCL solvers that uses imitation learning. Unlike its predecessors, ImitSAT learns directly from ‘expert’ demonstrations, specifically from something called a KeyTrace. Imagine a perfect, or near-perfect, run of a SAT solver. This run would avoid unnecessary detours and conflicts, making only the most crucial decisions. ImitSAT aims to mimic this ideal behavior.
The Power of KeyTrace
The core innovation behind ImitSAT is the KeyTrace. A typical CDCL solver’s execution trace is long and filled with decisions that are later undone by backtracking. The KeyTrace simplifies this by collapsing a full solver run into a concise sequence of only the ‘surviving’ decisions – those that actually contribute to solving the problem. This process effectively removes all the wasted effort and redundant propagations. When a KeyTrace is replayed on the same problem, it results in a nearly conflict-free run, drastically reducing propagations to a mere 4% of a standard solver’s total. This provides a clean, dense, and highly effective training signal for the learning model.
How ImitSAT Learns and Integrates
ImitSAT treats the branching problem as a sequence modeling task. It takes the problem formula and the current KeyTrace prefix (the sequence of decisions made so far) and, using a Transformer-based model, predicts the next optimal branching decision. This approach, known as behavior cloning, allows the model to learn high-quality decisions without the need for costly exploration, leading to faster and more stable training.
During its operation, ImitSAT is integrated seamlessly into the CDCL framework. It’s queried for a decision under a small computational budget. If its prediction is valid, the solver uses it; otherwise, it falls back to the traditional VSIDS heuristic. This ensures the solver remains complete and robust, while benefiting from the learned policy’s guidance, especially for early decisions which significantly influence the overall search trajectory.
Also Read:
- Bolt Tool Accelerates Temporal Logic Learning with Boolean Set Cover
- Interactive Refinement: A New Strategy to Combat Over-fitting in Constraint Acquisition
Impressive Results and Generalization
Extensive experiments demonstrate ImitSAT’s effectiveness. It consistently reduces propagation counts and overall runtime compared to state-of-the-art learned approaches like SATformer and Graph-Q-SAT. Remarkably, even though ImitSAT is trained primarily on random 3-SAT instances, it shows strong generalization capabilities. It performs well on diverse, structured SAT families, including satisfiable and unsatisfiable instances, and even non-k-SAT formulas, without any retraining or fine-tuning.
The researchers also implemented improved training techniques to prevent overfitting, such as variable permutation augmentation (randomly shuffling variable IDs) and a staged curriculum learning strategy (gradually increasing problem complexity during training). These methods further enhance ImitSAT’s robustness and efficiency.
In conclusion, ImitSAT represents a significant step forward in guiding CDCL solvers. By leveraging imitation learning and the innovative KeyTrace concept, it provides a stable, efficient, and generalizable approach to making better branching decisions, ultimately leading to faster SAT solving.
