Research map / Reinforcement learning / Visual and representation RL

Learning Splitting Heuristics in Divide-and-Conquer SAT Solvers with Reinforcement Learning

ICLR 2025 · Reinforcement learning › Visual and representation RL · approach: Scalable RL systems and environments

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's abstract only. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Proposes RDC-SAT, which uses deep reinforcement learning with a GNN-based actor-critic to learn variable splitting heuristics for Divide-and-Conquer SAT solvers.

Problem

Choosing good splitting variables in Divide-and-Conquer SAT solvers is critical for performance, and existing heuristics are hand-designed.

Approach

Dynamically extracts solver-state features (learned clauses, variable activity scores, clause LBD values) at each split decision, represents them as a graph, and uses a GNN integrated with an Actor-Critic RL agent to pick split variables.

Experimental setup

Builds on: Divide-and-Conquer SAT solving

Closest papers by meaning

• Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs (ICLR 2026 · similarity 0.91)
• Learning How to Cube (NeurIPS 2026 · similarity 0.87)
• SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.86)
• HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation (NeurIPS 2024 · similarity 0.84)
• NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks (ICLR 2024 · similarity 0.84)
• UDC: A Unified Neural Divide-and-Conquer Framework for Large-Scale Combinatorial Optimization Problems (NeurIPS 2024 · similarity 0.84)