### MCP Solver Quick Start Example

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

A complete example demonstrating the setup and solving of a MaxSAT problem using the MCP Solver, covering variable definition, constraints, and solution export.

```python
# Item 0: Imports and initialization
from pysat.formula import WCNF
from pysat.examples.rc2 import RC2
# Note: Helper functions (exactly_k, at_most_k, etc.) are already available

wcnf = WCNF()

# Item 1: Variables
# Problem: Select items to maximize value
# Variables: 1=itemA, 2=itemB, 3=itemC
itemA = 1
itemB = 2  
itemC = 3

# Item 2: Hard constraints
# Hard constraint: Can't select both A and B
wcnf.append([-itemA, -itemB])

# Item 3: Soft constraints
# Soft constraints: We want to MAXIMIZE total value
# Remember: MaxSAT MINIMIZES penalties, so we penalize NOT selecting valuable items

wcnf.append([itemA], weight=5)   # Lose 5 points if itemA=FALSE (not selected)
wcnf.append([itemB], weight=3)   # Lose 3 points if itemB=FALSE (not selected)  
wcnf.append([itemC], weight=2)   # Lose 2 points if itemC=FALSE (not selected)

# MaxSAT will select items to minimize penalties → maximizes value!

# Item 4: Solve and export
```

--------------------------------

### Install Additional Solvers

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Installs the z3-solver and python-sat libraries using uv.

```bash
uv pip install "z3-solver>=4.12.1"
uv pip install python-sat
```

--------------------------------

### Quick Start Example: SAT Solving

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

A complete example demonstrating how to define a CNF formula, add clauses, solve it using Glucose3, interpret the model, and export the solution. It also shows proper memory management by calling `solver.delete()`.

```python
from pysat.formula import CNF
from pysat.solvers import Glucose3
from pysat.card import *  # Import cardinality helpers

# Simple problem: Find values for A, B, C such that: 
# (A OR B) AND (NOT A OR C) AND (NOT B OR NOT C)

formula = CNF()

# Define variables: 1=A, 2=B, 3=C
A, B, C = 1, 2, 3

# Add clauses
formula.append([A, B])        # A OR B
formula.append([-A, C])       # NOT A OR C
formula.append([-B, -C])      # NOT B OR NOT C

# Create solver and add formula
solver = Glucose3()
solver.append_formula(formula)

# Solve and process results
if solver.solve():
    model = solver.get_model()
    
    # Interpret model (positive numbers are True, negative are False)
    solution = {
        "A": A in model,
        "B": B in model,
        "C": C in model
    }
    
    export_solution({
        "satisfiable": True,
        "assignment": solution
    })
else:
    export_solution({
        "satisfiable": False,
        "message": "No solution exists"
    })

# Free solver memory
solver.delete()
```

--------------------------------

### Problem Parameter Verification Example

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Provides an example of how to verify problem parameters by adding comments and checking the encoding against the original problem statement.

```python
# Problem parameters (DO NOT CHANGE):
# - Number of items: 10
# - Must select: exactly 3  
# - Budget limit: 50

# Verify encoding matches:
items = list(range(10))  # ✓ 10 items [0,1,2,3,4,5,6,7,8,9]
required_selections = 3   # ✓ Exactly 3 items
budget = 50              # ✓ Budget limit 50
```

--------------------------------

### Install MCP Solver Dependencies

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Installs the MCP Solver and its dependencies in editable mode using uv.

```bash
uv pip install -e ."[all]"
```

--------------------------------

### Example Using Cardinality Constraints with Parameter Verification

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

A comprehensive example demonstrating the use of cardinality constraints, parameter verification, and variable mapping within the MCP Solver.

```python
from pysat.formula import CNF
from pysat.solvers import Glucose3
from pysat.card import *

# PARAMETER VERIFICATION - Track problem requirements
# Problem parameters (example):
# - Total items: 4
# - Must select: exactly 2
# - Constraint: if first item selected, at most 1 of the others

# Verify we're using correct parameters
total_items = 4
required_selections = 2

formula = CNF()

# Create variables with meaningful names
items = list(range(1, total_items + 1))  # [1, 2, 3, 4]
assert len(items) == total_items, f"Expected {total_items} items"

a, b, c, d = items
var_names = {1: "a", 2: "b", 3: "c", 4: "d"}

# Add cardinality constraints using verified parameters
# Exactly 'required_selections' items must be selected
for clause in exactly_k(items, required_selections):  # Using verified parameter
    formula.append(clause)
    
# Additional constraint from problem
# (Example constraint logic here)
    
# Combining constraints - If 'a' is true, then at most one of b,c,d can be true
formula.append([-a, b, c, d])  # If a is true, at least one of b,c,d must be true
for clause in at_most_one([b, c, d]):
    formula.append(clause)

# Solve
solver = Glucose3()
solver.append_formula(formula)
if solver.solve():
    model = solver.get_model()
    solution = {var_names[abs(v)]: (v > 0) for v in model if abs(v) in var_names}
    
    export_solution({
        "satisfiable": True,
        "assignment": solution
    })
else:
    export_solution({
        "satisfiable": False,
        "message": "No solution exists"
    })

solver.delete()
```

--------------------------------

### Install pipx and uv on Windows

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Installs pipx and uv on Windows using pipx, with instructions to add to PATH if necessary.

```powershell
python -m pip install --user pipx
python -m pipx ensurepath
pipx install uv

# Add to PATH if needed:
# %USERPROFILE%\AppData\Roaming\Python\Python313\Scripts
```

--------------------------------

### Test MCP Solver Client Setup

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Execute this command to test the client setup for the MCP Solver.

```bash
uv run test-setup-client
```

--------------------------------

### Install pipx and uv on Linux

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Installs pipx on Linux via APT and uv via pipx, ensuring uv is in the PATH.

```bash
sudo apt install pipx
pipx ensurepath
pipx install uv

# Ensure ~/.local/bin is in your PATH
```

--------------------------------

### Configure MiniZinc on Linux

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Instructions for installing MiniZinc on Linux, including adding it to the PATH.

```env
PATH=/opt/minizinc:$PATH
```

--------------------------------

### Feature Selection Example: Maximize Value

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Example demonstrating how to maximize the total value of selected features by penalizing their deselection.

```python
# Problem: Maximize total value of selected features
# Feature A has value 10
wcnf.append([featureA], weight=10)  # Lose 10 points if A not selected
```

--------------------------------

### Feature Selection Example: Minimize Cost

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Example demonstrating how to minimize the total cost of selected items by penalizing their selection.

```python
# Problem: Minimize total cost of selected items  
# Item B has cost 5
wcnf.append([-itemB], weight=5)  # Pay 5 points if B is selected
```

--------------------------------

### MCP Solver API Documentation

Source: https://github.com/szeider/mcp-solver/blob/main/src/mcp_solver/core/instructions.md

Documentation for the MCP Solver tools, including their inputs, outputs, and usage guidelines.

```APIDOC
clear_model:
  Description: Clears the current MiniZinc model.
  Input: No arguments.
  Output: Confirmation message.

add_item:
  Description: Adds a MiniZinc statement to the model.
  Input:
    - index (integer): The position to insert the statement.
    - content (string): The MiniZinc statement.
  Output:
    - Confirmation message and the current (truncated) model.

replace_item:
  Description: Replaces an existing MiniZinc statement in the model.
  Input:
    - index (integer): The index of the item to replace.
    - content (string): The new MiniZinc statement.
  Output:
    - Confirmation message and the updated (truncated) model.

delete_item:
  Description: Deletes a MiniZinc statement from the model.
  Input:
    - index (integer): The index of the item to delete.
  Output:
    - Confirmation message and the updated (truncated) model.

solve_model:
  Description: Solves the current MiniZinc model.
  Input:
    - timeout (number): Time in seconds for solving (1-30).
  Output:
    - JSON object with status ('SAT', 'UNSAT', 'TIMEOUT') and optionally a 'solution' object if satisfiable.
```

--------------------------------

### Pre-Implemented Constraint Helpers (No Import)

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Provides examples of constraint helper functions that are automatically available without needing explicit imports.

```python
# NO IMPORT NEEDED - these are available by default
at_most_one([1, 2, 3])        # At most one variable is true
exactly_one([1, 2, 3])        # Exactly one variable is true
implies(1, 2)                 # If var1 is true, then var2 must be true
mutually_exclusive([1, 2, 3]) # Variables are mutually exclusive
if_then_else(1, 2, 3)         # If var1 then var2 else var3
```

--------------------------------

### Run Verification Tests

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Executes various verification tests for the MCP Solver setup using uv.

```bash
uv run test-setup-mzn
uv run test-setup-z3
uv run test-setup-pysat
uv run test-setup-maxsat
uv run test-setup-client
```

--------------------------------

### Install Python on Windows

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Installs Python 3.13 on Windows using winget and verifies the installation.

```powershell
winget install --id Python.Python.3.13

python --version
pip --version
```

--------------------------------

### Parameter Validation Example

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Demonstrates how to validate parameters before solving a problem, ensuring the correct number of colors is used.

```python
# Problem: "Find a coloring with 9 colors"
# CORRECT:
colors = list(range(9))  # [0, 1, 2, 3, 4, 5, 6, 7, 8] - exactly 9 colors
print(f"Using {len(colors)} colors: {colors}")  # Verify before solving

# INCORRECT:
# colors = list(range(10))  # This gives 10 colors!
```

--------------------------------

### Install MCP Test Client

Source: https://github.com/szeider/mcp-solver/blob/main/README.md

Installs the MCP client dependencies and verifies its setup using uv pip and uv run.

```bash
uv pip install -e ".[client]"

uv run test-setup-client
```

--------------------------------

### Install pipx and uv on macOS

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Installs pipx and uv on macOS using Homebrew, ensuring pipx is in the PATH.

```bash
brew install pipx
pipx ensurepath
pipx install uv
```

--------------------------------

### Clone MCP Solver Project

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Clones the MCP Solver repository from GitHub to a specified directory.

```bash
mkdir -p ~/projects/mcp-solver
cd ~/projects/mcp-solver
git clone --branch z3 https://github.com/szeider/mcp-solver.git .
```

--------------------------------

### Claude Desktop Linux Installation and Launch

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Steps to install and launch Claude Desktop on Linux using a community wrapper, including setting Chrome as the default browser and running without a sandbox.

```bash
git clone https://github.com/aaddrick/claude-desktop-debian.git
cd claude-desktop-debian
sudo ./build-deb.sh
sudo dpkg -i /path/to/claude-desktop_0.9.0_amd64.deb

# optionally
xdg-settings set default-web-browser google-chrome.desktop # optionally
/usr/bin/claude-desktop --no-sandbox
```

--------------------------------

### Problem Specification Examples (Python)

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Demonstrates how to correctly interpret problem specifications for counts and ranges in Python, ensuring the exact numbers required by the problem are used.

```python
# Problem asks for 9 colors
colors = list(range(9))  # CORRECT: Exactly 9 colors [0-8]

# Problem asks for 6 queens  
for clause in exactly_k(queen_vars, 6):  # CORRECT: Exactly 6
```

```python
# For N colors:
colors = list(range(N))        # [0, 1, 2, ..., N-1]

# For grid positions:
positions = [(i,j) for i in range(rows) for j in range(cols)]

# For counting items:
assert len(selected_items) == required_count
```

```python
# Verify counts match problem specification
assert len(colors) == required_colors, f"Wrong number of colors"
assert num_pieces == required_pieces, f"Wrong number of pieces"
```

--------------------------------

### Available Imports

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Lists the essential PySAT modules and standard Python modules required for using the solver and its functionalities.

```python
# Core PySAT modules
from pysat.formula import CNF
from pysat.solvers import Glucose3, Cadical153

# Standard Python modules
import math  
import random
import collections
import itertools
import re
import json

# Helper functions (must be explicitly imported)
from pysat.card import *
```

--------------------------------

### Configure MiniZinc on macOS

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Instructions for installing MiniZinc on macOS, including adding it to the PATH.

```env
PATH=/Applications/MiniZincIDE.app/Contents/Resources:$PATH
```

--------------------------------

### Problem Parameter Verification Example

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Illustrates how to correctly extract, comment, and verify numeric parameters from a problem statement to ensure the SAT encoding matches the requirements precisely. Includes assertions for validation.

```python
# Problem parameters (DO NOT CHANGE):
# - Number of colors: 9
# - Number of queens: 6  
# - Number of knights: 5
# - Grid size: 6x6

# Verify encoding matches:
colors = list(range(9))  # ✓ 9 colors [0,1,2,3,4,5,6,7,8]
num_queens = 6          # ✓ Exactly 6 queens
num_knights = 5         # ✓ Exactly 5 knights

# Verification: Using exactly the required parameters
assert len(colors) == 9, f"Expected 9 colors, using {len(colors)}"
```

--------------------------------

### LLM Provider Configuration

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Demonstrates the syntax for configuring different LLM providers and local models, including parameters.

```APIDOC
LLM Model Configuration:

Syntax:
  XY:model                     # For cloud providers
  LM:model@url                 # For local models via LM Studio (basic)
  LM:model(param=value)@url    # For local models with parameters

Parameters for Local Models:
  format=json                  # Request JSON output
  temp=0.7                     # Set temperature to 0.7
  max_tokens=1000              # Set maximum tokens to 1000

Provider Codes (XY):
  OA: OpenAI
  AT: Anthropic
  OR: OpenRouter
  GO: Google (Gemini)
  LM: LM Studio (local models)

Examples:
  OA:gpt-4.1-2025-04-14
  AT:claude-3-7-sonnet-20250219
  OR:google/gemini-2.5-pro-preview
  LM:model(format=json,temp=0.7)@http://localhost:1234
```

--------------------------------

### MCP Solver Feature Selection Example: Imports and Initialization

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Sets up the necessary imports from the pysat library and initializes the WCNF object for the feature selection problem.

```python
from pysat.formula import WCNF
from pysat.examples.rc2 import RC2
# Note: Helper functions are already available

wcnf = WCNF()
```

--------------------------------

### Detecting Conflicting Constraints (UNSAT Example)

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Provides an example of an unsatisfiable problem scenario (scheduling more items than available slots) and how to report it using `export_solution`, including a message about the conflict.

```python
# Problem: Schedule 3 items in 2 slots, each slot holds at most 1 item
# This is UNSATISFIABLE (3 items can't fit in 2 single-item slots)

# After adding constraints and solving:
with RC2(wcnf) as solver:
    if not solver.compute():
        export_solution({
            "satisfiable": False,
            "message": "Cannot fit 3 items in 2 slots with capacity 1 each",
            "conflict": "3 items require 3 slots, but only 2 available"
        })
```

--------------------------------

### MCP Solver API Documentation

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Documentation for the MCP Solver's available tools and their functionalities, including model manipulation and solving.

```apidoc
Tool: clear_model
Description: Reset the PySAT model
```

```apidoc
Tool: add_item
Description: Add Python code to the model
```

```apidoc
Tool: replace_item
Description: Replace code in the model
```

```apidoc
Tool: delete_item
Description: Delete code from the model
```

```apidoc
Tool: solve_model
Description: Solve the current model (requires timeout parameter between 1-30 seconds)
Notes: If your model times out, you'll receive a response with "status": "timeout" and "timeout": true, but the connection will be maintained so you can modify and retry your model.
```

```apidoc
Tool: get_model
Description: Fetch the current content of the PySAT model
```

--------------------------------

### Integrating with Constraint Helpers

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Provides examples of integrating custom constraint logic, such as ensuring exactly one color per node or implementing logical implications using SAT clauses.

```python
# Ensure exactly one color per node
node_colors = [create_var(f"{node}_{color}") for color in colors]
for clause in exactly_one(node_colors):
    formula.append(clause)

# Example: "if user selected feature A AND feature B, then feature C must be enabled"
a_id = create_var("feature_A")
b_id = create_var("feature_B") 
c_id = create_var("feature_C")

# A ∧ B → C is equivalent to ¬A ∨ ¬B ∨ C
formula.append([-a_id, -b_id, c_id])
```

--------------------------------

### Variable Mapping Helper - Basic Usage

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Demonstrates the basic usage of the VariableMap helper for creating and managing variables with meaningful names.

```python
# Create a variable map for managing variables
var_map = VariableMap()

# Create variables with meaningful names
x1 = var_map.create_var("x1")
x2 = var_map.create_var("x2")

# Create multiple variables at once
features = var_map.create_vars(["premium", "basic", "cloud"])

# After solving, get a readable solution
if solver.solve():
    model = solver.get_model()
    solution = var_map.interpret_model(model)
    # solution = {"x1": True, "x2": False, "premium": True, ...}
```

--------------------------------

### Incorrect Solver Mocking Examples

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Illustrates common mistakes to avoid when working with the MaxSAT solver, such as creating fake solver objects or attempting to mock the optimization process. Emphasizes using the provided RC2 solver directly.

```python
# NEVER DO THIS - The environment has real RC2!
import types
solver = types.SimpleNamespace()
solver.compute = lambda: [1, 2, 3]  # compute() returns the model directly

# NEVER DO THIS - Use actual RC2!
def fake_optimize(wcnf):
    # Manual "optimization" logic
    return some_solution

# NEVER DO THIS
print("MaxSAT not available, using heuristic instead")
```

--------------------------------

### Create and Activate Virtual Environment (macOS/Linux)

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Creates a Python virtual environment and activates it for use on macOS and Linux.

```bash
python3 -m venv .venv
source .venv/bin/activate
```

--------------------------------

### Set Other LLM Provider API Keys

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Shows how to set API keys for other LLM providers in a .env file.

```env
OPENAI_API_KEY=sk-...
GOOGLE_API_KEY=...
OPENROUTER_API_KEY=sk-...
```

--------------------------------

### Variable Mapping for Readability - VariableMap Class

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Illustrates using the recommended VariableMap class for managing variables and creating them with descriptive names.

```python
# Create a variable map for managing variables
var_map = VariableMap()

# Create variables with meaningful names
x1 = var_map.create_var("x1")
edge_ab = var_map.create_var("edge_a_b")

# Create variables for all nodes
node_vars = var_map.create_vars(["node1", "node2", "node3"])
```

--------------------------------

### Bitvector Verification Example with Z3

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/z3/instructions.md

A modular example demonstrating the use of bitvectors and arrays in Z3 for verification, including setup, model building, execution, and result export.

```python
# Item 1: Setup and imports
from z3 import *
from mcp_solver.z3 import export_solution

# Item 2: Define the bitvector verification model
def build_verification_model():
    # Create an 8-bit input X
    X = BitVec('X', 8)
    
    # Create a lookup table (array indexed by 3-bit values)
    table = Array('table', BitVecSort(3), BitVecSort(8))
    
    # Step 1: Extract the lower 3 bits of X as the index
    index = Extract(2, 0, X)
    
    # Step 2: Look up a value Y from the table
    Y = Select(table, index)
    
    # Step 3: Compute Z = (X XOR Y) & 1
    Z = Extract(0, 0, X ^ Y)
    
    # Calculate the parity of X (XOR of all bits)
    parity = BitVecVal(0, 1)
    for i in range(8):
        parity = parity ^ Extract(i, i, X)
    
    # Check if property holds: Z == parity(X)
    property_holds = (Z == parity)
    
    # Create solver and look for counterexamples
    s = Solver()
    s.add(Not(property_holds))
    
    return s, X, Y, Z, parity, index

# Item 3: Execute the verification
# Build and get our verification model components
solver, X, Y, Z, parity, index = build_verification_model()

# Check if a counterexample exists (property violation)
result = solver.check()

# Item 4: Process results and export the solution
# Create Z3 boolean for the verification result
property_verified = Bool('property_verified')

if result == sat:
    # Found a counterexample - the solver successfully found a case where the property fails
    # This means the counterexample search was satisfiable (but the property is false)
    print("Property verification failed. Counterexample found.")
    # Export with solver result (sat) and the property_verified value (false)
    solver.add(property_verified == False)
    export_solution(solver=solver, variables={"property_verified": property_verified})
else:
    # No counterexample found - the property holds for all inputs
    # The counterexample search was unsatisfiable (meaning the property is true)
    print("Property verified: Z always equals parity of X")
    # Create a new solver to express that the property is verified
    result_solver = Solver()
    result_solver.add(property_verified == True)
    export_solution(solver=result_solver, variables={"property_verified": property_verified})
```

--------------------------------

### Create and Activate Virtual Environment (Windows)

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Creates a Python virtual environment and activates it for use on Windows PowerShell.

```powershell
Set-ExecutionPolicy -Scope CurrentUser -ExecutionPolicy RemoteSigned
python -m venv .venv
.\.venv\Scripts\Activate.ps1
```

--------------------------------

### Claude Desktop Configuration for MCP Solver (Windows)

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Configuration JSON for Claude Desktop on Windows to connect to the MCP Solver, specifying the command and arguments.

```json
{
  "mcpServers": {
    "MCP Solver": {
      "command": "cmd.exe",
      "args": [
        "/C",
        "cd C:\\Users\\AC Admin\\build\\mcp-solver && uv run mcp-solver-mzn"
      ]
    }
  }
}
```

--------------------------------

### Nurse Scheduling: Imports and Initialization

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Initializes the WCNF object and imports necessary components from the pysat library for the nurse scheduling problem.

```python
from pysat.formula import WCNF
from pysat.examples.rc2 import RC2
# Note: Helper functions are already available

wcnf = WCNF()
```

--------------------------------

### Claude Desktop Configuration for MCP Solver (Linux)

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Configuration JSON for Claude Desktop on Linux to connect to the MCP Solver, specifying the command and arguments.

```json
{
  "mcpServers": {
    "MCP Solver": {
      "command": "/bin/bash",
      "args": [
        "-c",
        "cd /path/to/mcp-solver && uv run mcp-solver-mzn"
      ]
    }
  }
}
```

--------------------------------

### Install Python on macOS

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Installs Python 3.13+ on macOS using Homebrew and verifies the installation.

```bash
brew install python

python3 --version
```

--------------------------------

### Final Notes and Best Practices

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Offers final recommendations including reviewing return information, splitting long code parts, verifying solutions, and consistently using actual PySAT solvers.

```python
- **Review Return Information:**  
  Carefully review the confirmation messages and the current model after each tool call.
- **Split long code parts** into smaller items.
- **Verification:**  
  Always verify the solution after a solve operation by checking that all constraints are satisfied and justified.
- **Always use actual PySAT solvers** - never create mock objects or try manual solutions.
```

--------------------------------

### Run MCP Solver Client with Queries

Source: https://github.com/szeider/mcp-solver/blob/main/INSTALL.md

Commands to run the MCP Solver client with a query file, supporting different modes like MiniZinc, PySAT, MaxSAT, and Z3.

```bash
# MiniZinc mode
uv run test-client --query <query_file>.md

# PySAT mode
uv run test-client-pysat --query <query_file>.md

# MaxSAT mode
uv run test-client-maxsat --query <query_file>.md

# Z3 mode
uv run test-client-z3 --query <query_file>.md
```

--------------------------------

### Creating and Using Variables

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Illustrates the process of creating variables with meaningful names using a helper function and managing a global variable count for unique IDs.

```python
# Create a variable mapping dictionary
var_mapping = {}
var_count = 1

# Create variables with meaningful names
def create_var(name):
    global var_count  # Use global for module-level variables
    var_mapping[name] = var_count
    var_count += 1
    return var_mapping[name]

# Create variables
x1 = create_var("x1")
edge_ab = create_var("edge_a_b")

# Lookup variable names
def get_var_name(var_id):
    for name, vid in var_mapping.items():
        if vid == abs(var_id):
            return name
    return f"unknown_{var_id}"

# Interpret model into a dictionary of {name: boolean_value}
def interpret_model(model):
    return {get_var_name(v): (v > 0) for v in model}
```

--------------------------------

### Solve and Process Results with Glucose3

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Demonstrates how to initialize a Glucose3 solver, append a formula, solve it, retrieve the model, and export the solution. It also shows how to free solver memory.

```python
solver = Glucose3()
solver.append_formula(formula)

if solver.solve():
    model = solver.get_model()
    solution = {name: (vid in model) for name, vid in var_mapping.items()}
    
    export_solution({
        "satisfiable": True,
        "assignment": solution
    })
else:
    export_solution({
        "satisfiable": False,
        "message": "No solution exists"
    })
    
solver.delete()
```

--------------------------------

### MCP Solver Feature Selection Example: Variable Definitions

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Defines the variables representing features and their associated values, used for setting up soft constraints in the MaxSAT problem.

```python
# PARAMETER VERIFICATION
# Problem parameters (DO NOT CHANGE):
# - Number of features: 6
# - Feature values: cloud=10, ai=8, security=6, mobile=7, analytics=9, integration=5

# Variables: 1=cloud, 2=ai, 3=security, 4=mobile, 5=analytics, 6=integration
cloud = 1
ai = 2
security = 3
mobile = 4
analytics = 5
integration = 6

# Feature values for soft constraints
values = {
    cloud: 10,
    ai: 8,
    security: 6,
    mobile: 7,
    analytics: 9,
    integration: 5
}
```

--------------------------------

### Graph Coloring Problem Example

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Provides a complete example of solving the graph coloring problem using PySAT. It includes defining the graph, setting up variables, creating the CNF formula with constraints (each node has one color, adjacent nodes have different colors), solving, and interpreting the results.

```python
from pysat.formula import CNF
from pysat.solvers import Glucose3
from pysat.card import *

# Define a simple graph (adjacency list)
graph = {
    'A': ['B', 'C', 'D'],
    'B': ['A', 'C', 'E'],
    'C': ['A', 'B', 'D'],
    'D': ['A', 'C', 'E'],
    'E': ['B', 'D']
}
colors = ['Red', 'Green', 'Blue']

# Create variable mapping
var_mapping = {}
var_count = 1

def create_var(name):
    global var_count  # Use global for module-level variables
    var_mapping[name] = var_count
    var_count += 1
    return var_mapping[name]

# Create variables for node-color pairs
node_colors = {}
for node in graph:
    for color in colors:
        node_colors[(node, color)] = create_var(f"{node}_{color}")

# Create CNF formula
formula = CNF()

# Each node must have exactly one color
for node in graph:
    node_color_vars = [node_colors[(node, color)] for color in colors]
    for clause in exactly_one(node_color_vars):
        formula.append(clause)

# Adjacent nodes cannot have the same color
for node in graph:
    for neighbor in graph[node]:
        if neighbor > node:  # Avoid duplicate constraints
            for color in colors:
                formula.append([-node_colors[(node, color)], -node_colors[(neighbor, color)]])

# Create solver and add formula
solver = Glucose3()
solver.append_formula(formula)

# Solve and interpret results
if solver.solve():
    model = solver.get_model()
    
    # Create dict of node colors
    coloring = {}
    for (node, color), var_id in node_colors.items():
        if var_id in model:  # If this node-color assignment is true
            coloring[node] = color
    
    export_solution({
        "satisfiable": True,
        "coloring": coloring,
        "variable_mapping": var_mapping
    })
else:
    export_solution({
        "satisfiable": False,
        "message": "No valid coloring exists"
    })

solver.delete()
```

--------------------------------

### MCP Solver Feature Selection Example: Soft Constraints

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Defines the soft constraints for the feature selection problem, aiming to maximize the total value of selected features by penalizing deselection.

```python
# Goal: Maximize total value of selected features
# Strategy: Penalize NOT selecting each feature by its value
# This is COUNTERINTUITIVE but correct!

for feature, value in values.items():
    wcnf.append([feature], weight=value)  # Penalty = value if feature=FALSE
    
# Example: cloud (value=10) not selected → penalty of 10
# MaxSAT minimizes penalties → selects high-value features
```

--------------------------------

### MCP Solver Feature Selection Example: Hard Constraints

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Implements hard constraints for the feature selection problem, such as dependencies between features (e.g., if AI is selected, cloud must also be selected).

```python
# Hard constraints: Dependencies
# If AI selected, must have cloud
wcnf.append([-ai, cloud])  # NOT ai OR cloud

# If analytics selected, must have integration
wcnf.append([-analytics, integration])
```

--------------------------------

### Interpreting Solver Model

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Explains how to interpret the model returned by `solver.get_model()`. Positive numbers indicate TRUE variables, and negative numbers indicate FALSE variables. Includes examples for checking variable truthfulness and creating a solution dictionary.

```python
model = solver.get_model()
is_true = X in model  # Will be True if variable X is true in the solution

# With variable mapping
is_x1_true = var_mapping["x1"] in model

# Create a complete solution dictionary
solution = {name: (vid in model) for name, vid in var_mapping.items()}
```

--------------------------------

### Instantiate and Compute with RC2 Solver

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/maxsat/instructions.md

Demonstrates the mandatory steps of instantiating the RC2 solver with a WCNF object and calling the compute() method to find a solution. It also shows how to handle the case where a solution is found versus when it is not.

```python
from mcp_solver.maxsat import RC2, WCNF

# Assume wcnf is a pre-defined WCNF object
wcnf = WCNF()
# ... add constraints to wcnf ...

with RC2(wcnf) as solver:
    # MANDATORY: Call compute() to solve the problem
    model = solver.compute()  # Returns variable assignments or None
    
    if model:
        # Solution found - model contains true variables
        # Create solution dictionary
        solution = {
            "itemA": "itemA" in model,
            "itemB": "itemB" in model,
            "itemC": "itemC" in model
        }
        
        # MANDATORY: Call export_solution with results
        export_solution({
            "satisfiable": True,
            "cost": solver.cost,  # Total weight of unsatisfied soft clauses
            "assignment": solution
        })
    else:
        # No solution exists (hard constraints cannot be satisfied)
        export_solution({
            "satisfiable": False,
            "message": "No solution exists"
        })
```

--------------------------------

### Variable Mapping with VariableMap Class

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/pysat/instructions.md

Illustrates the recommended approach using the `VariableMap` class for creating and managing variable mappings. This includes adding constraints and processing solver results.

```python
# 1. Create formula and variable mapping
from pysat.formula import CNF
from pysat.solvers import Glucose3

formula = CNF()
var_map = VariableMap()

# 2. Create variables with meaningful names
x1 = var_map.create_var("x1")
x2 = var_map.create_var("x2")
x3 = var_map.create_var("x3")

# 3. Add constraints using helper functions
# Add constraint: exactly 2 of x1, x2, x3 must be true
for clause in exactly_k([x1, x2, x3], 2):
    formula.append(clause)

# Add constraint: if x1 then x2
formula.append([-x1, x2])  # NOT x1 OR x2

# 4. Solve and process results
solver = Glucose3()
solver.append_formula(formula)

if solver.solve():
    model = solver.get_model()
    solution = var_map.interpret_model(model)
    
    export_solution({
        "satisfiable": True,
        "assignment": solution
    })
else:
    export_solution({
        "satisfiable": False,
        "message": "No solution exists"
    })
    
# 5. Always free solver memory
solver.delete()
```

--------------------------------

### Example Z3 Model with Constraints

Source: https://github.com/szeider/mcp-solver/blob/main/prompts/z3/instructions.md

A complete example demonstrating Z3 variable creation, constraint addition (sorting and bounds), and solution export.

```python
from z3 import *
from mcp_solver.z3 import export_solution

# Create array of 8 integers
arr = [Int(f"x_{i}") for i in range(8)]

solver = Solver()

# For sorting constraint with Python lists, use loops:
for i in range(7):
    solver.add(arr[i] <= arr[i+1])

# Add other constraints using loops
for i in range(8):
    solver.add(arr[i] >= 1)
    solver.add(arr[i] <= 15)

# Check solution
if solver.check() == sat:
    export_solution(solver=solver, variables={f"x_{i}": arr[i] for i in range(8)})
```