# LangSAT: A Novel Framework Combining NLP and Reinforcement Learning for SAT Solving

arXiv: https://arxiv.org/abs/2512.04374 · HTML: https://mlsanity.com/paper/2512.04374/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in RL training of language and agent models, one of 15 directions in Deep reinforcement learning methods.
- Builds on 4 of its 21 references that are in the map.
- First posted on arXiv 4 Dec 2025.

## Placed in

- Deep reinforcement learning methods / [RL training of language and agent models](https://mlsanity.com/deeprl/rl-training-of-language-and-agent-models/)

## Builds on (most cited first, 4 of 4)

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers](https://mlsanity.com/paper/1506.08905/) (2015)
- [SATfeatPy -- A Python-based Feature Extraction System for Satisfiability](https://mlsanity.com/paper/2204.14116/) (2022)

## Built on by (most cited first, 2 of 2)

- [TIAR: Trajectory-Informed Advantage Reweighting for LLM Abstention Learning](https://mlsanity.com/paper/2605.25850/) (2026)
- [Auto-Formalizing Neuro-Symbolic Predictors](https://mlsanity.com/paper/2610.01519/) (2026)

## Abstract (arXiv)

Our work presents a novel reinforcement learning (RL) based framework to optimize heuristic selection within the conflict-driven clause learning (CDCL) process, improving the efficiency of Boolean satisfiability (SAT) solving. The proposed system, LangSAT, bridges the gap between natural language inputs and propositional logic by converting English descriptions into Conjunctive Normal Form (CNF) expressions and solving them using an RL-enhanced CDCL SAT solver. Unlike existing SAT-solving platforms that require CNF as input, LangSAT enables users to input standard English descriptions, making SAT-solving more accessible. The framework comprises two key components: Lang2Logic, which translates English sentences into CNF expressions, and SmartSAT, an RL-based SAT solver. SmartSAT encodes clause-variable relationships as structured graph representations and extracts global features specific to the SAT problem. This implementation provides the RL agent with deeper contextual information, enabling SAT problems to be solved more efficiently. Lang2Logic was evaluated on diverse natural language inputs, processing descriptions up to 450 words. The generated CNFs were solved by SmartSAT, which demonstrated comparable performance to traditional CDCL heuristics with respect to solving time. The combined LangSAT framework offers a more accessible and scalable solution for SAT-solving tasks across reasoning, formal verification, and debugging.