╭─╮╭┬╮╶┬╴   ╭─╮╷ ╷╶┬╮╭─╮╷╭ ╷ ╷
╰─╮│││ │    ╰─╮│ │ │││ │├┴╮│ │
╰─╯╵ ╵ ╵    ╰─╯╰─╯╶┴╯╰─╯╵ ╵╰─╯

smt-sudoku-mcp

이제 에이전트가 스도쿠를 자신 있게 플레이할 수 있습니다!

Z3를 사용하여 고전적인 제약 충족 퍼즐인 스도쿠를 통해 만족성 모듈로 이론(SMT) 해결의 힘을 보여주는 MCP 서버입니다.

스도쿠는 SMT 기본 요소에 깔끔하게 매핑됩니다. 퍼즐 생성은 스도쿠 제약 조건을 충족하는 모델을 찾은 다음 축소된 단서 집합이 여전히 유일한 해를 가짐을 증명하는 것을 의미하고, 그리드 검증은 주어진 셀 값에 대해 동일한 제약 조건을 확인하는 것을 의미하며, 퍼즐 해결은 모델을 찾거나 존재하지 않음을 증명하는 것을 의미합니다.

도구

네 가지 도구 모두 상태 비저장입니다. 모든 호출은 완전한 그리드를 명시적으로 받거나 반환하며, 서버 측 세션 상태가 없습니다.

스도쿠 그리드는 {"rows": [[...9 ints...], ...9 rows...]}로 표현되며, 각 셀은 주어진 숫자에 대해 1-9 또는 빈 셀에 대해 0입니다. 특정 셀(충돌)을 지칭하는 모든 도구 결과는 row/col을 1부터 시작하는 인덱스로 보고하며, 이는 스도쿠 셀이 텍스트에서 일반적으로 설명되는 방식(1행 1열이 왼쪽 위 셀)과 일치합니다.

generate_sudoku_puzzle

새롭고 유일하게 풀 수 있는 스도쿠 퍼즐을 생성합니다.

• 입력: difficulty — "easy", "medium", "hard" 중 하나(기본값 "medium"), 대략적인 목표 단서 수에 매핑됩니다.

• 출력: {"puzzle": <grid>, "difficulty": <str>, "givens": <int>} — givens는 실제로 채워진 셀 수이며, 추가로 셀을 제거하면 유일성이 깨질 경우 목표보다 약간 높을 수 있습니다.

validate_partial_sudoku_solution

부분적으로 채워진 그리드에 충돌이 없는지, 그리고 충돌이 없다면 여전히 완성할 수 있는지 확인합니다.

• 입력: grid — 부분 그리드(빈 셀은 0).

• 출력: {"has_conflicts": <bool>, "conflicts": [<cell>, ...], "is_completable": <bool | null>} — is_completable은 충돌이 있을 때 null입니다. 충돌이 해결되기 전에는 완성 가능성이 의미 있는 질문이 아니기 때문입니다.

validate_full_sudoku_solution

완전히 채워진 그리드가 올바른 스도쿠 해인지 확인합니다.

• 입력: grid — 빈 셀이 없어야 합니다.

• 출력: {"is_valid": <bool>, "has_empty_cells": <bool>, "conflicts": [<cell>, ...]}.

solve_sudoku_puzzle

풀리지 않은 그리드를 풀거나, 풀 수 없는 이유를 보고합니다.

• 입력: grid — 풀 부분 그리드(빈 셀은 0).

• 출력: {"status": "satisfiable" | "conflicting_givens" | "unsatisfiable", "solution": <grid | null>, "conflicts": [<cell>, ...]}. conflicts는 status가 "conflicting_givens"일 때만 채워집니다(두 개의 주어진 셀이 행/열/박스 규칙을 직접 위반하는 경우). "unsatisfiable"은 주어진 값들이 쌍별로 충돌이 없지만 완성이 존재하지 않음을 의미합니다.

Related MCP server: Gurddy MCP Server

설치

Python 3.13+가 필요합니다. 패키지는 PyPI에 게시되어 있습니다.

가장 간단한 실행 방법은 uvx를 사용하는 것입니다. 이는 첫 사용 시 패키지를 임시 환경으로 가져오며 별도의 설치 단계가 필요하지 않습니다:

uvx smt-sudoku-mcp

또는 pip(또는 uv pip)로 설치하고 설치된 콘솔 스크립트를 직접 실행할 수 있습니다:

pip install smt-sudoku-mcp
smt-sudoku-mcp

게시된 패키지 대신 소스 자체를 작업하려면 아래의 개발을 참조하세요.

MCP 클라이언트와 함께 사용하기

이 서버는 기본적으로 stdio를 통해 MCP를 사용하므로 하위 프로세스를 시작할 수 있는 모든 MCP 클라이언트는 추가 설정 없이 사용할 수 있습니다. 클라이언트가 독립형 HTTP 서비스에 연결해야 하는 경우 SMT_SUDOKU_MCP_TRANSPORT=streamable-http로 설정하세요. 구성을 참조하세요.

Claude Code

claude mcp add smt-sudoku -- uvx smt-sudoku-mcp

Claude Desktop

설정 → 개발자 → 구성 편집(claude_desktop_config.json)에서 항목을 추가하세요:

{
  "mcpServers": {
    "smt-sudoku": {
      "command": "uvx",
      "args": ["smt-sudoku-mcp"]
    }
  }
}

기타 MCP 클라이언트 및 에이전트 프레임워크

원시 MCP 서버 정의를 허용하는 모든 클라이언트(Cursor, Windsurf, VS Code 또는 MCP SDK 기반의 사용자 지정 에이전트)는 동일한 command/args 쌍(uvx 및 ["smt-sudoku-mcp"])을 사용할 수 있습니다. streamable-http의 경우 SMT_SUDOKU_MCP_TRANSPORT=streamable-http uvx smt-sudoku-mcp로 서버를 별도로 실행하고 클라이언트를 시작할 명령을 제공하는 대신 http://<host>:<port>/mcp를 가리키게 하세요.

연결되면 에이전트는 다른 도구와 마찬가지로 위의 네 가지 도구를 호출할 수 있습니다. 예를 들어 에이전트에게 "어려운 스도쿠 퍼즐을 생성한 다음 풀고 해를 확인하세요"라고 요청하면 추가 지침 없이 generate_sudoku_puzzle, solve_sudoku_puzzle, validate_full_sudoku_solution을 연결합니다. 각 도구의 설명과 스키마가 에이전트가 시퀀스 자체를 계획하기에 충분하기 때문입니다.

구성

환경 변수, 모두 선택 사항:

개발

게시된 패키지 대신 소스 체크아웃에서 서버를 실행하려면 uv를 사용하세요:

uv sync
uv run smt-sudoku-mcp

아키텍처 노트와 전체 개발 명령어(just -l)는 AGENTS.md를 참조하세요.

기여

이슈와 풀 리퀘스트를 환영합니다.

라이선스

MIT.