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

arXiv: https://arxiv.org/abs/2607.14818 · HTML: https://mlsanity.com/paper/2607.14818/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 17 references that are in the map.
- First posted on arXiv 16 Jul 2026.

## Builds on (most cited first, 8 of 8)

- [PaperBench: Evaluating AI's Ability to Replicate AI Research](https://mlsanity.com/paper/2504.01848/) (2025)
- [Paper2Code: Automating Code Generation from Scientific Papers in Machine Learning](https://mlsanity.com/paper/2504.17192/) (2025)
- [ResearchCodeBench: Benchmarking LLMs on Implementing Novel Machine Learning Research Code](https://mlsanity.com/paper/2506.02314/) (2025)
- [AutoSAT: Automatically Optimize SAT Solvers via Large Language Models](https://mlsanity.com/paper/2402.10705/) (2024)
- [Incremental Cardinality Constraints for MaxSAT](https://mlsanity.com/paper/1408.4628/) (2014)
- [Exploiting Resolution-based Representations for MaxSAT Solving](https://mlsanity.com/paper/1505.02405/) (2015)
- [LLM2SMT: Building an SMT Solver with Zero Human-Written Code](https://mlsanity.com/paper/2603.06931/) (2026)
- [SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation](https://mlsanity.com/paper/2502.14328/) (2025)

## Abstract (arXiv)

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.