Developers v8

API reference · request/response schema · client examples · paper · architecture · economics · satlib game

Base URL

https://npdollars.aws.monce.ai

Endpoints

POST /cnf/solve

Request:

curl -X POST https://npdollars.aws.monce.ai/cnf/solve \
  -H 'Content-Type: application/json' \
  -d '{"dimacs": "p cnf 3 2\n1 2 3 0\n-1 -2 3 0\n", "budget": 10, "max_workers": 30}'

Request body:

{
  "dimacs":       string,      // DIMACS CNF formula (required)
  "budget":       float,       // wall-clock budget in seconds (default 30)
  "max_workers":  int,         // v6/v7 worker ceiling (default 100)
  "mode":         string       // "auto" | "haiku" | "sonnet" | "opus" (default "auto")
}

Response envelope (stable across all engines):

{
  "session_id":        "abcd1234ef56",
  "result":            "SAT" | "UNSAT" | "REDUCED" | "TIMEOUT",
  "engine":            "kissat" | "v6" | "v7" | "local_reduce" | "fast_reduce" | "v8_watchdog",
  "solved_by":         "v8_kissat" | "v8_race_kissat" | "v8_race_v6:..." | "v8_v7:..." | "v8_reduced" | ...,
  "tier":              "small" | "medium" | "large" | "xlarge",
  "tokens_in":         int,    // bytes of request CNF (1 byte = 1 token)
  "tokens_out":        int,    // bytes of response CNF
  "n_vars":            int,
  "n_clauses":         int,
  "total_ms":          float,
  "cost_usd":          float,

  "assignment":        [int],  // SAT: full model
  "partial_backbones": [int],  // REDUCED: forced literals proven
  "learned_2sat":      [[int,int]],  // REDUCED: proven binary implications
  "cnf":               string,       // always-valid DIMACS body with audit header

  "extras": {
    "var_reduction_pct":  float,
    "cls_reduction_pct":  float,
    "learned_clauses":    int,
    "workers":            int,
    "rounds":             int,
    "kissat_ms":          float,
    "engines_tried":      [string],
    "reason":             string       // e.g. "race_deadline", "v7_timeout_large"
  }
}

Result values

POST /satlib/claim

Pick an unsolved SATLIB instance, solve it, record it on the community leaderboard. Same envelope as /cnf/solve plus instance metadata.

Query parameters

Example: push mode

curl -X POST "https://npdollars.aws.monce.ai/satlib/claim?handle=me&push=laptop"

Push calls enforce a $12 per-call and $50 monthly spend ceiling. If either would be exceeded, the service refuses before any Lambda fires. Check budget first:

curl https://npdollars.aws.monce.ai/satlib/push_status

Python client

import requests, json

resp = requests.post(
    "https://npdollars.aws.monce.ai/cnf/solve",
    json={"dimacs": open("problem.cnf").read(), "budget": 30}
)
env = resp.json()

if env["result"] == "SAT":
    print("SAT, assignment:", env["assignment"][:10], "...")
elif env["result"] == "UNSAT":
    print("UNSAT proven in", env["total_ms"], "ms")
elif env["result"] == "REDUCED":
    ex = env["extras"]
    print(f"Reduced by {ex['cls_reduction_pct']}% in {env['total_ms']}ms")
    print("Re-POST the simplified CNF:", env["cnf"][:200])
else:
    print("Timeout:", env["extras"].get("reason"))

Bash one-liner

curl -sS -X POST https://npdollars.aws.monce.ai/cnf/solve \
  -H 'Content-Type: application/json' \
  --data-binary @- << EOF
{"dimacs": "$(cat problem.cnf | sed ':a;N;$!ba;s/\n/\\n/g')", "budget": 30}
EOF

DIMACS quick reference

c this is a comment
p cnf <n_vars> <n_clauses>
1 2 -3 0        # clause: (x1 OR x2 OR NOT x3)
-1 3 0          # clause: (NOT x1 OR x3)
0               # optional trailing zero

Limits

SDK

The monceai Python SDK wraps /cnf/solve:

pip install monceai

from monceai import SAT

result = SAT("problem.cnf", budget=10.0, vocal=True)
print(result.result)         # "SAT" | "UNSAT" | "REDUCED" | "TIMEOUT"
print(result.assignment)     # list[int] if SAT
print(result.cost)           # {"total_usd": 0.004, ...}

Rate limits & etiquette

No hard rate limits today. If you plan a batch run (> 100 calls), use tier=small where possible, back off on 5xx, and keep push mode for the instances that actually need it. The gate allows 6 concurrent solves on EC2; exceeding that queues gracefully.

Charles Dana · Monce SAS · npdollars.aws.monce.ai · April 2026
Co-Authored-By: Claude (Anthropic)