{"id":"fae401c1-2d55-47e0-82a6-ab1aadfe692f","arxiv_id":"2501.14630","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"LLM-generated, encoding-specific local search functions can improve CDCL SAT solving on some structured problems, though gains are inconsistent and the best DFVS function is actually a generic WalkSAT variant.","lead":"Researchers used large language models to read the Python code that turns problems into SAT formulas, and then automatically generated custom local search programs that exploit patterns in that code. The generated programs give SAT solvers better starting points, and on some hard instances they solve problems that a plain solver cannot.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The headline comparative claim is unsupported: evaluation compares only against vanilla CDCL, not against any baseline preprocessing/local-search system, and the best DFVS function is a generic WalkSAT, so encoding-structure gains are not established.","rationale":"Read in good faith, the paper's pipeline is transparent and the authors honestly report limitations. However, the central claim in the Abstract requires either a mechanism demonstration (LLM uses encoding structure) or a comparative demonstration (beats baseline preprocessing). The test-evaluation section provides neither: no baseline preprocessing system is run, and the DFVS best function is explicitly generic WalkSAT, while the LLMs did not understand DFVS. This is exactly the gap the reader flagged. A direct comparison against generic local search is cheap, unambiguous, and would settle whether the encoding-specific component earns the result. Since the reader already conditioned acceptance on such evidence, I keep the verdict unchanged.","tokens_in":14039,"tokens_out":3395,"duration_ms":32220,"concrete_test":"Add three baselines to the §5.5 evaluation on the same DFVS test set: (i) CaDiCaL 1.9.5 with its default rephasing/local-search preprocessing, (ii) standard WalkSAT, and (iii) ProbSAT, with assignments injected as default phases exactly as for the generated functions, using the same 15-minute gather and 1-hour CDCL budget and 10 repeated runs. If the best LLM function's 12 new instances over vanilla SAT shrink to parity with generic WalkSAT/ProbSAT, the structure-exploitation and baseline-preprocessing claims fail; if it exceeds them robustly, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The Abstract claims 'faster solving times compared to baseline preprocessing systems,' and the conclusion credits the gains to targeting encoding methodology rather than instances. Neither claim is testable from the reported experiments. In §5.5, the only reference is 'the SAT solver without any local search' run for one hour; Table 1 reports Solved/New relative to that vanilla solver. No comparison is made to CaDiCaL's built-in rephasing/ProbSAT phase, CryptoMiniSat's preprocessing, or a standard WalkSAT/ProbSAT default-phase injection, even though §2.3 identifies these as the baseline preprocessing systems the paper seeks to improve on. For DFVS, the strongest result (12 new instances) comes from a function that §5.6.3 describes as 'a straightforward WalkSAT implementation,' and §5.2 reports the LLMs failed to identify the DFVS encoding's purpose. §5.6.2 adds that even wrong implementations can score well and comments often mismatch code. Thus the 12 'new' instances may reflect the benefit of any local search starting point—or the ensemble sampling of dozens of heuristics—rather than LLM-extracted structural insight. The mechanism claim and the comparative claim therefore rest on the same missing pivot: a generic local-search baseline.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an automated pipeline in which LLMs read PySAT-based SAT encoding schemes and generate specialized local search functions; the best functions, selected on training instances, are used to set default phases in the CDCL solver CaDiCaL. The pipeline has a gathering phase, a scoring phase on training instances, and a refinement phase. It is evaluated on three families of benchmarks: Graph Coloring, Directed Feedback Vertex Set (DFVS), and Bounded Depth Decision Trees (BDDT), with the headline result being that the best DFVS function solves 12 instances that the vanilla solver alone cannot solve. The authors claim that the method exploits encoding structure and achieves faster solving times compared to baseline preprocessing systems.","tokens_in":14247,"tokens_out":4752,"duration_ms":40514,"significance":"If the claims were fully supported, the paper would make a useful contribution: it proposes a reproducible, automated way to generate encoding-specific local search heuristics, and it ships code and data on Zenodo. The idea of using LLMs to analyze encodings rather than instances is original and could be of interest to the SAT/AI community. However, the current experimental validation does not establish the central comparative and mechanistic claims: no existing preprocessing or rephasing baseline is evaluated, and the paper's own analysis shows that the best DFVS function is a generic WalkSAT implementation, that the LLMs failed to understand the DFVS encoding, and that even incorrect implementations can score well. The significance therefore rests on plausible promise rather than demonstrated effect.","major_comments":[{"comment":"The evaluation compares only against 'the SAT solver without any local search' run for one hour. The abstract claims 'faster solving times compared to baseline preprocessing systems,' and §2.3 identifies CaDiCaL's ProbSAT-based rephasing and CryptoMiniSat's preprocessing as the relevant baseline systems, yet none of these is run or reported. To support the comparative claim, the authors should add these baselines (or a standard local-search phase injection such as ProbSAT/WalkSAT) under identical time and hardware conditions, and report runtime distributions, not only solved/new counts.","section":"§5.5, Table 1"},{"comment":"The mechanism claim—that gains come from extracting and exploiting encoding structure—is not established. The paper itself states that the best DFVS function is 'a straightforward WalkSAT implementation' (§5.6.3), that all LLMs 'fail to identify its overall purpose' for the DFVS encoding (§5.2), and that 'even wrong implementations can sometimes deliver good results' (§5.6.2). Consequently, the 12 additional DFVS instances may reflect the general benefit of any local-search starting point, or of sampling many heuristics in the gathering phase, rather than encoding-aware specialization. A generic local-search control (e.g., WalkSAT/ProbSAT with default-phase injection on the same instances) is needed to attribute the improvement to structure extraction; alternatively, the conclusions should be substantially weakened.","section":"§5.6.3, §5.2, §5.6.2"},{"comment":"Table 1 as printed appears internally inconsistent, which prevents interpretation of the quantitative results. For example, the Coloring benchmark is stated to have 38 test instances, yet the GPT 4o row reports 49 solved instances; in the DFVS block, the GPT o1-mini Base entry reports New=60 while Solved=30, which is impossible under the stated definitions. The table structure seems misaligned or the numbers contain errors. The authors should provide a corrected, clearly labeled table with per-variant Solved and New counts that are consistent with the benchmark sizes.","section":"Table 1"}],"minor_comments":[{"comment":"The abstract promises 'faster solving times,' but the test evaluation reports only solved-instance counts and new-instance counts, not runtimes. If the authors wish to keep this claim, they should report actual solving-time comparisons or speedups.","section":"Abstract and §5.5"},{"comment":"The sentence 'we expect a good native implementation, e.g., in C++, would run orders of magnitudes faster than the Python prototypes' is speculative and should be moved to a limitations or future-work paragraph rather than appearing in the results section.","section":"§5.5"},{"comment":"The refinement phase uses a 10% average-runtime threshold to decide whether a change is significant, but no statistical testing or variance information is reported. Given that the selection of 'best' versions is based on training scores, some measure of stability across repeated runs would strengthen the ranking procedure.","section":"§5.4 and §4.4"},{"comment":"There are typographical issues, including 'Anthropnic' for Anthropic and 'Cadical' for CaDiCaL, and several author names appear with spacing artifacts (e.g., 'V oboril'). These should be corrected in a final version.","section":"Throughout"},{"comment":"The evaluation uses a single run per LLM model, but the generation process is stochastic. Reporting the variance across multiple pipeline runs, or at least explicitly noting the single-run limitation, would improve the reproducibility assessment.","section":"§5.3 and §5.6.1"}],"recommendation":"major_revision","confidential_remarks":"The paper's core idea is timely and the artifact availability is a plus, but the empirical support for the headline claims is currently too thin. The missing baselines and the admitted generic nature of the best DFVS function are fixable with additional experiments, so I do not recommend rejection. I would encourage the editor to ask for a revision that either adds the missing baselines and a generic local-search control or substantially rewrites the claims to match the evidence. The garbled Table 1 must also be corrected before the paper can be evaluated quantitatively."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short take: this is a real proof-of-concept with a transparent pipeline and honest limitations, but the abstract overclaims. The experiments compare against plain CDCL, not against the baseline preprocessing systems named in Section 2.3 (CaDiCaL's rephasing, CryptoMiniSat's preprocessing, or a standard WalkSAT). So the headline 'faster solving times compared to baseline preprocessing systems' is unsupported as written. The DFVS result—12 new instances solved by the best refined function—is the strongest number, but Section 5.6.3 tells you that function is 'a straightforward WalkSAT implementation,' and the LLMs failed to identify the DFVS encoding's purpose. That means the gain may just be from any local search starting point, not from structure extraction.\n\nWhat is genuinely new: the gather-verify-refine loop for generating encoding-specific local search functions from PySAT code, targeting the encoding rather than instances, with cross-instance transfer. The paper ships code and data on Zenodo and is refreshingly candid about failure modes, including the polarity misunderstanding in DFVS and the mismatch between comments and code. The BDDT section is the strongest evidence for the central thesis: the best Claude-generated function respects the encoding's level structure and solved an instance reported unsolvable in six hours. That is a concrete result worth building on.\n\nSoft spots: (1) missing baseline preprocessing comparison, as above; (2) training-test correlation is weak for Coloring and BDDT, so the selection step may be fragile; (3) no repeated runs or error bars—table entries could be noise; (4) the claim in Section 2.4 that the method provides 'runtime and correctness guarantees' is overstated; the pipeline checks for timeouts and return types, not correctness. These are fixable with a proper baseline (e.g., default phases from ProbSAT or a generic WalkSAT), repeated runs, and a reworded abstract.\n\nWho benefits: anyone working on AI4SAT or automated heuristic design. It's a useful proof-of-concept, not a definitive win. I'd send it to a serious referee, expecting heavy revision before acceptance.","headline":"A genuine proof-of-concept for LLM-generated SAT preprocessing, but the comparative claim needs a proper baseline and the structure-exploitation mechanism is only partially supported.","tokens_in":14822,"tokens_out":2699,"would_cite":true,"duration_ms":24657,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that LLMs can generate encoding-specific local search preprocessing that beats baseline CDCL seeding on hard structured SAT instances.","keywords":["SAT solving","local search preprocessing","CDCL solvers","large language models","encoding structure","PySAT","Directed Feedback Vertex Set","bounded-depth decision trees"],"falsifier":"Run the pipeline a second time without showing the encoding code—prompt the LLM for generic local search functions that operate only on the CNF—and compare solved-instance counts on the same test sets; if the generic set matches the encoding-aware set on hard instances, the structure-extraction premise is false.","tokens_in":13782,"feed_emoji":"🤖","tokens_out":6092,"duration_ms":43477,"temperature":0.7,"pith_summary":"The paper claims that a large language model can read the Python code of a SAT encoding and turn it into a specialized local search routine that, when used as preprocessing for a CDCL (conflict-driven clause learning) solver, produces strong starting assignments for every instance of that encoding. The method is automatic: an LLM generates many candidate searches, a training-phase scorer ranks them, and a refinement loop with feedback improves them. On hard Directed Feedback Vertex Set instances the best generated function solves 12 instances that the solver alone could not; on graph coloring the best function solves more instances than the solver alone. The authors read the result as evidence that encoding-aware preprocessing can be synthesized rather than hand-crafted. They also report that the best DFVS function is a generic WalkSAT implementation, because the models misunderstood the DFVS encoding, which weakens the claim that structural understanding caused that particular gain.","feed_headline":"LLM-generated local search solves 12 hard SAT instances","feed_subtitle":"Automated structure-aware preprocessing beats generic seeding on directed feedback vertex set and graph coloring.","key_machinery":"The load-bearing object is the local search function generated by the LLM from the PySAT encoding code, plus the two-phase pipeline that produces it. In the gathering phase the LLM is asked only for a local search routine with a fixed interface and is given the encoding program without its name or purpose; errors are repaired and successful functions are added to the prompt context to force diversity. In the refinement phase the top functions are iteratively varied and scored on training instances, with the LLM told whether a change improved average solver runtime by more than ten percent. The generated assignment enters the solver as the default phase, and the quality of an assignment is measured by how quickly the solver finishes from that starting point.","core_discovery":"In the paper's own framing, the discovery is that the structure of a SAT encoding is a reusable asset: an LLM that inspects the encoding program can generate local search algorithms that exploit that structure, and those algorithms apply to all instances produced by the same encoding, not just one instance. The generated algorithm produces an assignment that is fed into the solver as the default phase of every variable, so the solver's search starts from a promising point. The evaluation on three encodings of increasing complexity—graph coloring, directed feedback vertex set, bounded-depth decision trees—shows that such generated preprocessors can beat the solver alone on hard instances, but the benefit is uneven: it is clearest for directed feedback vertex set, absent in aggregate for bounded-depth decision trees, and the authors explicitly note that the best DFVS search was a standard WalkSAT because the models failed to grasp the encoding's intent.","pith_inferences":["The DFVS result is consistent with a weaker hypothesis: that most of the gain comes from cheaply sampling many plausible local search heuristics and keeping the best, rather than from extracting encoding structure. The paper's own report that the winning DFVS function is generic WalkSAT supports this reading.","A direct test would be to run the same pipeline with the encoding program withheld, or replaced by a generic 'SAT formula' description, and compare solved-instance counts; if generic search matches structure-aware search, the structural explanation is not needed.","The comments in LLM-generated code often did not match what the code did, so diversity claims based on self-description are unreliable; measuring code behavior or edit distance would be a safer diversity signal.","The correlation between training and test scores was strong for DFVS but weak for coloring, implying that training-instance selection, not just the LLM, determines how well refinement generalizes."],"forward_implications":["A user who has a PySAT encoding can obtain a family of candidate local search preprocessors without manual algorithm design.","The same generated search applies to every future instance of that encoding, so the cost of generation is amortized over a benchmark family.","The refinement phase is necessary: the base versions from the gathering phase do not yield the best results.","Better LLM comprehension of the encoding correlates with better generated searches, so prompting that improves encoding understanding should improve the preprocessors.","The authors expect an efficient native implementation of the prototypes to be substantially faster than the Python versions they evaluated."],"supporting_citations":[{"why":"Establishes that local search preprocessing boosts CDCL solver performance, the premise the paper builds on.","marker":"[Balint and Manthey, 2013]"},{"why":"Introduces GSAT, the basic local search approach the generated functions build on or deviate from.","marker":"[Selman et al., 1992]"},{"why":"Introduces WalkSAT, the generic algorithm that turned out to be the best DFVS function.","marker":"[Selman et al., 1994]"},{"why":"Provides the hybrid local search plus CDCL target-phase mechanism the evaluation's default-phase seeding is based on.","marker":"[Cai et al., 2022]"},{"why":"Supplies PySAT, the Python toolkit in which the encoding schemes are written and the input the LLM reads.","marker":"[Ignatiev et al., 2018]"},{"why":"Gives the reachability-based DFVS encoding used as one of the three test cases.","marker":"[Janota et al., 2017]"},{"why":"Gives the complicated BDDT encoding used as the hardest test case.","marker":"[Shati et al., 2021]"},{"why":"Provides DAGer, used to compute optimal DFVS solutions that define the benchmark instances.","marker":"[Kiesel and Schidler, 2023]"}],"fun_headline_variants":["LLM reads code to build better SAT starting points","AI generates local search from encoding structure","LLM-tuned local search speeds up hard SAT instances","From encoding code to smarter SAT solves","Structure-aware preprocessing via LLM beats baselines"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the speedups come from encoding-aware specialization, not simply from generating and testing dozens of generic local search heuristics; the paper's own Section 5.6.3 reports the best DFVS function was a plain WalkSAT because the models did not understand the DFVS encoding.","fun_headline_variants_meta":{"raw":{"variants":["LLM reads code to build better SAT starting points","AI generates local search from encoding structure","LLM-tuned local search speeds up hard SAT instances","From encoding code to smarter SAT solves","Structure-aware preprocessing via LLM beats baselines"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000184,"raw_usage":{"total_tokens":1256,"prompt_tokens":820,"completion_tokens":436,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":436,"completion_tokens_details":{"reasoning_tokens":366}},"tokens_in":436,"tokens_out":436,"duration_ms":4154,"temperature":1.0,"reasoning_tokens":366,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T14:57:44.577067+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the pipeline a second time without showing the encoding code—prompt the LLM for generic local search functions that operate only on the CNF—and compare solved-instance counts on the same test sets; if the generic set matches the encoding-aware set on hard instances, the structure-extraction premise is false.","supporting_citations":[{"cited_title":"Boosting the performance of SLS and CDCL solvers by preprocessor tuning","cited_arxiv_id":null,"evidence_quote":"Establishes that local search preprocessing boosts CDCL solver performance, the premise the paper builds on."},{"cited_title":"Levesque, and David G","cited_arxiv_id":null,"evidence_quote":"Introduces GSAT, the basic local search approach the generated functions build on or deviate from."},{"cited_title":"Kautz, and Bram Cohen","cited_arxiv_id":null,"evidence_quote":"Introduces WalkSAT, the generic algorithm that turned out to be the best DFVS function."},{"cited_title":"Better decision heuristics in CDCL through local search and target phases","cited_arxiv_id":null,"evidence_quote":"Provides the hybrid local search plus CDCL target-phase mechanism the evaluation's default-phase seeding is based on."},{"cited_title":"On the quest for an acyclic graph","cited_arxiv_id":null,"evidence_quote":"Gives the reachability-based DFVS encoding used as one of the three test cases."},{"cited_title":"McIlraith","cited_arxiv_id":null,"evidence_quote":"Gives the complicated BDDT encoding used as the hardest test case."},{"cited_title":"A dynamic MaxSAT -based approach to directed feedback vertex sets","cited_arxiv_id":null,"evidence_quote":"Provides DAGer, used to compute optimal DFVS solutions that define the benchmark instances."}],"review_version":1}