LLMs meet Constraint Solving 2026
FLOC & CP 2026 Workshop
Sunday July 19, 2026
Location: Room C5.08, Building 2, Edifício II - ISCTE
FLOC & CP 2026 Workshop
Sunday July 19, 2026
Location: Room C5.08, Building 2, Edifício II - ISCTE
09:00 - 09:50: Invited talk
Tias Guns: “Conversational Combinatorial Optimisation”
09:50 - 10:30: Session “Explanations with LLMs”
K. Feltus, V. Poucet, H. Verhaeghe
“Towards Human Readable Explanations” [paper]
I. Bleukx, T. Guns
“Large Language Models for Explaining Unsatisfiable Constraint Satisfaction Problems” [paper]
10:30 - 11:00: Coffee break
11:00 - 12:40: Session “LLMs for Constraint Modelling and Symbolic Problem Solving”
K. Uppuluri, S. Kadioglu
“Learn2Zinc: Fine-tuning Small Language Models for Text-to-Model Translation in MiniZinc” [paper]
Y. Song, E. Cohen
“CP-SynC: Multi-Agent Zero-Shot Constraint Modeling in MiniZinc with Synthesized Checkers” [paper] [slides] [video]
M. Lester
“Using LLMs to Generate CoPTIC Constraint Models” [paper]
P. Orvalho, M. Kwiatkowska, G. Alenyà, F. Manyà
“Solving MaxSAT Problems from Natural Language Descriptions with LLMs and PySAT” [paper]
A. Salah, É. Lozes, P. Urso
“ZebraProlog: Solving the Zebra Logic Benchmark with the Help of Prolog and CLP(FD)” [paper]
12:40 - 14:00: Lunch break
14:00 - 14:50: Invited talk
Vijay Ganesh: “Auto-Formalization and Proof Synthesis via Semantic Alignment Models”
14:50 - 15:30: Session “Formal Methods for LLMs”
E. Averkova, N. Kulin
“Escaping Local Optima in Prompt Optimisation via Failure-Driven Refinement and History-Guided Restarting”
A. Mondl, M. Maisel, J. Brock
“Controlling Agent Behavior with Policy-as-Code via Autoformalization” [paper]
15:30 - 16:00: Coffee break
16:00 - 17:20: Session “LLMs for Improving Solvers and Models”
F. Voboril, S. Szeider
“Improving Constraint Models with LLM Agents” [paper]
K. Michailidis, D. Tsouros, N. Dang, T. Guns
“LLM-Guided Constraint Model Reformulation for Solving Efficiency” [paper]
M. Gopalan, J. Lu, J. Song, S. Zhang, H. Nguyen, W. Chen, V. Ganesh
“KissatEvolve: Controllable and Scalable Synthesis of SAT Heuristics with Densely Annotated Memory Bank” [paper]
R. Martins
“Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience” [paper]
17:20 - 17:30: Closing remarks
Title: Conversational Combinatorial Optimisation
Abstract: Combinatorial optimisation is widely used to solve scheduling, sequencing, rostering, routing and other assignment problems. State-of-the-art CP and MIP solvers can compute optimal solutions to increasingly large problems, but they require to /model/ the problem into formal constraints.
In today's LLM-fueled world, do we still need modeling languages? What does it mean to correctly model a problem, and how can we systematically evaluate the correctness of a model, the capabilities of LLMs, and the scaffolding needed to get the most out of autoformulating LLMs?
I will share 2.5 years of experience in trying to answer these questions. The culmination is DCP-Bench-Open, an open collaborative benchmark for Discrete Combinatorial Problems that will never be finished.
Title: Auto-Formalization and Proof Synthesis via Semantic Alignment Models
Abstract: Recent years have seen a powerful symbiosis between large language models (LLMs) and formal tools such as provers, solvers, and computer algebra systems — driving dramatic breakthroughs in AI for mathematics. Building on this trend, our research group has pursued two complementary lines of work.
The first centers on the idea that high-quality joint embeddings (JEs) can substantially improve the effectiveness of auto-formalization, and more generally, AI for math tools. We define a JE as "good" if it satisfies the following invariant: semantically aligned but formally dissimilar objects — such as paired natural-language and formal-language proofs — must lie close together in the embedding space, while semantically misaligned objects must be well-separated. We incorporate these JE-based semantic alignment models (SAMs) into a RAG-based auto-formalization pipeline, demonstrating that SAMs represent a critical enabling technology for AI-assisted mathematics. The second line of work introduces Reinforcement Learning with Symbolic Feedback (RLSF), a family of techniques designed to address LLM hallucination in domains—such as mathematics, physics, and programming—where rich symbolic feedback is available. We demonstrate that RLSF methods are equally essential to advancing the state of the art in AI for mathematics.
Brief Bio: Dr. Vijay Ganesh (https://vganesh1.github.io/) is a Professor of Computer Science at Georgia Tech and Associate Director of the Institute for Data Engineering and Science (IDEaS). He is also a co-founder and Steering Committee member of the Centre for Mathematical AI at the Fields Institute, and an AI Fellow at the Balsillie School of International Affairs (BSIA) in Waterloo, Canada. Before joining Georgia Tech in 2023, Vijay was a Professor at the University of Waterloo (2012–2023), co-Director of the Waterloo AI Institute (2021–2023), and a Research Scientist at MIT (2007–2012). He earned his PhD in Computer Science from Stanford University in 2007.
Vijay's research spans the theory and practice of SAT/SMT solvers, the integration of machine learning with automated reasoning, and their applications in neurosymbolic AI for mathematics, physics, and software engineering. He has led the development of numerous SAT/SMT solvers—most notably STP, the Z3str family of string solvers, Z3-alpha, MapleSAT, AlphaMapleSAT, and MathCheck—as well as several neurosymbolic AI tools targeting mathematics, physics, and software engineering. His theoretical work encompasses mathematical logic and proof complexity. Vijay's contributions have been recognized with over 35 awards, honors, and medals, including the ACM Impact Paper Award at ISSTA 2019, the ACM Test of Time Award at CCS 2016, and a Ten-Year Most Influential Paper citation at DATE 2008.
The second edition of LLMs meet Constraint Solving (LLM-Solve) will take place on July 19, 2026, at the University Institute of Lisbon (ISCTE) Campus in the city center of Lisbon, Portugal as part of the Federated Logic Conference (FLoC'26) and Constraint Programming (CP'26).
FLoC'26: https://www.floc26.org/venue
CP'26: https://cp2026.a4cp.org/
LLM-Solve submission page: https://submissions.floc26.org/llm-solve/
Submission deadline: May 15, 2026
Notification: May 25, 2026
Workshop date: July 19, 2026
Large Language Models (LLMs) have rapidly evolved from purely natural‑language tools into powerful agentic systems capable of orchestrating complex tasks, interacting with external tools, and executing multi‑step reasoning workflows. This new generation of models promises transformative applications across scientific discovery, automation, and decision support. Yet despite their impressive versatility, LLMs still struggle with consistency, reliability, and formal correctness—limitations that become critical when deploying autonomous agents in domains requiring structured reasoning, constraint satisfaction, or guaranteed solution quality.
On the other hand, constraint-solving technologies such as CP/SAT/OR provide mature frameworks for modeling and solving combinatorial problems with provable guarantees on correctness, optimality, and explainability. However, the need for expert knowledge in formalizing problems, selecting appropriate modeling abstractions, and choosing suitable solving techniques continues to limit the broader adoption of these powerful methods.
Bringing LLMs and constraint solving together opens new opportunities on both sides: LLMs can support non-experts in model formulation, constraint acquisition, and interactive problem solving, while constraint solvers can serve as execution engines, verification modules, and structured reasoning components for LLM-driven agents. Recent research has shown promising results in both directions—from LLM-assisted constraint modeling and hybrid search to solver-backed LLM validation, correction, and planning.
The LLM-Solve 2026 workshop aims to unite researchers working at this rapidly evolving frontier to discuss challenges, synergies, and future research directions. The workshop seeks to shape the emerging landscape of LLM‑powered constraint solving and constraint‑driven LLM architectures.
The LLM-Solve 2026 workshop aims to bring together researchers exploring the intersection of Large Language Models (LLMs) and Constraint Solving (CP, SAT, SMT, MIP, and related paradigms). This workshop provides a platform to discuss recent advances, challenges, and opportunities in combining LLMs and constraint solving.
The workshop covers both directions of this interaction:
LLMs for Constraint Solving: Investigating how LLMs and agentic systems can be used to tackle challenges in constraint solving research, i.e., assist in constraint modeling, solving, and explanations; including automated constraint acquisition, solver configuration and selection, solver heuristics, automated solver code generation and natural-language based solving and solution refinement.
Constraint Solving for LLMs: Exploring how constraint-solving techniques can improve LLM reasoning and verification, LLM safety, and applications in structure reasoning, formal verification, and more.
The topics of interest include (but are not restricted to):
LLMs and agentic systems for constraint modeling and acquisition
LLM-guided solver heuristics and search strategies
Hybrid approaches combining LLMs and constraint solvers
Constraint solvers for improving LLM reasoning and verification
SAT/CP-based methods for controlling or guiding LLM outputs
LLM-driven explanations and interactive constraint solving
Benchmarks, datasets and evaluation methodologies for LLM-Constraint integration
Real-world applications involving the use of constraint-solving technologies and LLMs.
This workshop welcomes contributions from both theoretical and applied perspectives, fostering discussions between researchers in CP, SAT, AI, OR, and NLP who are interested in bridging the gap between constraint solving and natural language processing with LLMs.
Authors are invited to send contributions in the form of extended abstracts (up to 2 pages, without counting references). The authors can optionally add up to 10 pages as appendix. Submissions can be published journal/conference papers, original work, work in progress with preliminary results, or position papers. The review process is single-blind, i.e., submissions should include identifying information about the authors and their organization. There is no need to anonymize the paper artifacts, such as code, notebooks, datasets, or any other external resources.
Contributions should be submitted in the form of a PDF file, following LIPIcs guidelines: https://submission.dagstuhl.de/series/details/5#author
The workshop co-chairs will select the papers to be presented at the workshop according to their suitability to the aims. All presenters and attendees are expected to register for the FLOC workshop day.
Submission web page: https://submissions.floc26.org/llm-solve/
The workshop co-chairs are:
Tias Guns (KU Leuven, Belgium), https://people.cs.kuleuven.be/~tias.guns/
Serdar Kadıoglu (Brown University, USA), https://skadio.github.io/
Stefan Szeider (TU Wien, Austria), https://www.ac.tuwien.ac.at/people/szeider/
Dimos Tsouros (UOWM, Greece), https://dimostsouros.github.io/