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

TL;DR

LangSAT introduces an innovative framework that translates natural language into CNF and employs reinforcement learning to enhance SAT solving efficiency, making the process more accessible and scalable.

Contribution

The paper presents a novel NLP-RL integrated framework, LangSAT, enabling natural language input for SAT solving and improving heuristic selection in the CDCL process.

Findings

Lang2Logic effectively converts English descriptions into CNF expressions.

SmartSAT achieves solving times comparable to traditional heuristics.

Framework enhances accessibility and scalability of SAT solving.

Abstract

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.