SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation

TL;DR

This paper introduces SolSearch, a framework using large language models to automatically generate and optimize SAT solver code, improving efficiency and performance on benchmark problems.

Contribution

It presents a novel LLM-driven approach for automatic SAT solver code generation and optimization, enhancing solver performance and adaptability.

Findings

Improves SAT solver performance by 11% on PAR-2 score.

Enables plug-and-play integration with existing SAT solvers.

Demonstrates potential for AI-driven advancements in software engineering.

Abstract

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.