Pith. sign in

REVIEW 3 major objections 4 minor 11 references

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

T0 review · 3 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read CoreForge shows that LLMs, guided by iterative audits and benchmarking, can build a nontrivial MaxSAT solver from research papers.

desk verdict Honest experience report that mostly delivers, but the 'from papers' claim is undercut by possible training-data recall, and the new lookahead heuristic doesn't yet beat the baseline. read the letter →

arxiv 2607.14818 v1 pith:ZLSJ7QIR submitted 2026-07-16 cs.LO cs.AI

Ruben Martins This is my paper
classification cs.LOcs.AI
keywords MaxSATlargelanguagemodelscodegenerationunsatisfiability-basedalgorithmscore-guidedsearchpaper-to-codesolverconstructionautomatedreasoning
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 reports a four-week experiment in which large language models, guided by iterative prompting, audits, fuzzing, and benchmarking, built a 25,000-line C++ MaxSAT solver from research papers rather than from an existing solver codebase. The central claim is that LLMs can support substantial solver construction from papers, though not in a one-shot or fully autonomous way: the process required repeated human-driven iteration. Across the tested configurations, the solver solved 308 of 417 selected MaxSAT Evaluation 2024 instances and no wrong answers were observed, although performance lags the strongest hand-engineered solvers. The paper also introduces a new core-sequence lookahead feature developed through the same workflow and identifies overhead control as the main technical bottleneck.

What carries the argument

The key mechanism is the iterative planning-coding-audit loop: research papers are read and discussed with ChatGPT for planning, plans become Codex prompts, generated code is audited by LLMs and revised, and fuzzing and benchmarks supply external validation. Within the solver itself, the central algorithmic machinery is the family of unsatisfiability-based MaxSAT algorithms (OLL, MSU3, PM2), which iteratively query a SAT solver for unsatisfiable cores and add cardinality constraints, plus the new core-sequence lookahead that runs bounded probes scanning alternative early core-extraction strategies before committing to the main search.

What would settle it

Run a code-clone or structural similarity analysis of CoreForge's generated components (especially its OLL implementation and cardinality encodings) against publicly available MaxSAT solvers; if large chunks match existing open-source code with only superficial edits, the paper-to-code attribution collapses. Alternatively, run the solver on a broader set of random and crafted MaxSAT instances beyond the 417-instance subset: any found wrong answer on a correct optimum would refute the no-wrong-answers claim.

Watch

Extended reading notes

Core claim

On its own terms, CoreForge is an existence proof: a capable LLM, paired with a human who selects papers, converts planning discussions into coding prompts, and runs validation, can produce a working unsatisfiability-based MaxSAT solver from scratch. The final codebase implements algorithms such as PM2, MSU3, and OLL, along with core minimization, preprocessing, and integration with SCIP and CP-SAT. The authors emphasize that this is not a one-shot generation result: more than seventy large prompts and around 120 commits were needed, and the LLM was effective at translating algorithmic ideas into code but weaker at aggressive low-level solver engineering. The observed absence of wrong answer

Load-bearing premise

The paper's 'from papers rather than from code' interpretation depends on the generated solver not being substantially shaped by MaxSAT solver code memorized in the LLM's training data, and the paper offers no evidence about code-similarity.

Editorial extensions

If this is right

  • If CoreForge's central claim holds, solver developers can use LLM-assisted paper-to-code workflows to bootstrap nontrivial constraint solvers, cutting the time to a working implementation from weeks to days while keeping humans in the loop for validation.
  • The paper's own data imply that the gap to state-of-the-art solvers is not uniform: a few benchmark families (frb, minimize-5gons) account for most lost instances, so targeted improvements on those families should yield outsized gains.
  • The VBS gap (332 vs 308 instances) shows the three configurations are complementary, meaning better instance-level selection and resource guardrails could recover much of the remaining performance without new algorithmic ideas.
  • The core-sequence lookahead feature, though preliminary, provides a concrete starting point for research on exploiting early core-sequence variation in MaxSAT solving.

Reading between the lines

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

  • A hidden dependency of the 'from papers' claim is that the LLM did not implicitly draw on memorized solver code; if the generated components closely resemble public implementations, the paper-to-code interpretation weakens. Comparing the generated code against open-source MaxSAT solvers would test this.
  • The workflow's success suggests a more general recipe: LLM-generated code for NP-hard problem solvers may be correct on tested instances but require fuzzing and delta debugging to establish trust; this experience generalizes beyond MaxSAT to other solver families.
  • The core-sequence lookahead idea could be tested independently: a careful ablation on full MaxSAT Evaluation benchmarks, with a hard wall-clock budget for probing, would reveal whether the selection rule rather than the extra CPU time drives the reported gains.
  • Beyond the paper's conclusions, the biggest open question is whether a fully autonomous agent could close the loop by running its own benchmarks and audits; CoreForge stops at human-in-the-loop validation, so the next test is a closed-loop variant.
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 / 4 minor

Summary. CoreForge is an iterative LLM-assisted project that implements an unweighted MaxSAT solver in C++ from research papers rather than from an existing solver codebase. The workflow alternates ChatGPT-based planning, Codex-based code generation, LLM-assisted audits, fuzzing, and benchmarking. Three configurations are evaluated: an OLL-style core-guided baseline, an ILP extension using SCIP/CP-SAT, and a core-sequence lookahead variant. On a 417-instance subset of MaxSAT Evaluation 2024 with known nonzero optima, the configurations solve 302–308 instances and their virtual best solves 332, remaining below the strongest solvers. No wrong answers were observed on the tested configurations. The paper’s thesis is that LLMs can support substantial solver construction from research papers when paired with iterative guidance, benchmarking, and external validation.

Significance. If the thesis holds, the paper is a useful empirical data point for LLM-assisted solver engineering and paper-to-code workflows. Its strengths are the honest hedging, explicit limitation statements, the use of external validation through fuzzing and benchmark instances, and a detailed description of a four-week, 25k-line development process. However, the central distinction "from papers rather than from an existing solver codebase" is not yet protected against the possibility that the LLM reproduced memorized solver code from pretraining; and the quantitative comparison mixes runtimes and hardware. The current value is as a credible experience report whose main attribution requires additional evidence before the paper can support strong conclusions about paper-to-code solver construction.

major comments (3)
  1. [Appendix A; Sections 2 and 3] The claim that CoreForge was built "from research papers rather than from an existing solver codebase" is load-bearing, but Appendix A's statement "No external solver code was analyzed" only excludes explicit inspection during development. It does not address whether the LLM's pretraining included public MaxSAT solver implementations (e.g., Open-WBO, RC2, Pacose, MaxHS). If substantial portions of CoreForge are near-verbatim recall of such code, the paper-to-code attribution and novelty claim would be weakened. This is not an accusation, but an untested threat to the central claim. Please provide a code-similarity/clone analysis against known open-source MaxSAT solvers, or an ablation using a model with controlled training data, and release the code to make this check possible.
  2. [Appendix D, Table 2] The comparison of solved-instance counts mixes the authors' local runs (900s timeout, single machine type) with MaxSAT Evaluation 2024 results (1200s timeout, different hardware). The footnote acknowledges this, but Section 2 still concludes that CoreForge "outperform[s] several established solvers on our benchmark subset" based on Table 2. With different timeouts and hardware, rankings by aggregate solved count are not directly comparable. For example, CoreForge baseline at 900s (308) versus Pacose at 1200s (292) cannot be interpreted as a head-to-head advantage. Please report per-instance local runtimes for all solvers compared, or restrict the "outperforms" claim to local reruns with identical timeouts and hardware.
  3. [Appendix D, experimental setup; Appendix A] The 417-instance subset is selected as instances solved by at least one MSE'24 solver and with nonzero optimum. This is reasonable for a diagnostic study, but the same benchmark instances were also used during development: Appendix A states that benchmark evaluation was run manually and guided revisions. Consequently, the reported solved-instance counts and the "no wrong answers" claim could reflect some degree of selection or overfitting to these benchmarks. The manuscript should either provide a holdout set that was not used during the iterative loop, or report results from a time-based split, to support the general claim that the workflow produces correct and robust solver configurations.
minor comments (4)
  1. [Appendix B] The core-sequence lookahead is not evaluated in isolation: the lookahead configuration differs from the ILP configuration only by lookahead, but the ILP configuration differs from the baseline by several components (initial upper bound, SCIP, CP-SAT). The attribution of gains or losses to lookahead is therefore indirect. The appendix already says it is not a finished technique; consider saying this explicitly in the evaluation discussion.
  2. [Appendix D] Figure 3 is referenced but not included in the text; the per-instance comparisons (9 instances missed by UWrMaxSat, 19 by maxcdcl, etc.) would be more informative if accompanied by a small table of per-family counts. Also, no confidence intervals or variance information are given for the local runs.
  3. [Front matter] The author field appears corrupted: "Ruben Martins/envel⌢pe/h⌢me" is likely a formatting artifact and should be fixed before publication.
  4. [Appendix A] The manuscript states the codebase contains "more than 25K lines of C++" and was developed over "around 120 Git commits," but no code or repository link is provided. Releasing the code (or at least a representative excerpt and the audit logs) would strengthen reproducibility and also help address the memorization concern above.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the paper's claims are empirical and externally benchmarked, with no prediction reduced to a fitted input or self-citation chain.

full rationale

CoreForge is an experience report rather than a formal derivation; its central claims are empirical. The claimed outcome, that LLMs can support substantial solver construction from papers, is supported by the described workflow and by external evaluation: correctness is checked against known optima from MaxSAT Evaluation 2024 instances and fuzzing, so the correctness verdict is not defined by the solver's own assumptions. The lookahead scoring in Appendix B uses 'inexpensive statistics, such as lower-bound gain, core sizes, and the number of distinct soft clauses involved' rather than parameters fitted to the benchmark, so no fitted input is renamed as a prediction. References to prior work by the author (e.g., MSU3 [7], resolution-based representations [9]) are cited as algorithm provenance, not as the justification for the conclusion about LLM capability; that conclusion rests on the development workflow, the generated codebase, and external benchmarks. The Appendix A statement 'No external solver code was analyzed' could be questioned as a validity threat regarding LLM training-data memorization, but that is a threat to the 'from papers' attribution, not a circular derivation. No equation, fitted parameter, or self-citation chain makes any result equivalent to its input. Therefore no significant circularity is present.

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

The central claim is an experience report and does not depend on a mathematical derivation. The listed free parameters are heuristic choices in the core-sequence lookahead (Appendix B) that affect performance but not the qualitative conclusion. The axioms are standard reliability assumptions about the solver algorithms, external backends, benchmark optima, and LLM training-data independence. No new physical or formal entities are introduced.

free parameters (3)
  • core-sequence probe count = 8
    Appendix B says the lookahead configuration runs eight bounded probes; the number is chosen by hand and affects the overhead/loss tradeoff reported in Appendix D.
  • probe budgets (SAT calls, conflicts per call, cores collected) = not given
    Appendix B states each probe has limits on SAT calls, conflicts per call, and cores collected, but exact values are not reported; these are hand-set and affect the lookahead configuration's balance of gains vs. losses.
  • prefix scoring statistics weights = not given
    Appendix B mentions inexpensive statistics (lower-bound gain, core sizes, distinct soft clauses) but does not give the scoring formula or weights; these choices determine strategy selection and are not fit externally.
assumptions (5)
  • domain assumption The OLL unsatisfiability-based MaxSAT algorithm from [8] is correct and is faithfully implemented by the LLM-generated code.
    Section 2 says CoreForge implements OLL; if the implementation deviates from the paper, the evaluation is measuring a different algorithm. The audits are LLM-assisted and not detailed.
  • domain assumption SCIP [1] and CP-SAT [11] behave as correct optimization backends within their timeouts.
    Appendix C relies on these backends for presolve/search; if they return incorrect results, the ILP configuration's correctness claims could be affected (though they are mature tools).
  • domain assumption MaxSAT Evaluation 2024 reference optima used for fuzzing/evaluation are correct.
    Appendix D selects instances with 'known reference optima' and compares against them; incorrect optima would invalidate the 'no wrong answers' claim.
  • domain assumption LLM outputs are not substantially contaminated by memorized MaxSAT solver code from training data.
    The study's 'from papers rather than from an existing solver codebase' premise (Section 1, Appendix A) assumes the generated components originate from the provided papers rather than from training-data recall of public solver repositories.
  • domain assumption The fuzzing methodology of Paxian and Biere [10] is sufficient to expose wrong answers in the tested configurations.
    Section 2 relies on fuzzing as a correctness check; the paper gives no fuzzing depth, instance count, or coverage statistics.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience." pith.science (2026). https://pith.science/paper/ZLSJ7QIR

@misc{pith2026260714818,
  author       = {Pith},
  title        = {Pith review of: Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZLSJ7QIR}},
  note         = {Machine review of arXiv:2607.14818}
}
read the original abstract

We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase. The project focuses on unsatisfiability-based MaxSAT algorithms and follows an iterative workflow that combines paper discussions with ChatGPT, implementation through Codex prompts, and repeated LLM-assisted code audits and revisions. Although the codebase implements several algorithms and solver components, our evaluation focuses on configurations that combine core-guided optimization, lightweight preprocessing, core minimization, integration with integer linear optimization backends, and a new core-sequence lookahead approach. Our experience suggests that LLMs can support solver implementation from papers, while requiring external validation, benchmarking, and human guidance. In our experiments, fuzzing and MaxSAT Evaluation instances did not reveal wrong answers in the tested configurations, although performance remains below the best hand-engineered MaxSAT solvers. We summarize what worked, what remained difficult, and the lessons for future LLM-assisted solver development.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

11 extracted references · 1 canonical work pages

  1. [1]

    SCIP: Solving constraint integer programs.Mathematical Programming Computation, 1(1):1–41, 2009.doi:10.1007/s12532-008-0001-1

    1 Tobias Achterberg. SCIP: Solving constraint integer programs.Mathematical Programming Computation, 1(1):1–41, 2009.doi:10.1007/s12532-008-0001-1. 2 Josep Alòs, Carlos Ansótegui, and Eduard Torres. Revisiting sat-based solvers: Maxsat rules and core sequences.Journal of Artificial Intelligence Research, 85:Article 16,

    doi:10.1007/s12532-008-0001-1 2009

  2. [8]

    Papers were used for planning, planning was converted into implementation prompts, and the resulting code was evaluated, audited, and revised across iterations

    4 Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience Papers LLM Planning LLM Coding Audit & ReviseEvaluate iterate Figure 1High-level iterative workflow used to developCoreForge. Papers were used for planning, planning was converted into implementation prompts, and the resulting code was evaluated, audited, and revised across iterations....

    arXiv 2025

  3. [9]

    17 Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang, Bingzhen Zhang, Ke Wei, and Shaowei Cai

    arXiv:2507.22876. 17 Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang, Bingzhen Zhang, Ke Wei, and Shaowei Cai. AutoSAT: Automatically Optimize SAT Solvers via Large Language Models.CoRR, abs/2402.10705, 2024.arXiv:2402.10705. 18 Cunxi Yu, Rongjian Liang, Chia-Tung Ho, and Haoxing Ren. Autonomous Code Evolution Meets NP-Completeness.CoRR, abs/2509.07367, ...

    arXiv 2024

  4. [11]

    When these backend stages do not solve the instance, the remaining search is handled by the core-guided MaxSAT engine

    as an additional optimization backend, each with a short timeout. When these backend stages do not solve the instance, the remaining search is handled by the core-guided MaxSAT engine. Ruben Martins 7 Lookahead.The lookahead configuration extends the ILP configuration with core- sequence lookahead, described in Appendix B. Before the main MaxSAT search, t...

    2024

  5. [12]

    The locally rerun baselines provide a useful calibration point. In particular,maxcdcl-openwbo300 solves the same number of instances locally as in the evaluation data, even though our runs used a 900s timeout while the MaxSAT Evaluation 2024 used a 1200s timeout. Moreover,UWrMaxSat-SCIP-MaxPre solves slightly more instances in our local setting. These res...

    2024

  6. [20]

    Uncovering and classifying bugs in maxsat solvers through fuzzing and delta debugging

    10 Tobias Paxian and Armin Biere. Uncovering and classifying bugs in maxsat solvers through fuzzing and delta debugging. InProceedings of the 14th International Workshop on Pragmatics of SAT (POS 2023), volume 3545 ofCEUR Workshop Proceedings, pages 59–71. CEUR-WS.org,

    2023

  7. [2009]

    Truong, Weixin Liang, Fan-Yun Sun, and Nick Haber

    4 Tianyu Hua, Harper Hua, Violet Xiang, Benjamin Klieger, Sang T. Truong, Weixin Liang, Fan-Yun Sun, and Nick Haber. ResearchCodeBench: Benchmarking LLMs on Implementing Novel Machine Learning Research Code.CoRR, abs/2506.02314, 2025.arXiv:2506.02314. 5 Alexey Ignatiev, António Morgado, and Joao Marques-Silva. RC2: An efficient maxsat solver.Journal on Sa...

    arXiv 2025

  8. [2019]

    6 Mikolás Janota and Mirek Olsák

    doi:10.3233/SAT190116. 6 Mikolás Janota and Mirek Olsák. LLM2SMT: Building an SMT Solver with Zero Human- Written Code.CoRR, abs/2603.06931, 2026.arXiv:2603.06931. 7 Ruben Martins, Saurabh Joshi, Vasco Manquinho, and Inês Lynce. Incremental cardinality constraints for maxsat. InProceedings of the 20th International Conference on Principles and Practice of...

    arXiv 2026

Show all 11 references
  1. [2024]

    The results should be interpreted with care because they combine runs obtained in two environments

    Comparison against other MaxSAT Evaluation 2024 solvers Table 2 comparesCoreForge against the strongest solvers on the selected 417-instance subset. The results should be interpreted with care because they combine runs obtained in two environments. Some solvers were rerun on o...

    2024

  2. [2025]

    14 Junjie Sheng, Yanqiu Lin, Jiehao Wu, Yanhong Huang, Jianqi Shi, Min Zhang, and Xiangfeng Wang

    arXiv:2504.17192. 14 Junjie Sheng, Yanqiu Lin, Jiehao Wu, Yanhong Huang, Jianqi Shi, Min Zhang, and Xiangfeng Wang. SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation. In International Conference on Software Engineering: New Ideas and Emerging Results...

    2025

  3. [2026]

    3 Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy

    doi:10.1613/jair.1.19525. 3 Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Solving weighted partial maxsat through satisfiability testing. InProceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 5584 ofLecture...

    doi

Pith tools

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