mcp-z3-prover

mcp-z3-prover

Z3 ソルバー API を公開する MCP サーバー

インストール

pip install mcp-z3-prover

使用方法

from mcp_z3_prover import mcp

# Run the server
mcp.run()

または、コマンドラインから実行します。

mcp-z3-prover

MCP ツール

サーバーは以下のツールを公開します。

• create_bool_var - ブール変数を作成します
• create_int_var - 整数変数を作成します
• create_real_var - 実数変数を作成します
• create_int_constant - 整数定数を作成します
• create_real_constant - 実数定数を作成します
• add_constraint - ソルバーに制約を追加します
• solve - 現在の問題を解きます
• get_model_value - モデルから変数の値を取得します
• optimize - 最適化の目的関数を指定して解きます
• reset_solver - ソルバーの状態をリセットします
• list_variables - 作成済みのすべての変数を一覧表示します

例

# Create variables
create_int_var("x")
create_int_var("y")

# Add constraints
add_constraint("int:x + int:y == 10")
add_constraint("int:x > 0")
add_constraint("int:y > 0")

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}

# Get specific values
x_val = get_model_value("int:x")

整数の素因数分解の例

# Factor n = 4295229443 where n = p * q with q <= sqrt(n)
create_int_var("p")
create_int_var("q")

# Add constraints
add_constraint("int:p * int:q == 4295229443")
add_constraint("4295229443 > int:p")
add_constraint("4295229443 > int:q")
add_constraint("int:q <= 65537")  # sqrt(4295229443) ≈ 65537
add_constraint("int:q > 1")
add_constraint("int:p > 1")
add_constraint("int:q % 2 != 0")  # q is odd
add_constraint("int:p % 2 != 0")  # p is odd

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}
# Verification: 65537 * 65539 = 4295229443

開発

git clone https://github.com/daedalus/mcp-z3-prover.git
cd mcp-z3-prover
pip install -e ".[test]"

# run tests
pytest

# format
ruff format src/ tests/

# lint
ruff check src/ tests/

# type check
mypy src/

MCP 登録

mcp-name: io.github.daedalus/mcp-z3-prover