While Large Language Models (LLMs) perform exceptionally well at natural language tasks, they often struggle with precise formal reasoning and the rigorous specification of problems. We present MCP-Solver, a prototype implementation of the Model Context Protocol that demonstrates the potential for systematic integration between LLMs and constraint programming systems. Our implementation provides interfaces for the creation, editing, and validation of a constraint model. Through an item-based editing approach with integrated validation, the system ensures model consistency at every modification step and enables structured iterative refinement. The system handles concurrent solving sessions and maintains a persistent knowledge base of modeling insights. Initial experiments suggest that this integration can effectively combine LLMs' natural language understanding with constraint-solving capabilities. Our open-source implementation is proof of concept for integrating formal reasoning systems with LLMs through standardized protocols. While further research is needed to establish comprehensive formal guarantees, this work takes a first step toward principled integration of natural language processing with constraint-based reasoning.

This article presents a framework for generating optimisation models using a pre-trained generative transformer. The framework involves specifying the features that the optimisation model should have and using a language model to generate an initial version of the model. The model is then tested and validated, and if it contains build errors, an automatic edition process is triggered. An experiment was performed using MiniZinc as the target language and two GPT-3.5 language models for generation and debugging. The results show that the use of language models for the generation of optimisation models is feasible, with some models satisfying the requested specifications, while others require further refinement. The study provides promising evidence for the use of language models in the modelling of optimisation problems and suggests avenues for future research.

Ill-managed intersections are the primary reasons behind the increasing traffic problem in urban areas, leading to nonoptimal traffic-flow and unnecessary deadlocks. In this paper, we propose an automated intersection management system that extracts data from a well-defined grid of sensors and optimizes traffic flow by controlling traffic signals. The data extraction mechanism is independent of the optimization algorithm and this paper primarily emphasizes the later one. We have used MiniZinc modeling language to define our system as a constraint satisfaction problem which can be solved using any off-the-shelf solver. The proposed system performs much better than the systems currently in use. Our system reduces the mean waiting time and standard deviation of the waiting time of vehicles and avoids deadlocks.

Class Scheduling is a highly constrained task. Educational institutes spend a lot of resources, in the form of time and manual computation, to find a satisficing schedule that fulfills all the requirements. A satisficing class schedule accommodates all the students to all their desired courses at convenient timing. The scheduler also needs to take into account the availability of course teachers on the given slots. With the added limitation of available classrooms, the number of solutions satisfying all constraints in this huge search-space, further decreases. This paper proposes an efficient system to generate class schedules that can fulfill every possible need of a typical university. Though it is primarily a fixed-credit scheduler, it can be adjusted for open-credit systems as well. The model is designed in MiniZinc and solved using various off-the-shelf solvers. The proposed scheduling system can find a balanced schedule for a moderate-sized educational institute in less than a minute.

MiniZinc provides a solver-independent modeling language that is now supported by constraint-programming solvers, mixed integer programming solvers, SAT and SAT modulo theory solvers, and hybrid solvers. Every year since 2008 we have run the MiniZinc Challenge, which compares and contrasts the different strengths of different solvers and solving technologies on a set of MiniZinc models. Here we report on what we have learned from running the competition for 6 years. MiniZinc is high level enough to express most combinatorial optimization problems easily and in a largely solverindependent way; for example, it supports sets, arrays, and user-defined predicates, some overloading, and some automatic coercions. However, MiniZinc is low level enough that it can be mapped easily onto many solvers.

Recent research has shown that a single arbitrarily efficient solver can be significantly outperformed by a portfolio of possibly slower on-average solvers. The solver selection is usually done by means of (un)supervised learning techniques which exploit features extracted from the problem specification. In this paper we present an useful and flexible framework that is able to extract an extensive set of features from a Constraint (Satisfaction/Optimization) Problem defined in possibly different modeling languages: MiniZinc, FlatZinc or XCSP. We also report some empirical results showing that the performances that can be obtained using these features are effective and competitive with state of the art CSP portfolio techniques.