Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Muyu Pan, Matthew Walter, Dheeraj Kodakandla, Mahfuza Farooque

TL;DR

LangSAT addresses the accessibility gap in SAT solving by enabling natural language inputs to be converted into CNF and solved with an RL-enhanced CDCL solver. It introduces Lang2Logic for NL-to-CNF and SmartSAT for PPO-based heuristic optimization, and demonstrates comparable performance to traditional CDCL on the uf20-91 dataset with improved consistency. The approach enables more user-friendly reasoning, formal verification, and debugging workflows. Future work includes expanding input modalities (e.g., code) and enriching global features to further boost solving efficiency.

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.

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

TL;DR

LangSAT addresses the accessibility gap in SAT solving by enabling natural language inputs to be converted into CNF and solved with an RL-enhanced CDCL solver. It introduces Lang2Logic for NL-to-CNF and SmartSAT for PPO-based heuristic optimization, and demonstrates comparable performance to traditional CDCL on the uf20-91 dataset with improved consistency. The approach enables more user-friendly reasoning, formal verification, and debugging workflows. Future work includes expanding input modalities (e.g., code) and enriching global features to further boost solving efficiency.

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.

Paper Structure

This paper contains 21 sections, 1 equation, 4 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Overview of Methods for CNF Conversion in SAT Solvers
  4. Boolean Satisfiability Problem
  5. Conflict-Driven Clause Learning
  6. Methodology
  7. Lang2Logic: Translating Natural Language to CNF
  8. Natural Language to Logical Expression
  9. Logical Expression to CNF Conversion
  10. CNF Simplification
  11. SmartSAT: RL-Driven Heuristic Optimization for SAT Solvers
  12. Reinforcement Learning
  13. Observation Space
  14. Action Space and Rewards
  15. Feature Selection
  16. ...and 6 more sections

Figures (4)

  • Figure 1: Lang2Logic framework: Flow from natural language input to CNF output.
  • Figure 2: Architecture comparison of SmartSAT vs. Traditional CDCL
  • Figure 3: Lang2Logic test case with four clauses and four variables
  • Figure 4: Comparison of Baseline Times and SmartSAT Times for uf20-91 Test Set