mcp-solver

MCP-Solver

Ein Model Context Protocol (MCP)-Server, der SAT-, SMT- und Constraint-Lösungsfunktionen für große Sprachmodelle bereitstellt.

Überblick

Der MCP Solver integriert SAT, SMT und Constraint Solving mit LLMs über das Model Context Protocol und ermöglicht KI-Modellen die interaktive Erstellung, Bearbeitung und Lösung von:

• Constraint-Modelle in MiniZinc
• SAT-Modelle in PySAT
• SMT-Formeln in Z3 Python

Eine detaillierte Beschreibung der Systemarchitektur und der theoretischen Grundlagen des MCP-Solvers finden Sie im begleitenden Forschungspapier: Stefan Szeider, „MCP-Solver: Integrating Language Models with Constraint Programming Systems“ , arXiv:2501.00539, 2024.

Verfügbare Tools

Im Folgenden bezieht sich „Element“ auf einen Teil des Codes (MinZinc/Pysat/Z3) und „Modell“ auf die Kodierung.

Systemanforderungen

• Python und Projektmanager uv
• Python 3.11+
• Modusspezifische Anforderungen: MiniZinc, PySAT, Python Z3 (erforderliche Pakete werden über Pip installiert)
• Betriebssysteme: macOS, Windows, Linux (mit entsprechenden Anpassungen)

Installation

MCP Solver erfordert Python 3.11+, den uv Paketmanager und solverspezifische Abhängigkeiten (MiniZinc, Z3 oder PySAT).

Ausführliche Installationsanweisungen für Windows, macOS und Linux finden Sie unter INSTALL.md .

Schnellstart:

Verfügbare Modi / Lösen von Backends

Der MCP-Solver bietet drei verschiedene Betriebsmodi, die jeweils mit einem anderen Backend zur Constraint-Lösung integriert sind. Jeder Modus erfordert spezifische Abhängigkeiten und bietet einzigartige Funktionen zur Lösung unterschiedlicher Problemklassen.

MiniZinc-Modus

Der MiniZinc-Modus ermöglicht die Integration mit der MiniZinc-Einschränkungsmodellierungssprache mit den folgenden Funktionen:

• Umfangreicher Einschränkungsausdruck mit globalen Einschränkungen
• Integration mit dem Chuffed-Constraint-Solver
• Optimierungsmöglichkeiten
• Zugriff auf Lösungswerte über get_solution

Abhängigkeiten : Erfordert das minizinc Paket ( uv pip install -e ".[mzn]" )

Konfiguration : Um im MiniZinc-Modus zu laufen, verwenden Sie:

PySAT-Modus

Der PySAT-Modus ermöglicht die Interaktion mit dem Python SAT-Lösungs-Toolkit mit den folgenden Funktionen:

• Propositionale Constraint-Modellierung mit CNF (Konjunktive Normalform)
• Zugriff auf verschiedene SAT-Solver (Glucose3, Glucose4, Lingeling usw.)
• Kardinalitätsbeschränkungen (höchstens k, mindestens k, genau k)
• Unterstützung für die Lösung boolescher Einschränkungen

Abhängigkeiten : Erfordert das Paket python-sat ( uv pip install -e ".[pysat]" )

Konfiguration : Um im PySAT-Modus zu laufen, verwenden Sie:

Z3-Modus

Der Z3-Modus bietet Zugriff auf die Lösungsfunktionen von Z3 SMT (Satisfiability Modulo Theories) mit den folgenden Funktionen:

• Umfangreiches Typsystem: Boolesche Werte, Ganzzahlen, Realzahlen, Bitvektoren, Arrays
• Constraint-Lösung mit Quantifizierern
• Optimierungsmöglichkeiten
• Vorlagenbibliothek für gängige Modellierungsmuster

Abhängigkeiten : Erfordert das z3-solver Paket ( uv pip install -e ".[z3]" )

Konfiguration : Um im Z3-Modus zu laufen, verwenden Sie:

MCP-Testclient

Der MCP Solver enthält einen MCP-Client für Entwicklungs-, Experimentier- und Diagnosezwecke, basierend auf dem ReAct -Agenten-Framework. Dieser Client dient als Vermittler zwischen einem LLM und dem MCP-Server und erleichtert die Übersetzung natürlichsprachlicher Problemstellungen in formale Constraint-Programmierungslösungen.

Installation

Der Client benötigt einen API-Schlüssel von einem LLM-Anbieter. Für Anthropic (das Standard-LLM ist Claude Sonnet 3.7) setzen Sie die Umgebungsvariable ANTHROPIC_API_KEY . Diese kann in Ihrer Umgebung festgelegt oder in einer .env Datei im Projektstammverzeichnis eingefügt werden.

Der Client unterstützt auch andere LLM-Anbieter, darunter OpenAI, Google (Gemini), OpenRouter und sogar lokale Modelle über LM Studio. Sie können das zu verwendende Modell mit dem Kommandozeilenflag --mc angeben. Details zu den Modellcodeformaten finden Sie in INSTALL.md .

Verwendung

Der Client stellt spezielle Befehle für jedes Solver-Backend bereit:

Beispiele

Beispiel 1: Gussproblem (MiniZinc)

Dies basiert auf einem Beispiel von George Johnson (NYT, 13. Juli 1999).

Benutzer

Angenommen, ein Theaterregisseur fühlt sich verpflichtet, entweder seine junge Frau, die Schauspielerin Alvarez, oder seinen Neffen, den Schauspieler Cohen, in einer Produktion zu besetzen. Doch Miss Alvarez will nicht mit Mr. Cohen (ihrem ehemaligen Liebhaber) in einem Stück mitspielen und verlangt daher, dass ihre neue Flamme, der Schauspieler Davenport, in die Besetzung aufgenommen wird. Der Produzent, der sich selbst revanchieren muss, besteht darauf, dass Schauspieler Branislavsky eine Rolle bekommt. Doch Mr. Branislavsky will in keinem Stück mit Miss Alvarez oder Mr. Davenport mitspielen. Kann der Regisseur das Stück besetzen?

System: clear_model

Model cleared

System: add_item (mehrere)

var bool: alvarez; var bool: cohen; var bool: branislavsky; var bool: davenport; constraint alvarez \/ cohen; % Must cast either Alvarez or Cohen constraint not (alvarez /\ cohen); % Alvarez won't work with Cohen constraint alvarez -> davenport; % If Alvarez is cast, Davenport must be cast constraint branislavsky; % Branislavsky must be cast constraint not (branislavsky /\ alvarez); % Branislavsky won't work with Alvarez constraint not (branislavsky /\ davenport); % Branislavsky won't work with Davenport solve satisfy;

System: solve_model

{'status': 'SAT', 'solution': Solution(alvarez=False, cohen=True, branislavsky=True, davenport=False, _checker=''), 'solve_time': 0.0}

Die Lösung (Cohen und Branislavsky besetzen, aber nicht Alvarez oder Davenport) erfüllt alle Einschränkungen.

Beispiel 2: N-Damen-Problem (MiniZinc)

Benutzer

Überprüfe, ob du n Damen auf einem nxn Schachbrett platzieren kannst. Versuche n=10,20,30,40 und vergleiche die Lösungszeiten.

System: clear_model

Model cleared

System: add_item (mehrere)

int: n = 10; array[1..n] of var 1..n: queens; constraint alldifferent(queens); constraint alldifferent([queens[i] + i | i in 1..n]); constraint alldifferent([queens[i] - i | i in 1..n]); solve satisfy;

System: solve_model (mit n=10, 20, 30 und 40 durch Ändern des Wertes von n)

Vergleich der Lösungszeiten: n=10: 0,001 s n=20: 0,005 s n=30: 0,040 s n=40: 0,043 s

Für alle getesteten Platinengrößen gibt es Lösungen. Die Zeitkomplexität steigt nichtlinear an, bleibt aber bis n=40 beherrschbar.

Beispiel 3: Problem des Handlungsreisenden (MiniZinc)

Benutzer

Eine Verkäuferin aus Wien plant ihre nächste Österreich-Tour und besucht dabei jede Landeshauptstadt einmal. Helfen Sie mit, die kürzeste Route zu finden. Entfernungen in km: 1=Wien, 2=St. Pölten, 3=Eisenstadt, 4=Linz, 5=Graz, 6=Klagenfurt, 7=Salzburg, 8=Innsbruck, 9=Bregenz

[Distanzmatrixtabelle in Benutzernachricht bereitgestellt]

System: add_item (mehrere)

include "globals.mzn"; int: n = 9; array[1..n,1..n] of int: dist = [|0,65,60,184,195,319,299,478,631|65,0,125,119,130,254,234,413,566|60,125,0,184,157,281,261,440,593|184,119,184,0,208,252,136,315,468|195,130,157,208,0,136,280,459,629|319,254,281,252,136,0,217,391,566|299,234,261,136,280,217,0,188,343|478,413,440,315,459,391,188,0,157|631,566,593,468,629,566,343,157,0|]; array[1..n] of var 1..n: succ; var int: total_dist = sum(i in 1..n)(dist[i,succ[i]]); constraint circuit(succ); solve minimize total_dist;

System: solve_model

{'status': 'SAT', 'solution': Solution(objective=1564, succ=[2, 4, 1, 7, 3, 5, 9, 6, 8], _checker=''), 'solve_time': 0.002}

Optimale Route: Wien → St. Pölten → Linz → Salzburg → Bregenz → Innsbruck → Klagenfurt → Graz → Eisenstadt → Wien mit einer Gesamtstrecke von 1.564 km.

Rückmeldung

Über dieses Formular können Sie dem Autor Feedback geben.

Haftungsausschluss

Dieser MCP-Solver befindet sich im Prototypstadium und sollte mit Vorsicht verwendet werden. Benutzer werden ermutigt, zu experimentieren, aber die Verwendung in kritischen Umgebungen erfolgt auf eigene Gefahr.

Lizenz

Dieses Projekt ist unter der MIT-Lizenz lizenziert – Einzelheiten finden Sie in der Datei LICENSE .