ABSTRACT. LLMs and their capabilities to handle natural language are more and more used as an intuitive interface between non-experts users and complex algorithms. This is facilitated by the recent introduction of the Model Context Protocol (MCP). In this work, the LLMs facilitate the use of explanation algorithms by translating back their outputs into natural language adapted to the user.

ABSTRACT. Minimal Unsatisfiable Subsets are often used as a method for explaining why a CSP is unsatisfiable. While the meaning of each constraint in an MUS can be made clearer using a natural language description, the interaction between constraints can make it non-trivial to understand why an MUS is unsatisfiable. We investigate the use of Large Language Models (LLMs) for producing natural language explanations of unsatisfiable CSPs, similar to the example shown. More specifically, we are interested in a concise explanation of why a Constraint Satisfaction Problem (CSP) is unsatisfiable that is both sound and complete.

ABSTRACT. Large language models excel at code generation for mainstream programming languages but struggle with domain-specific languages such as MiniZinc, a constraint modeling language for combinatorial problems. To address this propose Learn2Zinc and investigate whether targeted fine-tuning can teach small language models (0.6B to 20B parameters) to generate syntactically correct and semantically valid MiniZinc models from natural language descriptions. Our key finding is that syntax errors dominate failures: the out-of-the-box execution accuracy of small language models is near zero. We propose cross-model error bootstrapping approach that collects syntax errors from multiple LLM runs and leverages those to curate an error correction dataset. With an ensemble of our fine-tuned models, we achieve up to 98% execution accuracy. The solution accuracy remains at 35% indicating that while syntax is learnable, constraint reasoning still remains a challenge. We open-source Learn2Zinc fine-tuning pipeline, datasets, and models for further research.

ABSTRACT. Constraint Programming (CP) is a powerful paradigm for solving combinatorial problems, yet translating natural language problem descriptions into executable models remains a significant bottleneck. While Large Language Models (LLMs) show promise in automating this translation, they often struggle with subtle semantic errors in the absence of oracle validation at test time. To address this, we introduce CP-SynC (Constraint Programming modeling with Synthesized Checkers), a multi-agent workflow for zero-shot constraint modeling in MiniZinc. CP-SynC coordinates modeling agents that generate and refine candidate models and validation agents that synthesize semantic checkers to provide feedback on semantic correctness. To mitigate noise inherent in individual LLM outputs, CP-SynC explores multiple modeling trajectories in parallel and employs selection agents to select the final model via multi-agent evidence aggregation. Extensive experiments on a benchmark of 100 CP problems show that CP-SynC substantially outperforms representative baselines in MiniZinc modeling.

ABSTRACT. Constraint programming languages such as MiniZinc provide a way of modelling a wide range of problems, enabling their solution with general-purpose constraint solvers. However, the process of turning a natural language problem description into a constraint program requires a human expert familiar with the target language. This is a barrier to broader adoption and use of constraint solvers. Large Language Models (LLMs) are excellent at processing natural language and competent at imperative programming. Recent work shows that LLMs are moderately effective at turning natural language problem descriptions into MiniZinc constraint models. However, they are relatively weak at writing MiniZinc, when compared with their ability to write conventional programs in C, Java and Python. We have previously developed the CoPTIC constraint programming system, which uses bounded model-checking to repurpose C as a declarative programming language. A CoPTIC model is a C program that checks whether a prospective solution satisfies the required constraints. As LLMs are better at writing C than MiniZinc, we posit that they will be better at turning natural language problem descriptions into CoPTIC models than into MiniZinc models. We propose to evaluate this claim using the CPEVAL benchmark.

ABSTRACT. Large Language Models (LLMs) provide a flexible interface for interpreting natural language problem descriptions, but they remain unreliable when asked to solve constrained optimisation tasks directly. We study a neuro-symbolic approach in which an LLM translates a natural language description of an optimisation problem into executable Python code using PySAT. The generated program constructs a weighted partial Maximum Satisfiability (MaxSAT) instance, invokes a MaxSAT solver, and returns the resulting assignment in a prescribed output format. In this way, the LLM is used primarily for semantic parsing and modelling, while the optimisation step is delegated to an exact symbolic solver. We outline an end-to-end pipeline consisting of natural language input, intermediate encoding plans, PySAT code generation, MaxSAT solving through RC2, and independent validation of returned solutions. This workshop abstract distils the main idea of using LLMs as natural language front-ends for solver-backed MaxSAT modelling, with the goal of making MaxSAT technology more accessible to users who do not write formal encodings by hand.

ABSTRACT. We introduce ZebraProlog, an approach for solving the Zebra Logic benchmark combining Large Language Models (LLMs) and constraint programming. We compare the performance of ZebraProlog with the logic.py approach, another approach for solving the Zebra Logic benchmark using LLMs and a constraint solver. Our approach does not go through an intermediate representation of the problem in a domain specific language, but rather directly translates to Prolog/CLP(FD) code which is then executed to find a solution. This approach contributes to clarify the benefits and costs of using an intermediate representation. Our experiments reveal two main findings: on the one hand, the DSL-based approach of logic.py gives a slight advantage in terms of success rate (91.9% for logic.py vs 84.6% for ZebraProlog). On the other hand, the DSL-free approach of ZebraProlog is 19.6% faster than logic.py.

ABSTRACT. Automatic prompt optimisation is a challenging black-box combinatorial problem central to deploying large language models (LLMs) at scale. Existing generation-based methods ignore concrete failure patterns of the current prompt, while iterative editing methods suffer from premature convergence. We introduce LEAP (Local–global Exploration for Automatic Prompting), a two-stage framework alternating between a convergence stage—targeted editing guided by verbal error feedback and multi-parent beam search—and an escape stage that activates upon stagnation and leverages the full optimisation history to generate structurally diverse candidates. On four NLP benchmarks against six baselines, LEAP achieves a mean composite score of 0.485, outperforming the nearest competitor by 7.1%.

ABSTRACT. Agent safety in high-stakes domains requires formal policy enforcement, but most existing approaches either rely on probabilistic guardrails (prompt-based steering; fine-tuned classifiers, e.g., Llama Guard \cite{inan2023llamaguard}) that offer no formal guarantees, or on hand-coded symbolic enforcement that does not scale to the breadth of real policy specifications. In this paper, we present an alternative approach: an autoformalization pipeline that translates natural language agent prompts, MCP tool descriptions, and policy documents into formally verified policies via an LLM-based generator-critic loop. These policies run in a deterministic policy harness external to the agent, which evaluates agent actions against these formal policies to decide whether those actions should be permitted. We use Cedar as our policy language, which is formally analyzable by SMT solvers \cite{cutler2024cedar}. This work draws inspiration from the LLM Modulo framework \cite{kambhampati2024llmscantplanhelp} and neurosymbolic AI. On the MedAgentBench benchmark, our autoformalized policies cover substantially more of the natural language policy than the hand-coded symbolic enforcement in prior work. We have open sourced the external harness with support for several agent scaffolds, alongside custom Cedar language bindings in Python.

ABSTRACT. We implement an agentic approach that improves constraint models. It receives a CPMpy model and three small training instances as input, autonomously creates and tests alternative CPMpy models, and outputs the variant that it considers best-performing within about fifteen minutes. We then evaluate the proposed model on three larger test instances. Our experiments on nine combinatorial optimization problems show that the generated models outperform the original models on 20 out of 27 test instances (74\%), demonstrating that autonomous agentic methods can support the improvement of constraint models.

ABSTRACT. Recent works in Constraint Programming (CP) have investigated how Large Language Models (LLMs) can assist in model formulation from natural language problem descriptions, lowering the barrier to modelling. However, even when a model is correct, solver performance remains highly sensitive to modelling choices. Formulating high-performance models that effectively prune the search space requires expertise and manual trial-and-error, through techniques such as symmetry breaking, redundant constraints, or global constraint reformulation. In this work, we explore the potential of LLMs to assist in the model optimisation process. We present and evaluate an LLM-guided iterative framework that takes an initial constraint model and a natural language problem description as input, and produces a semantically equivalent but computationally faster model. Each step of the iterative process includes a model evaluation on a set of training instances to assess the candidate model before using it in the next generation, which additionally includes solver feedback (runtime/UNSAT/error etc.). We systematically evaluate our approach on a set of diverse combinatorial problems from CSPLib, and across various strategies that configure the context at each iteration.

ABSTRACT. We present KissatEvolve, an LLM-based framework for fully automatic, scalable, and controllable synthesis of SAT solver heuristics. Modern CDCL solvers such as Kissat employ a large ensemble of tightly coupled heuristic components whose joint configuration space is prohibitively large to search exhaustively. Existing LLM-based approaches explore only a narrow slice of this space, confining search to a single solver or a small set of heuristic functions, and optimize exclusively for aggregate PAR-2 without regard for targeted problem subcategories. KissatEvolve is the first framework to address both limitations simultaneously. For scalability, KissatEvolve combines a self-adaptive agentic workflow with a fully parallelized generation-and-evaluation pipeline that spans multiple solver families and heuristic functions concurrently, substantially reducing the wall-clock time required to cover the design space while minimizing human intervention. For controllability, KissatEvolve maintains a densely annotated memory bank that records both high- and low-performing heuristic variants, each enriched with solver analyses, search statistics, and code-diff traces. Selectively retrieved examples condition subsequent LLM generations toward targeting user-specified subcategories (SAT, UNSAT, easy, or hard problems), enabling fine-grained steering of solver behavior. Using KissatEvolve, we conduct a comprehensive study of 17 heuristic functions across 6 SAT solvers, finding improved heuristics for 3 solvers that reduce PAR-2 by 12.80% on average over their respective baselines. We also find that controlled retrieval reduces PAR-2 by up to 43.76% relative to uncontrolled retrieval.

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.