Search papers, labs, and topics across Lattice.
This paper details the CoreForge project, which explores the use of large language models (LLMs) to construct an unweighted MaxSAT solver directly from research papers, bypassing traditional codebases. The iterative approach integrates discussions with ChatGPT, implementation via Codex prompts, and LLM-assisted code audits, revealing that while LLMs can aid in solver development, they still require human oversight and validation. The results indicate that although the generated solver performs below the best hand-engineered counterparts, it successfully implements several algorithms without producing incorrect outputs during testing.
LLMs can effectively assist in building complex solvers from academic literature, but human oversight remains crucial for validation and performance optimization.
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.
