Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2502.14328 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913700336631808 |
|---|---|
| author | Sheng, Junjie Lin, Yanqiu Wu, Jiehao Huang, Yanhong Shi, Jianqi Zhang, Min Wang, Xiangfeng |
| author_facet | Sheng, Junjie Lin, Yanqiu Wu, Jiehao Huang, Yanhong Shi, Jianqi Zhang, Min Wang, Xiangfeng |
| contents | The Satisfiability (SAT) problem is a core challenge with significant applications in software engineering, including automated testing, configuration management, and program verification. This paper presents SolSearch, a novel framework that harnesses large language models (LLMs) to discover and optimize SAT-solving strategies automatically. Leveraging a curriculum-based, trial-and-error process, SolSearch enables the LLM to iteratively modify and generate SAT solver code, thereby improving solving efficiency and performance. This automated SAT-solving paradigm has the advantage of being plug-and-play, allowing integration with any SAT solver and accelerating the development or design process of new SAT solvers (new methods). Our preliminary experimental results are encouraging by demonstrating that the LLM-powered paradigm improves state-of-the-art SAT solvers on general SAT benchmarks and significantly enhances the performance of the widely used Z3 solver (11\% on PAR-2 score). These results highlight the potential for using LLM-driven methods to advance solver adaptability and effectiveness in real-world software engineering challenges. Future research directions are discussed to further refine and validate this approach, offering a promising avenue for integrating AI with traditional software engineering tasks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_14328 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation Sheng, Junjie Lin, Yanqiu Wu, Jiehao Huang, Yanhong Shi, Jianqi Zhang, Min Wang, Xiangfeng Software Engineering The Satisfiability (SAT) problem is a core challenge with significant applications in software engineering, including automated testing, configuration management, and program verification. This paper presents SolSearch, a novel framework that harnesses large language models (LLMs) to discover and optimize SAT-solving strategies automatically. Leveraging a curriculum-based, trial-and-error process, SolSearch enables the LLM to iteratively modify and generate SAT solver code, thereby improving solving efficiency and performance. This automated SAT-solving paradigm has the advantage of being plug-and-play, allowing integration with any SAT solver and accelerating the development or design process of new SAT solvers (new methods). Our preliminary experimental results are encouraging by demonstrating that the LLM-powered paradigm improves state-of-the-art SAT solvers on general SAT benchmarks and significantly enhances the performance of the widely used Z3 solver (11\% on PAR-2 score). These results highlight the potential for using LLM-driven methods to advance solver adaptability and effectiveness in real-world software engineering challenges. Future research directions are discussed to further refine and validate this approach, offering a promising avenue for integrating AI with traditional software engineering tasks. |
| title | SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2502.14328 |