Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang, Bingzhen Zhang, Ke Wei, Shaowei Cai

TL;DR

This work proposes AutoSAT, a framework that automatically optimizes heuristics in a pre-defined modular search space based on existing CDCL solvers based on Large Language Models, and demonstrates that LLMs can generally enhance the performance of CDCL solvers.

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.

AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

TL;DR

This work proposes AutoSAT, a framework that automatically optimizes heuristics in a pre-defined modular search space based on existing CDCL solvers based on Large Language Models, and demonstrates that LLMs can generally enhance the performance of CDCL solvers.

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.
Paper Structure (32 sections, 4 equations, 3 figures, 2 tables)

This paper contains 32 sections, 4 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries and Related Works
  3. Preliminary Definition on SAT
  4. CDCL solver
  5. LLM-based Optimizers
  6. Development in Evolutionary Computation
  7. AutoSAT
  8. Fine-Grained Search Space
  9. Search Strategies
  10. Optimization Problem
  11. Algorithms
  12. Prompt Engineering
  13. Experimental Results
  14. Settings
  15. Environment
  16. ...and 17 more sections

Figures (3)

  • Figure 1: PAR2 obtained by Different Search Strategies. This figure visualizes the comparison between AutoSAT with the greedy hill climber (GHC for short) and the $(1+1)$ EA (EA for short) regarding the PAR2 (lower is better). Overall, the EA outperforms the GHC, but on certain datasets, the GHC even achieves SOTA results.
  • Figure 2: PAR2 over Different Datasets. This figure visualizes the comparison of solvers regarding the PAR2 values in table \ref{['PAR2result']}. In practice, the plotted values are normalized for each dataset by $1 - \frac{curr - min}{2*(max - min)}$, where $curr$ is the PAR2 obtained by the corresponding solver, and $min$ and $max$ correspond to the minimum and maximum PAR2 values obtained by all the tested solvers, respectively. Larger shadow areas indicate better performance.
  • Figure 3: PAR2 during searching process in register-allocation dataset. This figure illustrates an example of AutoSAT searching for better heuristics. As shown in the figure, ten modifications result in improvements of PAR2 along the optimization process. We highlight on the right a modification of the $reduce\_condition\_functin$ heuristics, which happens at the forth evaluation.