Automatically discovering heuristics in a complex SAT solver with large language models

• URL: http://arxiv.org/abs/2507.22876v1
• Date: Wed, 30 Jul 2025 17:52:25 GMT
• Title: Automatically discovering heuristics in a complex SAT solver with large language models
• Authors: Yiwen Sun, Furong Ye, Zhihan Chen, Ke Wei, Shaowei Cai,
• Abstract summary: Satisfiability problem (SAT) is a cornerstone of computational complexity with broad industrial applications.<n>Modern SAT solvers rely on manually constrained search spaces and yield limited performance gains.<n>This work introduces a novel paradigm which effectively optimize complex SAT solvers via Large Language Models (LLMs)
• Score: 9.96578394096009
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Satisfiability problem (SAT) is a cornerstone of computational complexity with broad industrial applications, and it remains challenging to optimize modern SAT solvers in real-world settings due to their intricate architectures. While automatic configuration frameworks have been developed, they rely on manually constrained search spaces and yield limited performance gains. This work introduces a novel paradigm which effectively optimizes complex SAT solvers via Large Language Models (LLMs), and a tool called AutoModSAT is developed. Three fundamental challenges are addressed in order to achieve superior performance: (1) LLM-friendly solver: Systematic guidelines are proposed for developing a modularized solver to meet LLMs' compatibility, emphasizing code simplification, information share and bug reduction; (2) Automatic prompt optimization: An unsupervised automatic prompt optimization method is introduced to advance the diversity of LLMs' output; (3) Efficient search strategy: We design a presearch strategy and an EA evolutionary algorithm for the final efficient and effective discovery of heuristics. Extensive experiments across a wide range of datasets demonstrate that AutoModSAT achieves 50% performance improvement over the baseline solver and achieves 30% superiority against the state-of-the-art (SOTA) solvers. Moreover, AutoModSAT attains a 20% speedup on average compared to parameter-tuned alternatives of the SOTA solvers, showcasing the enhanced capability in handling complex problem instances. This work bridges the gap between AI-driven heuristics discovery and mission-critical system optimization, and provides both methodological advancements and empirically validated results for next-generation complex solver development.

Related papers

• Grammar-Guided Evolutionary Search for Discrete Prompt Optimisation [63.97051732013936]
  We propose an evolutionary search approach to automated discrete prompt optimisation consisting of two phases.<n>In the first phase, grammar-guided genetic programming is invoked to synthesise prompt-creating programmes.<n>In the second phase, local search is applied to explore the neighbourhoods of best-performing programmes.
  arXiv  Detail & Related papers  (2025-07-14T14:34:15Z)
• CROP: Circuit Retrieval and Optimization with Parameter Guidance using LLMs [4.481239665281804]
  We present CROP, the first large language model (LLM)-powered automatic VLSI design flow tuning framework.<n>Our approach includes: (1) a scalable methodology for transforming RTL source code into dense vector representations, (2) an embedding-based retrieval system for matching designs with semantically similar circuits, and (3) a retrieval-augmented generation (RAG)-enhanced LLM-guided parameter search system.<n>Experiment results demonstrate CROP's ability to achieve superior quality-of-results (QoR) with fewer iterations than existing approaches on industrial designs, including a 9.9% reduction in power consumption.
  arXiv  Detail & Related papers  (2025-07-02T20:25:47Z)
• Dynamic Location Search for Identifying Maximum Weighted Independent Sets in Complex Networks [0.47248250311484113]
  We introduce a novel and efficient algorithm for solving the maximum weighted independent set (MWIS) problem.<n>Given the NP-hard nature of the MWIS problem, our proposed algorithm, DynLS, incorporates three key innovations to solve it effectively.<n>Our experimental results demonstrate DynLS's superior performance, consistently delivering high-quality solutions within 1000 seconds.
  arXiv  Detail & Related papers  (2025-05-07T10:35:53Z)
• ZeroLM: Data-Free Transformer Architecture Search for Language Models [54.83882149157548]
  Current automated proxy discovery approaches suffer from extended search times, susceptibility to data overfitting, and structural complexity.<n>This paper introduces a novel zero-cost proxy methodology that quantifies model capacity through efficient weight statistics.<n>Our evaluation demonstrates the superiority of this approach, achieving a Spearman's rho of 0.76 and Kendall's tau of 0.53 on the FlexiBERT benchmark.
  arXiv  Detail & Related papers  (2025-03-24T13:11:22Z)
• SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation [13.056487325961688]
  The Satisfiability (SAT) problem is a core challenge with significant applications in software engineering.<n>This paper presents SolSearch, a novel framework that harnesses large language models (LLMs) to discover and optimize SAT-solving strategies automatically.
  arXiv  Detail & Related papers  (2025-02-20T07:25:21Z)
• Autoformulation of Mathematical Optimization Models Using LLMs [50.030647274271516]
  This paper approaches the problem of $textitautoformulation$: the automated creation of solver-ready optimization models from natural language problem descriptions.<n>We identify three core challenges of autoformulation: $textit(1)$ the vast, problem-dependent hypothesis space, and $textit(2)$ efficient and diverse exploration of this space under uncertainty.<n>We present a novel method leveraging $textitLarge Language Models$ with $textitMonte-Carlo Tree Search$, exploiting the hierarchical nature of optimization modeling to generate and systematically explore possible formulations
  arXiv  Detail & Related papers  (2024-11-03T20:41:38Z)
• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path. The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
  arXiv  Detail & Related papers  (2024-10-03T18:12:29Z)
• AutoSAT: Automatically Optimize SAT Solvers via Large Language Models [10.359005620433136]
  We propose AutoSAT, a framework that automatically optimizes in a pre-defined modular search space based on existing 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.
  arXiv  Detail & Related papers  (2024-02-16T14:04:56Z)
• Machine Learning Insides OptVerse AI Solver: Design Principles and Applications [74.67495900436728]
  We present a comprehensive study on the integration of machine learning (ML) techniques into Huawei Cloud's OptVerse AI solver. We showcase our methods for generating complex SAT and MILP instances utilizing generative models that mirror multifaceted structures of real-world problem. We detail the incorporation of state-of-the-art parameter tuning algorithms which markedly elevate solver performance.
  arXiv  Detail & Related papers  (2024-01-11T15:02:15Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.