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

• URL: http://arxiv.org/abs/2607.14818v1
• Date: Thu, 16 Jul 2026 10:37:02 GMT
• Title: Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
• Abstract summary: We report on an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers.<n>The project focuses on unsatisfiability-based MaxSAT algorithms and follows an iterative workflow that combines paper discussions with ChatGPT.<n>We summarize what worked, what remained difficult, and the lessons for future LLM-assisted solver development.
• Score: 5.812499828391904
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability [19.16962344736341]
  Large Language Models (LLMs) excel at understanding natural language but struggle with optimisation tasks involving user-defined preferences.<n>We propose a hybrid reasoning approach in which LLMs externalise reasoning through code generation.<n>Our results demonstrate that LLM-driven code generation combined with preference-based MaxSAT enables solver-verifiable optimisation.
  arXiv  Detail & Related papers  (2026-05-28T09:51:33Z)
• FrontierOR: Benchmarking LLMs' Capacity for Efficient Algorithm Design in Large-Scale Optimization [61.43300970020897]
  Large language models (LLMs) are increasingly used for optimization modeling and solver-code generation.<n>Existing benchmarks are limited to small or simplified examples far below real-world scale and complexity.<n>We introduce FrontierOR, among the first benchmarks to evaluate LLM-based efficient algorithm design for realistic large-scale optimization problems.
  arXiv  Detail & Related papers  (2026-05-24T20:10:42Z)
• Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers [52.23061619664667]
  Large Language Models (LLMs) struggle to solve complex problems through direct reasoning, so recent neuro-symbolic systems increasingly use them to synthesize executable solvers.<n>We introduce CP-SynC-XL, a benchmark of 100 problems (4,577 instances), and evaluate three solver--construction paradigms: native algorithmic search (Python), constraint modeling through a Python solver API (Python + OR-Tools), and declarative constraint modeling.
  arXiv  Detail & Related papers  (2026-05-12T17:15:45Z)
• Execution-Verified Reinforcement Learning for Optimization Modeling [49.171122807323634]
  Execution-verified learning framework treats a mathematical programming solver as a deterministic, interactive verifier.<n>Experiments on NL4OPT, MAMO, IndustryOR, and OptiBench across Gurobi, OR-Tools, and COPT show that EVOM matches or outperforms process-supervised SFT.
  arXiv  Detail & Related papers  (2026-04-01T03:39:11Z)
• Understanding the Challenges in Iterative Generative Optimization with LLMs [19.536425405805957]
  We argue that to set up a learning loop, an engineer must make hidden'' design choices.<n>We investigate three factors that affect most applications: the starting artifact, the credit horizon for execution traces, and trials and errors into learning evidence.<n>We conclude that the lack of a simple, universal way to set up learning loops across domains is a major hurdle for productionization and adoption.
  arXiv  Detail & Related papers  (2026-03-25T06:49:24Z)
• SolverLLM: Leveraging Test-Time Scaling for Optimization Problem via LLM-Guided Search [58.116954449750544]
  We introduce a training-free framework that leverages test-time scaling to solve diverse optimization problems.<n>Rather than solving directly, it generates mathematical formulations and translates them into solver-ready code, guided by a novel Monte Carlo Tree Search strategy.
  arXiv  Detail & Related papers  (2025-10-19T16:21:19Z)
• On LLM-Assisted Generation of Smart Contracts from Business Processes [0.08192907805418582]
  Large language models (LLMs) have changed the reality of how software is produced.<n>We present an exploratory study to investigate the use of LLMs for generating smart contract code from business process descriptions.<n>Our results show that LLM performance falls short of the perfect reliability required for smart contract development.
  arXiv  Detail & Related papers  (2025-07-30T20:39:45Z)
• Do LLMs Overthink Basic Math Reasoning? Benchmarking the Accuracy-Efficiency Tradeoff in Language Models [6.312798900093575]
  Large language models (LLMs) achieve impressive performance on complex mathematical benchmarks yet sometimes fail on basic math reasoning.<n>This paper focuses on the fundamental tradeoff between accuracy and overthinking.<n>We introduce the Overthinking Score, a harmonic-mean metric combining accuracy and token-efficiency for holistic model evaluation.
  arXiv  Detail & Related papers  (2025-07-05T12:31:17Z)
• AIME: AI System Optimization via Multiple LLM Evaluators [79.03422337674664]
  AIME is an evaluation protocol that utilizes multiple LLMs that each independently generate an evaluation on separate criteria and then combine them via concatenation. We show AIME outperforming baseline methods in code generation tasks, with up to $62%$ higher error detection rate and up to $16%$ higher success rate than a single LLM evaluation protocol on LeetCodeHard and HumanEval datasets.
  arXiv  Detail & Related papers  (2024-10-04T04:03:24Z)
• Code Simulation Challenges for Large Language Models [6.970495767499435]
  This work studies to what extent Large Language Models (LLMs) can simulate coding and algorithmic tasks. We introduce benchmarks for straight-line programs, code that contains critical paths, and approximate and redundant instructions. We propose a novel off-the-shelf prompting method, Chain of Simulation (CoSm), which instructs LLMs to simulate code execution line by line/follow the pattern of compilers.
  arXiv  Detail & Related papers  (2024-01-17T09:23:59Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.