AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

TL;DR

AutoSAT leverages large language models to automatically optimize heuristics in SAT solvers, significantly improving their performance across multiple datasets by generating new, efficient heuristics within a modular framework.

Contribution

This paper introduces AutoSAT, a novel framework that uses LLMs to automatically optimize heuristics in CDCL SAT solvers, enabling the generation of new heuristics beyond traditional tuning methods.

Findings

AutoSAT outperforms MiniSat on 9 out of 12 datasets.

AutoSAT surpasses Kissat on 4 datasets.

LLMs can generally enhance CDCL solver performance.

Abstract

Conflict-Driven Clause Learning (CDCL) is the mainstream framework for solving the Satisfiability problem (SAT), and CDCL solvers typically rely on various heuristics, which have a significant impact on their performance. Modern CDCL solvers, such as MiniSat and Kissat, commonly incorporate several heuristics and select one to use according to simple rules, requiring significant time and expert effort to fine-tune in practice. The pervasion of Large Language Models (LLMs) provides a potential solution to address this issue. However, generating a CDCL solver from scratch is not effective due to the complexity and context volume of SAT solvers. Instead, we propose AutoSAT, a framework that automatically optimizes heuristics in a pre-defined modular search space based on existing CDCL solvers. Unlike existing automated algorithm design approaches focusing on hyperparameter tuning and operator selection, AutoSAT can generate new efficient heuristics. In this first attempt at optimizing SAT solvers using LLMs, several strategies including the greedy hill climber and (1+1) Evolutionary Algorithm are employed to guide LLMs to search for better heuristics. Experimental results demonstrate that LLMs can generally enhance the performance of CDCL solvers. A realization of AutoSAT outperforms MiniSat on 9 out of 12 datasets and even surpasses the state-of-the-art hybrid solver Kissat on 4 datasets.