LangSAT: A Novel Framework Combining NLP and Reinforcement Learning for SAT Solving
This work addresses accessibility for users in reasoning, formal verification, and debugging by allowing natural language inputs instead of requiring CNF, though it is incremental as it builds on existing SAT-solving techniques.
The authors tackled the problem of making Boolean satisfiability (SAT) solving more accessible by developing LangSAT, a framework that converts English descriptions into Conjunctive Normal Form (CNF) expressions and solves them using a reinforcement learning-enhanced solver, achieving comparable solving times to traditional methods.
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.