用大模型分析代码结构，自动生成高效求解起点
Extracting Problem Structure with LLMs for Optimized SAT Local Search
- 用LLM分析问题编码代码，挖掘隐藏的结构模式
- 自动生成专用局部搜索算法，初始赋值质量显著提升
- 适用于同类型编码的所有实例，适合想加速SAT求解的研究者
局部搜索预处理通过提供高质量初始解，使冲突驱动子句学习（CDCL）求解器更快。但现有工具依赖基础策略，难以捕捉问题中的结构模式。本文提出一种方法，利用大语言模型（LLMs）分析基于Python的编码代码，揭示问题转换为布尔可满足性（SAT）时的隐藏结构特征。该方法自动构建专用局部搜索算法，识别并利用这些模式生成强初始赋值，适用于同种编码类型的任意问题实例。实验表明，相比基线预处理系统，本方法显著缩短了求解时间。
原文摘要 · Abstract (English)
Local search preprocessing makes Conflict-Driven Clause Learning (CDCL) solvers faster by providing high-quality starting points and modern SAT solvers have incorporated this technique into their preprocessing steps. However, these tools rely on basic strategies that miss the structural patterns in problems. We present a method that applies Large Language Models (LLMs) to analyze Python-based encoding code. This reveals hidden structural patterns in how problems convert into SAT. Our method automatically generates specialized local search algorithms that find these patterns and use them to create strong initial assignments. This works for any problem instance from the same encoding type. Our tests show encouraging results, achieving faster solving times compared to baseline preprocessing systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。