Pith. sign in

REVIEW 3 major objections 5 minor 4 cited by

Discovering heuristics in a complex SAT solver with large language models

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read LLM-guided search over a modular SAT solver's seven heuristics beats hand-tuned state-of-the-art solvers on most benchmark families.

desk verdict AutoModSAT is a serious engineering framework with strong ablation and honesty, but its headline >30% gains over SOTA are inflated by in-sample selection and need a held-out re-evaluation. read the letter →

arxiv 2507.22876 v2 pith:6YFIKLDI submitted 2025-07-30 cs.AI cs.LO

Yiwen Sun , Furong Ye , Zhihan Chen , Ke Wei , Shaowei Cai This is my paper · ORCID
classification cs.AIcs.LO MSC 68T20
keywords SATsolveroptimizationlargelanguagemodelsheuristicdiscoveryCDCLevolutionarysearchalgorithmconfigurationpromptMod
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that a large language model, pointed at a deliberately modularized SAT solver, can discover per-domain heuristics that outperform both hand-optimized and parameter-tuned state-of-the-art solvers. The framework, AutoModSAT, splits a CDCL (conflict-driven clause learning) solver into seven small heuristic functions, asks an LLM to propose rewritten versions of a few of them per iteration, prunes unpromising functions in a presearch pass, and keeps the best variant through a $(1+\lambda)$ evolutionary loop. Across 11 benchmark families the final solver improves on its modular baseline by more than 40% in PAR-2, beats the state-of-the-art solvers Kissat and CaDiCaL by an average of over 30%, and edges out their SMAC3-tuned versions on 8 of the 11 datasets. If this holds, LLM-guided heuristic discovery is a practical route for improving large, entangled solver codebases that are too complex to regenerate wholesale.

What carries the argument

The load-bearing object is ModSAT, a MiniSat-based CDCL solver whose heuristics are deliberately reorganized into seven small, focused functions (restart function, restart condition, reduce condition, rephase function, rephase condition, variable-activity bumping, and clause-activity bumping), forming the search space the LLM explores; the paper calls the resulting map from heuristics to solver $f(h_1,\dots,h_7) \mapsto A$. Three design principles make this space LLM-compatible: keep functions simple and focused, expose shared state through class member variables, and proactively prevent compile bugs. Around that core, a presearch stage evaluates each function's standalone PAR-2 impact on a half-sample and keeps about four candidates per dataset; an entropy-based prompt-optimization loop clusters CodeT5+ embeddings of generated code with K-Means++ and maximizes Shannon entropy to keep proposals diverse; and a $(1+\lambda)$ evolutionary algorithm with $\lambda=1$ runs three LLM agents (coder, evaluator, repairer), accepting a rewrite only when it improves PAR-2 on the full dataset.

What would settle it

The paper itself provides a near-falsifier: on Zamkeller, the tuned Kissat configuration's gain comes almost entirely from eliminate=0 and simplify=0, two preprocessing switches that AutoModSAT cannot touch because they lie outside the seven functions, and AutoModSAT's PAR-2 of 2052.87 stays far above Kissat para's 487.88. A decisive experiment is to extend the framework with preprocessing toggles as additional modifiable functions and check whether the Zamkeller gap closes; if the gap persists even with the space enlarged, the seven-function search space is not the binding constraint and the central claim needs qualification.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that the performance-relevant knowledge of a SAT solver can be concentrated into seven modular heuristic functions, and that LLM-proposed rewrites of those functions, filtered by evolutionary selection on a target dataset, form a genuinely new heuristic-discovery mechanism. The discovered heuristics are hybrids that blend and extend known techniques, such as a restart policy that switches between full, partial, and minimal restarts using two moving averages of LBD scores, and an activity-bumping rule scaled by the current decision level. A novelty check against 60 top solvers from SAT competitions 2020 to 2025 found no identical implementations, while some components, such as average-LBD restart measures, resemble existing ideas. Every accepted variant is correctness-checked: satisfying assignments are re-validated against the CNF, and UNSAT results are backed by DRAT proofs verified with drat-trim.

Load-bearing premise

The load-bearing premise is that ModSAT's seven modularized heuristic functions cover enough of what determines solver speed that optimizing only them can match or beat solvers whose speed also comes from mechanisms outside these functions, such as preprocessing switches and architectural choices.

Editorial extensions

If this is right

  • LLM-proposed heuristic rewrites beat global parameter tuning as an optimization lever for SAT solvers: AutoModSAT outperforms SMAC3-tuned Kissat and CaDiCaL on 8 of 11 datasets in both PAR-2 and solved-instance counts.
  • Domain specialization becomes cheap: each dataset gets its own evolved heuristic set in roughly 50 search iterations at about one to two minutes per iteration.
  • Complex solvers that cannot be regenerated by LLMs wholesale can still be improved by modularizing their heuristics, a recipe the paper suggests transfers beyond SAT to other large, entangled solver codebases.
  • The discovered heuristics mix known ideas with new rules, such as decision-level-scaled activity bumps and progress-sensitive restart thresholds, showing the search does not merely rediscover existing solver techniques.
  • Correctness survives automated mutation: every accepted solver's SAT assignments are re-verified against the formula and every UNSAT verdict carries a drat-trim-checked DRAT proof.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper's implicit trade-off is that ModSAT's known performance deficit against Kissat and CaDiCaL is repaid by the discoverability of its heuristic space; Zamkeller marks where that trade-off fails, because the winning move there is a preprocessing switch outside the seven functions.
  • A natural extension is to add top-level preprocessing controls as additional modular functions; the paper's own ablation suggests this would narrow the Zamkeller gap, though the weak ModSAT baseline on that family may still leave a deficit.
  • The entropy-maximizing prompt-optimization loop is label-free and evaluation-free during prompt selection, so it could transfer to other expensive black-box code-optimization tasks where supervised prompt tuning is impractical.
  • A concrete deployment concern follows from the paper's own admission that the generated restart function uses static local variables: verifying instance isolation before parallel or multi-solver use is advisable, and comparing conflict and decision statistics across solver copies is a cheap regression test.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents AutoModSAT, a framework that uses LLMs to search over seven modularized heuristic functions in ModSAT, a MiniSat-based CDCL solver. The pipeline consists of a modular solver, a presearch stage that prunes functions based on standalone PAR-2 on a 50% subset, entropy-based automatic prompt optimization, and a (1+lambda) evolutionary search with LLM coder/evaluator/repairer agents. The authors report PAR-2 and solved-instance counts on 11 datasets, claiming over 40% improvement over ModSAT and over 30% over Kissat and CaDiCaL, with a further comparison to SMAC3-tuned variants. They also provide analyses of discovered heuristics, ablations, in-domain and cross-domain generalization tests, and DRAT/assignment correctness verification.

Significance. If the reported gains were obtained under a matched evaluation protocol, the paper would be a significant step: it demonstrates that LLM-guided search over a small, well-chosen set of heuristic functions can produce competitive domain-specialized SAT solvers, with a concrete modularization methodology and new heuristic designs. The release of code and datasets, the use of DRAT proof checking for UNSAT instances, and the inclusion of generalization and ablation studies are strengths. The current main-text quantitative claims are, however, not yet established because the headline numbers are computed on the same instances used for heuristic selection and because generalization is demonstrated on only five of eleven families.

major comments (3)
  1. [Methods, Presearch strategy, Algorithm 4, and Table 2] The headline PAR-2 numbers in Table 2 are in-sample. The presearch evaluates candidate functions on a 50% subset of P, and Algorithm 4 then evaluates every retained candidate on the full dataset P and keeps any improvement, over 50 evaluations. The final PAR-2 in Table 2 is computed on the same instances used for selection, whereas the SMAC3 baselines are described as configured on instance-specific training datasets and validated on a testing dataset. This asymmetry means the stated 40% and 30% gains conflate optimization progress with selection on the evaluation set; for families with only 20 to 88 instances, selection on the same set can explain a substantial part of the gain. Please report results on a held-out split that is not used during search for all 11 families, or explicitly re-label the headline numbers as in-sample.
  2. [Supplementary Section 4.6, Tables 11-13] In-domain generalization is tested for only 5 of the 11 families (argumentation, hamiltonian, social-golfer, MineSweeper, and KnightTour). The remaining six families, including EDA, register-allocation, and Zamkeller, have no held-out evaluation, so the claim that AutoModSAT outperforms state-of-the-art solvers on those families is not established beyond the exact instances used in the search. Moreover, the cross-domain tables show that a heuristic selected on one family can be catastrophic on another, for example the social-golfer solver on register-allocation gives PAR-2 9646.80 with 1 solved instance versus 1177.80 with 18 solved in-domain. This confirms the risk of selection on the reported set and motivates a matched held-out protocol before the quantitative headline claims are accepted.
  3. [Results, PAR-2 comparison paragraph] The sentence 'AutoModSAT exhibits substantial improvements over the SOTA solvers Kissat and CaDiCaL on each dataset' is contradicted by Table 2 on Zamkeller: AutoModSAT has PAR-2 2052.87 while CaDiCaL has 1930.20, so AutoModSAT does not beat CaDiCaL on that dataset. The subsequent qualification about parameter-tuned variants covers only 8 of 11 datasets. Please correct this overstatement, for example by saying that AutoModSAT is better on most datasets and is not uniformly best.
minor comments (5)
  1. [Results, speedup definition] The quantity defined as speedup = (va - vb) / max(va, vb) is a relative improvement in PAR-2, not a speedup in the usual sense; please rename it to 'relative PAR-2 improvement' or define it more carefully.
  2. [Table 2 caption and Figure 3] Please clarify whether the ten random seeds in Table 2 correspond to ten independent AutoModSAT search runs or to ten evaluations of one discovered solver; the text is currently ambiguous.
  3. [Methods, Automatic prompt optimization and Supplementary Algorithm 5] Several constants needed to reproduce prompt optimization are missing: the number of clusters K in K-Means++ is never specified, and the thresholds d and 'threshold' for accepting a prompt update in Supplementary Algorithm 5 are not reported. Please provide these values in the text or in the supplementary material.
  4. [Supplementary Section 5.2, Novelty assessment] The claim that no discovered heuristic is identical to existing ones should be worded as 'no identical implementation was found in the collected 60-solver corpus', because the assessment depends on the corpus and on the reliability of the LLM-as-a-judge procedure, for which no inter-annotator agreement or false-negative rate is reported.
  5. [Results, LLM agent runtime] The reported per-agent times of about 20 seconds are given with confidence intervals, but the number of samples used to compute those intervals is not stated; please report the sample size and the conditions under which the timing was measured.

Circularity Check

1 steps flagged · score 6.0 of 10

Headline Table 2 PAR-2 gains are in-sample: AutoModSAT is selected on the same dataset P used for final evaluation, so the >30% SOTA claim is an optimized training score, not a held-out prediction.

  1. fitted input called prediction [Methods, 'Presearch strategy' and 'Heuristics discovery' (Algorithm 4); Results, Table 2]
    "Subsequently, we execute a (1 + λ) EA on the full dataset using this refined function set... f (A0) evaluate(A0, P); if f (A0)≤ f* then A A0; f* f (A0). ... After obtaining the optimized solver, the original 5000 seconds timeout is used for the final evaluation."

    Algorithm 4 accepts a candidate only when its PAR-2 on the full dataset P is no worse than the current best, so the final solver is selected by minimizing PAR-2 on P. Table 2 then reports PAR-2 on that same P as the headline 'over 40% performance improvement relative to ModSAT' and 'average performance gain exceeding 30%' over Kissat/CaDiCaL. The reported gain is therefore the optimized training objective, not an independent held-out prediction; by contrast, the SMAC3 baselines are 'validated on the testing dataset'. The in-domain generalization tests cover only 5 of 11 families, so the central quantitative claim is partly a selection artifact.

full rationale

The paper is an empirical optimization study, not a mathematical derivation, so most circularity patterns do not apply. No load-bearing self-citation chain or imported uniqueness theorem is present; comparisons to prior work are contextual. The one significant circular element is the evaluation protocol: the heuristic search and the headline Table 2 numbers use the same dataset P. Algorithm 4's acceptance criterion is PAR-2 on P, making the final AutoModSAT a fitted solution; reporting its PAR-2 on P as a 'performance gain' reduces to reporting the optimized objective. The in-domain generalization tests provide some independent evidence for 5 families, and cross-domain tests honestly show overfitting, but they do not replace a held-out split for the headline claims. The result is therefore partially circular rather than fully self-contained.

Assumptions & free parameters 7 free parameters · 5 assumptions · 0 invented entities

No new physical or mathematical entities are introduced. The free parameters are the constants inside LLM-generated heuristics, plus a few framework hyperparameters chosen by hand. The axioms are the standard correctness of the base CDCL solver, the completeness of the seven-function search space, the reliability of LLM agents after verification, and the adequacy of the presearch and EA components.

free parameters (7)
  • restart_function moving-average weights = fast=0.9, slow=0.99
    Generated by the LLM in the discovered restart_function and retained because they improved PAR-2 on the training datasets. The paper notes these constants lack interpretability.
  • restart depth thresholds = 1.2 (full), 1.0 (partial), else minimal
    Ratios of fast_avg/slow_avg in restart_function that decide full, partial, or minimal restart. No derivation; selected via search.
  • rephase policy probabilities = 0.4 local-best, 0.3 invert, 0.2 random low-activity, 0.1 user phases
    Discovered rephase_function uses these probability values; they are LLM outputs chosen by performance on data.
  • varBumpActivity scaling constants = 1.0+0.1*decisionLevel(), 1e-100 threshold and floor
    Discovered varBumpActivity uses these constants. Values are LLM-generated and selected on data.
  • claBumpActivity decay adjustment = conflict_scale = 1.0 - 0.01*(lbd_queue_size/50), floor 0.8
    Discovered claBumpActivity uses this formula. No theoretical derivation is provided.
  • presearch retention count = 4 functions
    Hand-chosen number of functions kept after presearch; not derived from data (Methods, Presearch strategy).
  • K-Means cluster count K = not specified in text
    Prompt optimization clusters code embeddings into K clusters; the value of K is not given in the manuscript, leaving a reproducibility gap.
assumptions (5)
  • domain assumption The CDCL algorithm as implemented in MiniSat and extended with rephasing is correct for SAT/UNSAT decisions.
    Standard, widely verified algorithm; the paper relies on it as the base solver.
  • ad hoc to paper The seven heuristic functions (restart condition/function, reduce condition, rephase condition/function, var/cla bump activity) capture the performance-critical degrees of freedom in a CDCL solver.
    This is the design decision that makes the search space small enough for LLMs; the Zamkeller ablation shows preprocessing toggles are missing, so the assumption is not universally valid.
  • domain assumption LLM-generated code can be made correct often enough by the coder/evaluator/repairer loop, and correctness is verified by SAT assignment checks and DRAT proofs.
    The entire search depends on generated code compiling and behaving correctly; the paper provides an automated verification pipeline (Supplementary Section 4.7).
  • ad hoc to paper Presearch pruning based on standalone PAR-2 impact on a 50% subset preserves the functions that matter in combination.
    The strategy assumes weak interaction effects among the seven functions; no interaction analysis is provided for ModSAT's functions.
  • domain assumption The (1+lambda) EA with lambda=1 and budget 50 iterations is an adequate search procedure for this landscape.
    Standard EA assumption; convergence curves are shown only for a few datasets, and the budget is small relative to the 5,000 second evaluation cost.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Discovering heuristics in a complex SAT solver with large language models." pith.science (2026). https://pith.science/paper/6YFIKLDI

@misc{pith2026250722876,
  author       = {Pith},
  title        = {Pith review of: Discovering heuristics in a complex SAT solver with large language models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6YFIKLDI}},
  note         = {Machine review of arXiv:2507.22876}
}
abstract

The Satisfiability problem (SAT) is fundamental in computational complexity theory and has a wide range of industrial applications. Optimizing modern SAT solvers in real-world settings is quite challenging due to their intricate architectures. While automatic configuration frameworks have been developed, they rely on manually constrained search spaces. Here we develop AutoModSAT, a framework that uses large language models (LLMs) to automatically optimize SAT solvers. AutoModSAT combines an LLM-compatible modular solver design, unsupervised prompt optimization to diversify generated functions, and an efficient search procedure based on presearch strategy and a $(1+\lambda)$ evolutionary algorithm. Extensive experiments across a wide range of datasets demonstrate that AutoModSAT achieves $40\%$ performance improvement over the baseline solver and $30\%$ improvement over the state-of-the-art solvers. Moreover, AutoModSAT also attains a notable speedup compared to the parameter-tuned alternatives of the state-of-the-art solvers over most of the test datasets. These results demonstrate the potential of LLM-guided heuristic discovery for optimizing complex SAT solvers.

Figures

Figures reproduced from arXiv: 2507.22876 by the authors.

Figure 1
Figure 1. Overview of AutoModSAT. This figure displays the workflow of AutoModSAT, which distinguishes itself from existing LLMs methods for algorithm design on challenges in optimizing large-scale, structurally complex solvers. The whole process requires a basic CDCL algorithm, initial prompt, and datasets as input, then involves four core components: (1) a modularizing SAT solver (ModSAT) based on the CDCL algorithm; (2) a … view at source ↗
Figure 2
Figure 2. PAR-2 over Different Datasets. (a) This subfigure provides a visualization of PAR-2 in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Iteration Process over Different Datasets. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (17 more)
Figure 4
Figure 4. Figure 4: This figure shows two effective LLM-generated heuristic functions for SAT solvers and their original counterparts. (Left) The claBumpActivity function innovatively scales activity increments based on the solver’s current decision level. Both functions introduce unprece…
Figure 5
Figure 5. Figure 5: Heuristic discovery. This procedure iteratively implements LLMs agents to generate new heuristics. Heuristics that passed a synonymous check are evaluated on the datasets and higher-performing heuristics are integrated back into the new solver, while failures trigger a…
Figure 6
Figure 6. Figure 6: Illustration of principle maintain functions simple and focus. a function contributes to the final performance improvement in each experiment, see Supplementary [PITH_FULL_IMAGE:figures/full_fig_p019_6.png]
Figure 7
Figure 7. Figure 7: Illustration of principle maintain functions simple and focus. Algorithm 3: Presearch Strategy in AutoModSAT 1 Input: Datasets P, modularized SAT solver with seven functions {h1,...,h7}, prompt template, baseline functions {b1,...,b7} 2 Pcompact ← 50% representative in…
Figure 8
Figure 8. Figure 8: Illustration of principle utilize class variables for shared information. Prevent bugs: add more packages # include < math .h > # include < unordered_set > # include < algorithm > using namespace std ; [PITH_FULL_IMAGE:figures/full_fig_p021_8.png]
Figure 9
Figure 9. Figure 9: Illustration of principle proactively prevent bugs during heuristics discovery. Algorithm 4: Heuristics Discovery Strategy in AutoModSAT 1 Input: Datasets P, modularized SAT solver with pruned four functions {h1,...,h4}, prompt template, baseline functions {b1,...,b4} …
Figure 10
Figure 10. Figure 10: Illustration of principle proactively prevent bugs during heuristics discovery. • Argumentation involves finding acceptable sets of arguments in a directed graph where attacks between arguments are represented by edges. • Social Golfer is a combinatorial problem that …
Figure 11
Figure 11. Figure 11: Function contribution: where the vertical axis lists different function candidates and the horizontal axis denotes the frequency of contributions. • KnightTour Parameter Θ: {k}; Parameter Space: [12,75]; Notes: A k × k chessboard where a knight’s tour is attempted, co…
Figure 12
Figure 12. Figure 12: Comparison of original prompt and optimized prompt For example, consider a benchmark dataset with three instances and a timeout bound T = 100 seconds. The runtimes (in seconds) for the three instances are: t1 = 80 for instance 1, t2 = 120 for instance 2, the solver fa…
Figure 13
Figure 13. Figure 13: Convergence behavior of AutoModSAT with and without presearch [PITH_FULL_IMAGE:figures/full_fig_p029_13.png]
Figure 14
Figure 14. Figure 14: Example of LLM discovered heuristics of claBumpActivity 34/41 [PITH_FULL_IMAGE:figures/full_fig_p034_14.png]
Figure 15
Figure 15. Figure 15: Example of LLM discovered heuristics of varBumpActivity 35/41 [PITH_FULL_IMAGE:figures/full_fig_p035_15.png]
Figure 16
Figure 16. Figure 16: Example of LLM discovered heuristics of restart condition 36/41 [PITH_FULL_IMAGE:figures/full_fig_p036_16.png]
Figure 17
Figure 17. Figure 17: Example of LLM discovered heuristics of restart function 37/41 [PITH_FULL_IMAGE:figures/full_fig_p037_17.png]
Figure 18
Figure 18. Figure 18: Example of LLM discovered heuristics of rephase condition 38/41 [PITH_FULL_IMAGE:figures/full_fig_p038_18.png]
Figure 19
Figure 19. Figure 19: Example of LLM discovered heuristics of rephase function 40/41 [PITH_FULL_IMAGE:figures/full_fig_p040_19.png]
Figure 20
Figure 20. Figure 20: Example of LLM discovered heuristics of reduce condition 41/41 [PITH_FULL_IMAGE:figures/full_fig_p041_20.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Autonomous Code Evolution Meets NP-Completeness

    cs.AI 2025-09 conditional novelty 7.0 of 10

    An LLM-based agent framework evolved five 2024 SAT solver codebases over 70 cycles and produced solvers that the authors report outperform the 2025 SAT Competition champions.

  2. AutoPBO: LLM-powered Optimization for Local Search PBO Solvers

    cs.AI 2025-09 conditional novelty 5.0 of 10

    An LLM multi-agent framework with a structured solver refactoring automatically improves pseudo-Boolean optimization local search heuristics, outperforming the authors' NuPBO-based baseline and rivaling Gurobi on seve...

  3. Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience

    cs.LO 2026-07 conditional novelty 4.0 of 10

    An LLM-assisted workflow turned MaxSAT papers into a working C++ solver; it solves 308 of 417 selected benchmarks with no observed wrong answers, still below state-of-the-art.

  4. From Heuristic Selection to Automated Algorithm Design: LLMs Benefit from Strong Priors

    cs.LG 2026-03 conditional novelty 4.0 of 10

    Prompting LLMs with strong benchmark algorithm code, rather than relying on linguistic instructions, improves LLM-driven black-box optimization; the proposed BAG method outperforms five baselines on pbo and bbob.

Reference graph

Works this paper leans on

65 extracted references · 54 canonical work pages · cited by 4 Pith papers

  1. [1]

    Cook, S. A. The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 151–158 (1971)

    work page 1971

  2. [2]

    & Zhou, X

    Gong, W. & Zhou, X. A survey of SA T solver. In AIP Conference Proceedings, vol. 1836, 1–10 (2017)

    work page 2017

  3. [3]

    Alouneh, S., Abed, S., Al Shayeji, M. H. & Mesleh, R. A comprehensive study and analysis on SA T-solvers: advances, usages and achievements. Artif. Intell. Rev. 52, 2575–2601 (2019)

    work page 2019

  4. [4]

    Fang, W. et al. A survey of circuit foundation model: Foundation AI models for VLSI circuit design and EDA. arXiv preprint arXiv:2504.03711 (2025)

    arXiv 2025

  5. [5]

    H., Hutter, F

    Hoos, H. H., Hutter, F. & Leyton-Brown, K. Automated configuration and selection of sat solvers. In Handbook of Satisfiability, 481–507 (IOS press, 2021)

    work page 2021

  6. [6]

    & V an Den Herik, H

    Beskyd, F., Surynek, P ., Rocha, A., Steels, L. & V an Den Herik, H. Parameter setting in sat solver using machine learning techniques. In ICAART (2), 586–597 (2022)

    work page 2022

  7. [7]

    & Dutheillet, C

    Saouli, S., Baarir, S. & Dutheillet, C. Improving SA T solver performance through MLP-predicted genetic algorithm parameters. In International Conference on Integrated F ormal Methods, 288–296 (2024). 13/41

    work page 2024

  8. [8]

    Achiam, J. et al. GPT-4 technical report. arXiv preprint arXiv:2303.08774 (2023)

    arXiv 2023

Show all 65 references
  1. [9]

    Liu, A. et al. Deepseek-V3 technical report. arXiv preprint arXiv:2412.19437 (2024)

    2024 arXiv

  2. [10]

    Guo, D. et al. Deepseek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning. arXiv preprint arXiv:2501.12948 (2025)

    2025 arXiv

  3. [11]

    Bai, J. et al. Qwen technical report. arXiv preprint arXiv:2309.16609 (2023)

    2023 arXiv

  4. [12]

    Qwen3 technical report

    Y ang, A.et al. Qwen3 technical report. arXiv preprint arXiv:2505.09388 (2025)

    2025 arXiv

  5. [13]

    Touvron, H. et al. Llama: Open and efficient foundation language models. arXiv preprint arXiv:2302.13971 (2023)

    2023 arXiv

  6. [14]

    Team, G. et al. Gemini: a family of highly capable multimodal models. arXiv preprint arXiv:2312.11805 (2023)

    2023 arXiv

  7. [15]

    Liu, F. et al. A systematic survey on large language models for algorithm design. arXiv preprint arXiv:2410.14716 (2024)

    2024

  8. [16]

    Romera-Paredes, B. et al. Mathematical discoveries from program search with large language models. Nature 625, 468–475 (2024)

    2024

  9. [17]

    Liu, F. et al. Evolution of heuristics: Towards efficient automatic algorithm design using large language model. In the 41st International Conference on Machine Learning (2024)

    2024

  10. [18]

    Y e, H. et al. Reevo: Large language models as hyper-heuristics with reflective evolution. Adv. neural information processing systems 37, 43571–43608 (2024)

    2024

  11. [19]

    AutoSA T: Automatically optimize SA T solvers via large language models.arXiv preprint arXiv:2402.10705 (2024)

    Sun, Y .et al. AutoSA T: Automatically optimize SA T solvers via large language models.arXiv preprint arXiv:2402.10705 (2024)

    2024 arXiv

  12. [20]

    & Zhang, Y

    Jiang, X., Wu, Y ., Zhang, C. & Zhang, Y . DRoC: Elevating large language models for complex vehicle routing via decomposed retrieval of constraints. In 13th international Conference on Learning Representations (2025)

    2025

  13. [21]

    Dat, P . V . T., Doan, L. & Binh, H. T. T. Hsevo: Elevating automatic heuristic design with diversity-driven harmony search and genetic algorithm using LLMs. In Proceedings of the AAAI Conference on Artificial Intelligence , vol. 39, 26931–26938 (2025)

    2025

  14. [22]

    & Szeider, S

    Schidler, A. & Szeider, S. Extracting problem structure with llms for optimized sat local search. In Proceedings of the International Symposium on Combinatorial Search , vol. 18, 236–240 (2025)

    2025

  15. [23]

    Novikov, A. et al. AlphaEvolve: A coding agent for scientific and algorithmic discovery. arXiv preprint arXiv:2506.13131 (2025)

    2025 arXiv

  16. [24]

    & Heisinger, M

    Biere, A., Fazekas, K., Fleury, M. & Heisinger, M. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SA T competition 2020. In Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions , vol. B-2020-1 of Department of Computer Science Report Seri...

    2020

  17. [25]

    Cadical at the sat race 2019

    Biere, A. Cadical at the sat race 2019. In Proceedings of SAT Competition 2019: Solver and Benchmark Descriptions , vol. 2019, 8–9 (Department of Computer Science, University of Helsinki, 2019)

    2019

  18. [26]

    & Neumann, F

    Doerr, B. & Neumann, F. Theory of evolutionary computation: Recent developments in discrete optimization (Spring Nature, 2019)

    2019

  19. [27]

    & Suda, M

    Balyo, T., Heule, M., Iser, M., Järvisalo, M. & Suda, M. (eds.) Proceedings of SAT Competition 2023: Solver , Benchmark and Proof Checker Descriptions (Department of Computer Science, University of Helsinki, 2023)

    2023

  20. [28]

    Heule, M. J. H., Iser, M., Järvisalo, M. & Suda, M. (eds.) Proceedings of SAT Competition 2024: Solver , Benchmark and Proof Checker Descriptions (Department of Computer Science, University of Helsinki, 2024)

    2024

  21. [29]

    & Fruhman, J

    Zhou, N.-F., Kjellerstrand, H. & Fruhman, J. Constraint solving and planning with Picat , vol. 11 (Springer, 2015)

    2015

  22. [30]

    & Een, N

    Sorensson, N. & Een, N. Minisat v1.13-a sat solver with conflict-clause minimization. SAT 2005, 1–2 (2005)

    2005

  23. [31]

    Lindauer, M. et al. SMAC3: A versatile Bayesian optimization package for hyperparameter optimization. J. Mach. Learn. Res. 23, 1–9 (2022)

    2022

  24. [32]

    Marques-Silva, J. P . & Sakallah, K. A. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Comput. 48, 506–521 (1999)

    1999

  25. [33]

    & Bäck, T

    Doerr, C., Y e, F., van Rijn, S., Wang, H. & Bäck, T. Towards a theory-guided benchmarking suite for discrete black-box optimization heuristics: profiling (1+ λ ) ea variants on onemax and leadingones. In Proceedings of the Genetic and Evolutionary Computation Conference, 951–9...

    2018

  26. [34]

    & Bäck, T

    Y e, F., Wang, H., Doerr, C. & Bäck, T. Benchmarking a genetic algorithm with configurable crossover probability. In International Conference on Parallel Problem Solving from Nature, 699–713 (Springer, 2020)

    2020

  27. [35]

    & Kötzing, T

    Doerr, B., Doerr, C. & Kötzing, T. Static and self-adjusting mutation strengths for multi-valued decision variables. Algorithmica 80, 1732–1768 (2018)

    2018

  28. [36]

    OpenAI API Documentation

    OpenAI. OpenAI API Documentation. https://platform.openai.com/docs (2023)

    2023

  29. [37]

    & Nakatumba-Nabende, J

    Marvin, G., Hellen, N., Jjingo, D. & Nakatumba-Nabende, J. Prompt engineering in large language models. In Interna- tional Conference on Data Intelligence and Cognitive Informatics , 387–402 (2023)

    2023

  30. [38]

    S., Reid, M., Matsuo, Y

    Kojima, T., Gu, S. S., Reid, M., Matsuo, Y . & Iwasawa, Y . Large language models are zero-shot reasoners. Adv. Neural Inf. Process. Syst. 35, 22199–22213 (2022)

    2022

  31. [39]

    Large language models are human-level prompt engineers

    Zhou, Y .et al. Large language models are human-level prompt engineers. In The Eleventh International Conference on Learning Representations (2022)

    2022

  32. [40]

    Pryzant, R. et al. Automatic prompt optimization with gradient descent and beam search. In Conference on Empirical Methods in Natural Language Processing , 7957–7968 (2023)

    2023

  33. [41]

    CodeT5+: Open code large language models for code understanding and generation

    Wang, Y .et al. CodeT5+: Open code large language models for code understanding and generation. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing , 1069–1088 (2023)

    2023

  34. [42]

    Google C++ Style Guide

    Google. Google C++ Style Guide. https://google.github.io/styleguide/cppguide.html (2025)

    2025

  35. [43]

    & V assilvitskii, S

    Arthur, D. & V assilvitskii, S. k-means++ the advantages of careful seeding. In Proceedings of the eighteenth annual ACM-SIAM symposium on Discrete algorithms , 1027–1035 (2007)

    2007

  36. [44]

    Wetzler, N., Heule, M. J. H. & Jr., W. A. H. Drat-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing , vol. 8561, 422–429 (Springer, 2014)

    2014

  37. [45]

    & Walsh, T

    Biere, A., Heule, M., van Maaren, H. & Walsh, T. Conflict-driven clause learning sat solvers. Handb. Satisf. Front. Artif. Intell. Appl. 4, 131–153 (2009)

    2009

  38. [46]

    H., Ganesh, V ., Poupart, P

    Liang, J. H., Ganesh, V ., Poupart, P . & Czarnecki, K. Learning rate based branching heuristic for SA T solvers. In Theory and Applications of Satisfiability Testing–SAT 2016: 19th International Conference , 123–140 (2016)

    2016

  39. [47]

    & Heule, M

    Ramos, A., V an Der Tak, P . & Heule, M. J. Between restarts and backjumps. In Theory and Applications of Satisfiability Testing-SAT 2011: 14th International Conference, SAT, 216–229 (2011)

    2011

  40. [48]

    & Zuckerman, D

    Luby, M., Sinclair, A. & Zuckerman, D. Optimal speedup of las vegas algorithms. Inf. Process. Lett. 47, 173–180 (1993)

    1993

  41. [49]

    & Simon, L

    Audemard, G. & Simon, L. Glucose 2.1: Aggressive, but reactive, clause database management, dynamic restarts. In Pragmatics of SAT 2012 (2012)

    2012

  42. [50]

    & Fröhlich, A

    Biere, A. & Fröhlich, A. Evaluating cdcl restart schemes. In Proceedings of Pragmatics of SAT, 1–17 (2015)

    2015

  43. [51]

    Lingeling, plingeling, picosat and precosat at sat race 2010

    Biere, A. Lingeling, plingeling, picosat and precosat at sat race 2010. FMVReport Ser. Tech. Rep. 10 (2010)

    2010

  44. [52]

    Jeroslow, R. G. & Wang, J. Solving propositional satisfiability problems. Annals mathematics Artif. Intell. 1, 167–187 (1990)

    1990

  45. [53]

    Strangenight

    Soos, M. Strangenight. In Proceedings of SAT Competition 2013: Solver , Benchmark and Proof Checker Descriptions , 89–90 (Department of Computer Science, University of Helsinki, 2013)

    2013

  46. [54]

    max : Both types must be integers ( int or long int )

    Balint, A., Belov, A., Järvisalo, M. & Sinz, C. Overview and analysis of the sat challenge 2012 solver competition. Artif. Intell. 223, 120–155 (2015). Acknowledgments We thank the anonymous reviewers for their constructive comments, which helped improve the manuscript. We als...

    2015

  47. [55]

    Y our rewritten function code must start with ”’// start function name”’ and end with ”’// end function name”’

  48. [56]

    Y our rewritten function(s) code must be different from original code, not just rewrite code synonymous!

  49. [57]

    Y ou are not allowed to create your own new global variables, but you can use the global variables existing in the <key code>

    Y ou are not allowed to create your own new function(s) in the rewritten function(s). Y ou are not allowed to create your own new global variables, but you can use the global variables existing in the <key code>

  50. [58]

    <key code> of SA T solver is: {{ replace_key_code }} Updated Prompt (Role) Y ou are a SA T solver researcher trying to improve the {{ func_name }} function

    Make sure the rewritten function(s) code can be executed correctly. <key code> of SA T solver is: {{ replace_key_code }} Updated Prompt (Role) Y ou are a SA T solver researcher trying to improve the {{ func_name }} function. (Goal) Objective: Y our goal is to improve the SA T ...

  51. [59]

    Carefully read and comprehend the <key code> of the SA T solver provided below

  52. [60]

    Analyze potential improvements and devise a strategy for optimizing the heuristics of function

  53. [61]

    Deliver your improved function(s) with the following format: - Begin with: ‘// start function name‘ - End with: ‘// end function name‘ (Tips) Tips:

  54. [62]

    Ensure that your rewritten function(s) are substantially different from the original, beyond mere synonym replacements

  55. [63]

    Y ou may utilize existing global variables from the <key code>, but refrain from introducing new global variables

  56. [64]

    "" {{ replace_key_code }}

    V erify that the rewritten function(s) execute correctly. Take a deep breath and think it step by step. <key code> of SA T solver is: """ {{ replace_key_code }} """ ... Figure 12. Comparison of original prompt and optimized prompt For example, consider a benchmark dataset with...

  57. [65]

    similar ideas

    Then • since t1 B, we have τ1 = 80; • since t2 > B, we have τ2 = 200 (penalized); • since the solver fails for instance 3, we have τ3 = 200 (penalized). 25/41 Therefore, the PAR-2 score is given by PAR-2 = 1 3 (80 + 200 + 200) = 480 3 = 160. Table 4. Configuration of training s...

    2000

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.