mcp-solver

MCP 솔버

대규모 언어 모델에 SAT, SMT 및 제약 조건 해결 기능을 제공하는 MCP(모델 컨텍스트 프로토콜) 서버입니다.

개요

MCP Solver는 모델 컨텍스트 프로토콜을 통해 SAT, SMT 및 제약 조건 해결을 LLM과 통합하여 AI 모델이 다음을 대화형으로 생성, 편집 및 해결할 수 있도록 합니다.

• MiniZinc 의 제약 모델
• PySAT 의 SAT 모델
• Z3 Python 의 SMT 공식

MCP Solver의 시스템 아키텍처와 이론적 기초에 대한 자세한 설명은 다음 연구 논문을 참조하세요: Stefan Szeider, "MCP-Solver: Integrating Language Models with Constraint Programming Systems" , arXiv:2501.00539, 2024.

사용 가능한 도구

다음 항목은 (MinZinc/Pysat/Z3) 코드의 일부를 의미하고, 모델은 인코딩을 의미합니다.

시스템 요구 사항

• 파이썬과 프로젝트 매니저 uv
• 파이썬 3.11+
• 모드별 요구 사항: MiniZinc, PySAT, Python Z3(필수 패키지는 pip를 통해 설치됨)
• 운영 체제: macOS, Windows, Linux(적절한 적응 포함)

설치

MCP Solver를 사용하려면 Python 3.11 이상, uv 패키지 관리자, 솔버별 종속성(MiniZinc, Z3 또는 PySAT)이 필요합니다.

Windows, macOS, Linux에 대한 자세한 설치 지침은 INSTALL.md를 참조하세요.

빠른 시작:

지엑스피1

사용 가능한 모드/백엔드 해결

MCP 솔버는 세 가지 고유한 운영 모드를 제공하며, 각 모드는 서로 다른 제약 조건 해결 백엔드와 통합됩니다. 각 모드는 특정 종속성을 필요로 하며, 다양한 유형의 문제를 해결하는 고유한 기능을 제공합니다.

미니징크 모드

MiniZinc 모드는 다음과 같은 기능을 통해 MiniZinc 제약 모델링 언어와의 통합을 제공합니다.

• 글로벌 제약 조건을 포함한 풍부한 제약 조건 표현식
• Chuffed 제약 조건 솔버와의 통합
• 최적화 기능
• get_solution 통해 솔루션 값에 액세스

종속성 : minizinc 패키지가 필요합니다( uv pip install -e ".[mzn]" )

구성 : MiniZinc 모드에서 실행하려면 다음을 사용하세요.

PySAT 모드

PySAT 모드에서는 다음 기능을 통해 Python SAT 솔빙 툴킷과 상호 작용할 수 있습니다.

• CNF(Conjunctive Normal Form)를 이용한 명제적 제약 모델링
• 다양한 SAT 솔버(Glucose3, Glucose4, Lingeling 등)에 접근 가능
• 기수 제약 조건(at_most_k, at_least_k, exact_k)
• 부울 제약 조건 해결 지원

종속성 : python-sat 패키지가 필요합니다( uv pip install -e ".[pysat]" )

구성 : PySAT 모드에서 실행하려면 다음을 사용하세요.

Z3 모드

Z3 모드는 다음 기능을 통해 Z3 SMT(Satisfiability Modulo Theories) 풀이 기능에 대한 액세스를 제공합니다.

• 풍부한 유형 시스템: 부울, 정수, 실수, 비트 벡터, 배열
• 양화사를 사용한 제약 조건 해결
• 최적화 기능
• 일반적인 모델링 패턴을 위한 템플릿 라이브러리

종속성 : z3-solver 패키지가 필요합니다( uv pip install -e ".[z3]" )

구성 : Z3 모드에서 실행하려면 다음을 사용하세요.

MCP 테스트 클라이언트

MCP 솔버에는 ReAct 에이전트 프레임워크를 기반으로 개발, 실험 및 진단을 위한 MCP 클라이언트가 포함되어 있습니다. 이 클라이언트는 LLM과 MCP 서버 간의 중개자 역할을 하며, 자연어 문제 진술을 정형 제약 조건 프로그래밍 솔루션으로 변환하는 과정을 용이하게 합니다.

설치

클라이언트는 LLM 제공업체의 API 키를 요구합니다. Anthropic(기본 LLM은 Claude Sonnet 3.7)의 경우 ANTHROPIC_API_KEY 환경 변수를 설정하세요. 이 변수는 사용자 환경에서 설정하거나 프로젝트 루트의 .env 파일에 포함할 수 있습니다.

용법

클라이언트는 각 솔버 백엔드에 대해 특수 명령을 제공합니다.

예시

예제 1: 주조 문제(MiniZinc)

이는 조지 존슨(George Johnson)의 사례에 근거합니다(NYT, 1999년 7월 13일).

사용자

연극 연출가가 자신의 순진한 배우 알바레즈나 조카인 배우 코헨을 작품에 캐스팅해야 한다고 느낀다고 가정해 보겠습니다. 하지만 알바레즈는 자신의 전 애인인 코헨 씨와 함께하는 연극에 출연하지 않고, 새로운 연인인 배우 데븐포트도 캐스팅해야 한다고 요구합니다. 자신의 호의에 보답해야 할 제작자는 배우 브라니슬랍스키에게 배역을 맡기겠다고 고집합니다. 하지만 브라니슬랍스키 씨는 알바레즈나 데븐포트 씨와 함께하는 어떤 연극에도 출연하지 않을 것입니다. 연출가는 그 연극을 캐스팅할 수 있을까요?

시스템: clear_model

Model cleared

시스템: add_item (다중)

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;

시스템: solve_model

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

해결책(코헨과 브라니슬랍스키는 출연시키지만 알바레즈와 데븐포트는 출연시키지 않음)은 모든 제약 조건을 충족합니다.

예제 2: N-퀸 문제(MiniZinc)

사용자

nxn 체스판에 n개의 퀸을 놓을 수 있는지 확인해 보세요. n=10, 20, 30, 40으로 놓고 풀이 시간을 비교해 보세요.

시스템: clear_model

Model cleared

시스템: add_item (다중)

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;

시스템: solve_model (n 값을 변경하여 n=10, 20, 30, 40)

시간 비교를 풀어보세요: n=10: 0.001sn=20: 0.005sn=30: 0.040sn=40: 0.043s

테스트된 모든 보드 크기에 대한 솔루션이 존재합니다. 시간 복잡도는 비선형적으로 증가하지만 n=40까지는 관리 가능한 수준입니다.

예제 3: 순회 판매원 문제(MiniZinc)

사용자

비엔나에 거주하는 한 판매원이 오스트리아 각 주의 주도를 한 번씩 방문하는 다가오는 여행을 계획해야 합니다. 최단 경로를 찾는 데 도움을 주세요. 거리(km): 1=비엔나, 2=장크트푈텐, 3=아이젠슈타트, 4=린츠, 5=그라츠, 6=클라겐푸르트, 7=잘츠부르크, 8=인스브루크, 9=브레겐츠

[사용자 메시지에 제공된 거리 행렬 표]

시스템: add_item (다중)

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;

시스템: solve_model

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

최적의 경로: 비엔나 → 장크트 푈텐 → 린츠 → 잘츠부르크 → 브레겐츠 → 인스부르크 → 클라겐푸르트 → 그라츠 → 아이젠슈타트 → 비엔나, 총 거리 1,564km.

피드백

이 양식을 통해 작성자에게 피드백을 제공할 수 있습니다.

부인 성명

이 MCP 솔버는 프로토타입 단계이므로 주의해서 사용해야 합니다. 사용자는 자유롭게 실험해 볼 수 있지만, 중요한 환경에서 사용하는 경우 모든 위험은 사용자에게 있습니다.

특허

이 프로젝트는 MIT 라이선스에 따라 라이선스가 부여되었습니다. 자세한 내용은 라이선스 파일을 참조하세요.