{"id":"05d598ec-f701-4c99-94ab-d50948039494","arxiv_id":"2507.22876","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":7,"one_line_summary":"LLM-guided evolutionary search over seven modularized SAT solver heuristics yields solvers that beat tuned Kissat and CaDiCaL on most of eleven test families.","lead":"AutoModSAT is a new framework that uses large language models to automatically rewrite seven heuristic functions inside a SAT solver, then keeps the best-performing versions. On eleven benchmark families it reports lower average solving times than the classic solvers MiniSat, Kissat, and CaDiCaL, including their automatically tuned variants.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Headline Table 2 gains may be in-sample: AutoModSAT is selected on the same instances reported, while SMAC3 baselines are validated on held-out test sets; matched held-out evaluation is needed before claiming >30% over SOTA.","rationale":"Read in good faith, AutoModSAT is a serious engineering contribution. The modularization principles are sensible, the correctness pipeline (SAT assignment checks, DRAT proof verification via drat-trim, cross-solver consistency) is genuine independent support, the ablations quantify component contributions, and the Zamkeller analysis honestly identifies a limitation of the seven-function search space. The paper's claim, however, is quantitative: \"over 40% improvement over ModSAT\" and \"average performance gain exceeding 30%\" over SOTA. Those numbers come from Table 2. The methods text and Algorithm 4 indicate the solver is evaluated and selected on the full dataset P, with no held-out split described for the main results, while the SMAC3 baseline section explicitly describes training and testing protocols. If this asymmetry exists, the headline comparison is not apples-to-apples and the gain is at least partly an artifact of selection on the evaluation set. The reader's weakest assumption (seven functions cannot express preprocessing switches) is a genuine limitation, but it is not the primary threat: Zamkeller is one family, and the claim about \"most families\" can survive losing one. The in-sample evaluation threat applies to every family. A held-out re-run is feasible and would settle the issue; if the gains persist on held-out instances, the central claim is much stronger. For these reasons, the CONDITIONAL verdict is appropriate, with the condition being a matched held-out evaluation.","tokens_in":33504,"tokens_out":4855,"duration_ms":60715,"concrete_test":"Hold out a fixed 30% of instances per family before any AutoModSAT computation. Run presearch and (1+λ) EA on the remaining 70%, then evaluate the final solver only on the held-out 30% with the 5000s timeout. Run SMAC3 for Kissat, CaDiCaL, and ModSAT with the identical split and budget. Recompute the average PAR-2 gain and win-count from the held-out cells. If the held-out average gain over Kissat/CaDiCaL is below 30% or AutoModSAT wins on fewer than 6 of 11 families, the paper's headline claim needs qualification.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim rests on Table 2, where AutoModSAT's PAR-2 is computed after 50 iterations of (1+λ) EA. In Methods (\"Presearch strategy\"), presearch runs on a 50% subset and then \"we execute a (1+λ) EA on the full dataset\"; Algorithm 4 evaluates candidates on the full dataset P and keeps improvements selected on that P. The final evaluation then uses the 5000s timeout on the same instances. Thus every Table 2 AutoModSAT entry is the result of selection on the evaluation set. By contrast, the SMAC3 protocol is described with \"instance-specific training datasets\" and \"validated on the testing dataset\". If AutoModSAT was not held out under the same split, the >30% average gain over Kissat/CaDiCaL and the >40% gain over ModSAT conflate optimization progress with test-set selection. With 20–88 instances per family, overfitting is plausible: cross-domain tables show the same discovered heuristic can be catastrophic on other families (e.g., the social-golfer solver on register-allocation), and the in-domain generalization tests cover only 5 of 11 families. This does not invalidate the framework, but it means the headline quantitative claim is not yet established.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":33854,"tokens_out":6838,"duration_ms":82991,"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":[{"comment":"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.","section":"Methods, Presearch strategy, Algorithm 4, and Table 2"},{"comment":"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.","section":"Supplementary Section 4.6, Tables 11-13"},{"comment":"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.","section":"Results, PAR-2 comparison paragraph"}],"minor_comments":[{"comment":"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.","section":"Results, speedup definition"},{"comment":"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.","section":"Table 2 caption and Figure 3"},{"comment":"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.","section":"Methods, Automatic prompt optimization and Supplementary Algorithm 5"},{"comment":"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.","section":"Supplementary Section 5.2, Novelty assessment"},{"comment":"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.","section":"Results, LLM agent runtime"}],"recommendation":"major_revision","confidential_remarks":"The central idea is promising and the authors are transparent about several limitations, including the Zamkeller case and the restriction to the seven modularized functions. The main blocker is the experimental protocol: the headline results are computed on the same instances used for selection, and the held-out evidence covers only a subset of families. I would support publication after a matched held-out evaluation and correction of the overstatement in the Results section."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a real engineering contribution that deserves a serious referee, but the headline numbers are not yet established because the optimization selects on the same instances used for final evaluation.\n\nWhat's new: the framework combines modularization principles for SAT solvers, presearch pruning of function candidates, entropy-based prompt optimization, and a (1+λ) EA with coder/evaluator/repairer agents. The ablation study shows each component contributes. The correctness verification, including DRAT proof checking for UNSAT and independent assignment checking for SAT, is solid. The Zamkeller analysis is a model of honest investigation: they show that Kissat para's huge gain comes from eliminate=0 and simplify=0, which are outside the seven functions, and they say so plainly. The novelty assessment against a 60-solver corpus with manual verification is a good-faith effort. Code and data are on Zenodo.\n\nThe soft spot is the evaluation protocol. Algorithm 4 runs the (1+λ) EA on the full dataset P, and the final PAR-2 uses the same instances. The SMAC3 baselines use instance-specific training sets and validate on held-out test sets. So the reported >30% average gain over Kissat/CaDiCaL and >40% over ModSAT conflates test-set selection with generalization. The in-domain generalization tests cover only 5 of 11 families, and the cross-domain tables show catastrophic failures on other families. This does not invalidate the framework, but the quantitative headline is not yet supported. Also missing is a benchmark against AutoSAT, their own direct predecessor, which would calibrate the incremental contribution. The discovered heuristics contain fitted constants and static local variables; the paper flags both, which is good, but it means the heuristics are not directly usable in parallel solvers.\n\nVerdict: this paper deserves a serious referee. The protocol issue is fixable with a held-out re-run, and the framework is solid enough to warrant the effort. I'd bring it to reading group as a case study in evaluating LLM-based algorithm design.","headline":"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.","tokens_in":34319,"tokens_out":2786,"would_cite":true,"duration_ms":34136,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68T20"],"pacs":[],"model":"deepseek-v4-flash","headline":"LLM-guided search over a modular SAT solver's seven heuristics beats hand-tuned state-of-the-art solvers on most benchmark families.","keywords":["SAT solver optimization","large language models","heuristic discovery","CDCL","evolutionary search","algorithm configuration","prompt optimization","ModSAT"],"falsifier":"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.","tokens_in":33310,"feed_emoji":"🤖","tokens_out":13903,"duration_ms":134546,"temperature":0.7,"pith_summary":"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.","feed_headline":"LLM heuristics beat tuned Kissat and CaDiCaL on 8 of 11 SAT families","feed_subtitle":"AutoModSAT evolves per-dataset solver code with an LLM, cutting PAR-2 by 40% over its own baseline.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"ModSAT is built by augmenting and modularizing this MiniSat solver; it supplies the starting codebase the LLM rewrites.","marker":"[30]"},{"why":"The CDCL conflict-analysis algorithm that defines ModSAT's search architecture and the seven heuristic slots.","marker":"[32]"},{"why":"Kissat, one of the two state-of-the-art solvers that AutoModSAT must outperform.","marker":"[24]"},{"why":"CaDiCaL, the other state-of-the-art baseline, included in both default and parameter-tuned forms.","marker":"[25]"},{"why":"SMAC3 Bayesian configuration produces the parameter-tuned baselines that AutoModSAT is compared against.","marker":"[31]"},{"why":"The prior LLM-based SAT-solver optimization work whose manually constrained search space AutoModSAT targets.","marker":"[19]"},{"why":"DeepSeek-V3 is the LLM used as coder, evaluator, and repairer in the main experiments.","marker":"[9]"},{"why":"CodeT5+ supplies code embeddings for the entropy-based diversity metric in prompt optimization.","marker":"[41]"},{"why":"drat-trim verifies the UNSAT proofs that certify the correctness of generated solver variants.","marker":"[44]"},{"why":"Provides the (1+lambda) evolutionary algorithm that drives the heuristic search loop.","marker":"[26]"}],"fun_headline_variants":["LLM-evolved heuristics outpace tuned Kissat and CaDiCaL on 8 of 11 SAT families","AutoModSAT: LLM search finds SAT heuristics cutting runtime 40%","LLM-guided heuristics beat state-of-the-art SAT solvers by 30%","LLM discovers modular SAT heuristics via evolutionary search"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["LLM-evolved heuristics outpace tuned Kissat and CaDiCaL on 8 of 11 SAT families","AutoModSAT: LLM search finds SAT heuristics cutting runtime 40%","LLM-guided heuristics beat state-of-the-art SAT solvers by 30%","LLM discovers modular SAT heuristics via evolutionary search"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000867,"raw_usage":{"total_tokens":3748,"prompt_tokens":927,"completion_tokens":2821,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":543,"completion_tokens_details":{"reasoning_tokens":2740}},"tokens_in":543,"tokens_out":2821,"duration_ms":24738,"temperature":1.0,"reasoning_tokens":2740,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T11:11:51.700565+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"& Een, N","cited_arxiv_id":null,"evidence_quote":"ModSAT is built by augmenting and modularizing this MiniSat solver; it supplies the starting codebase the LLM rewrites."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The CDCL conflict-analysis algorithm that defines ModSAT's search architecture and the seven heuristic slots."},{"cited_title":"& Heisinger, M","cited_arxiv_id":null,"evidence_quote":"Kissat, one of the two state-of-the-art solvers that AutoModSAT must outperform."},{"cited_title":"Cadical at the sat race 2019","cited_arxiv_id":null,"evidence_quote":"CaDiCaL, the other state-of-the-art baseline, included in both default and parameter-tuned forms."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"SMAC3 Bayesian configuration produces the parameter-tuned baselines that AutoModSAT is compared against."},{"cited_title":"CodeT5+: Open code large language models for code understanding and generation","cited_arxiv_id":null,"evidence_quote":"CodeT5+ supplies code embeddings for the entropy-based diversity metric in prompt optimization."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"drat-trim verifies the UNSAT proofs that certify the correctness of generated solver variants."},{"cited_title":"& Neumann, F","cited_arxiv_id":null,"evidence_quote":"Provides the (1+lambda) evolutionary algorithm that drives the heuristic search loop."}],"review_version":1}