让AI用自然语言直接解逻辑题，提升求解效率。
LangSAT: A Novel Framework Combining NLP and Reinforcement Learning for SAT Solving
- 用强化学习优化逻辑求解中的启发式策略。
- 支持450词英文描述转为逻辑公式并求解。
- 适合需要自然语言输入的推理与验证场景。
本文提出一种基于强化学习（RL）的新型框架LangSAT，用于优化冲突驱动子句学习（CDCL）过程中的启发式选择，提升布尔可满足性（SAT）求解效率。该系统通过将英文描述转化为合取范式（CNF）表达式，并利用增强型RL的CDCL SAT求解器进行求解，突破了传统SAT平台需以CNF为输入的限制，使非专业用户也能通过自然语言完成逻辑问题求解。框架包含两个核心组件：Lang2Logic负责将英文句子转换为CNF表达式，SmartSAT则采用图结构表示变量-子句关系，提取问题全局特征，赋予强化学习代理更深层上下文信息。实验表明，Lang2Logic可处理最长450词的自然语言输入，生成的CNF由SmartSAT求解，其求解时间与传统启发式方法相当。整个框架在推理、形式化验证和调试任务中展现出更高的可用性与可扩展性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。