Learning Splitting Heuristics in Divide-and-Conquer SAT Solvers with Reinforcement Learning
Shumao Zhai Ning Ge
We propose RDC-SAT, a novel approach to optimize splitting heuristics in Divide-and-Conquer SAT solvers using deep reinforcement learning.  Our method dynamically extracts features from the current solving state whenever a split is required.  These features, such as learned clauses, variable activity scores, and clause LBD (Literal Block Distance) values, are represented as a graph.  A GNN integrated with an Actor-Critic model processes this graph to determine the optimal split variable.  Unlike traditional linear state transitions characterized by Markov processes, divide-and-conquer challenges involve tree-like state transitions.  To address this, we developed a reinforcement learning environment based on the Painless framework that efficiently handles these transitions.  Additionally, we designed different discounted reward functions for satisfiable and unsatisfiable SAT problems, capable of handling tree-like state transitions.  We trained our model using the Decentralized Proximal Policy Optimization (DPPO) algorithm on phase transition random 3-SAT problems and implemented the RDC-SAT solver, which operates in both GPU-accelerated and non-GPU modes.  Evaluations show that RDC-SAT significantly improves the performance of D\&C solvers on phase transition random 3-SAT datasets and generalizes well to the SAT Competition 2023 dataset, substantially outperforming traditional splitting heuristics.
SAT Problem, Divide And Conquer, Graph Neural Network, Reinforcememt Learning