Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Extracting Problem Structure with LLMs for Optimized SAT Local Search

André Schidler, Stefan Szeider

TL;DR

The paper tackles the problem of enhancing SAT solving by exploiting structure in problem encodings. It introduces a two-phase, LLM-driven pipeline that analyzes PySAT encodings to automatically generate encoding-specific local search procedures that seed CDCL solvers, with correctness guarantees and cross-instance applicability. Evaluations on Graph Coloring, Directed Feedback Vertex Set, and Bounded Depth Decision Trees demonstrate that encoding-aware preprocessing can outperform baseline preprocessing on hard instances, though performance varies by encoding and model. The work highlights the potential of automated, structure-aware algorithm generation and points to future directions in model distillation, diversity metrics, and deeper encoding comprehension to further boost practical SAT solving performance.

Abstract

Local search preprocessing makes Conflict-Driven Clause Learning (CDCL) solvers faster by providing high-quality starting points and modern SAT solvers have incorporated this technique into their preprocessing steps. However, these tools rely on basic strategies that miss the structural patterns in problems. We present a method that applies Large Language Models (LLMs) to analyze Python-based encoding code. This reveals hidden structural patterns in how problems convert into SAT. Our method automatically generates specialized local search algorithms that find these patterns and use them to create strong initial assignments. This works for any problem instance from the same encoding type. Our tests show encouraging results, achieving faster solving times compared to baseline preprocessing systems.

Extracting Problem Structure with LLMs for Optimized SAT Local Search

TL;DR

The paper tackles the problem of enhancing SAT solving by exploiting structure in problem encodings. It introduces a two-phase, LLM-driven pipeline that analyzes PySAT encodings to automatically generate encoding-specific local search procedures that seed CDCL solvers, with correctness guarantees and cross-instance applicability. Evaluations on Graph Coloring, Directed Feedback Vertex Set, and Bounded Depth Decision Trees demonstrate that encoding-aware preprocessing can outperform baseline preprocessing on hard instances, though performance varies by encoding and model. The work highlights the potential of automated, structure-aware algorithm generation and points to future directions in model distillation, diversity metrics, and deeper encoding comprehension to further boost practical SAT solving performance.

Abstract

Local search preprocessing makes Conflict-Driven Clause Learning (CDCL) solvers faster by providing high-quality starting points and modern SAT solvers have incorporated this technique into their preprocessing steps. However, these tools rely on basic strategies that miss the structural patterns in problems. We present a method that applies Large Language Models (LLMs) to analyze Python-based encoding code. This reveals hidden structural patterns in how problems convert into SAT. Our method automatically generates specialized local search algorithms that find these patterns and use them to create strong initial assignments. This works for any problem instance from the same encoding type. Our tests show encouraging results, achieving faster solving times compared to baseline preprocessing systems.
Paper Structure (33 sections, 3 figures, 1 table)

This paper contains 33 sections, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Supplementary Material
  3. Background and Related Work
  4. SAT solving
  5. Local Search Algorithms for SAT
  6. Local Search in CDCL Solvers
  7. Machine Learning and SAT solving
  8. Problem Statement
  9. Graph Coloring (Coloring)
  10. Directed Feedback Vertex Set (DFVS)
  11. Bounded Depth Decision Trees (BDDT)
  12. Methodology
  13. Standardizing Encoding Schemes
  14. Gathering Phase
  15. Scoring
  16. ...and 18 more sections

Figures (3)

  • Figure 1: Schematic of the whole approach from the encoding scheme to pool of refined local search functions. From this pool we take the top-performing functions for the evaluation on test instances.
  • Figure 2: The top five local search functions for different problems over different refinement iterations.
  • Figure 3: Local search function scores on the training instances and test instances. Each marker represents one local search function.