Send a DIMACS CNF formula, get SAT/UNSAT back. Powered by npdollars.aws.monce.ai — parallel swarm: explorers grow implications, provers shrink assumptions, Kissat attacks the residual.
# Just describe the problem curl -sX POST https://monceapp.aws.monce.ai/v1/chat \ -F "model_id=eu.anthropic.claude-haiku-4-5-20251001-v1:0" \ -F "message=Solve this SAT: p cnf 3 2 1 -2 0 2 3 0" | jq .reply # Model calls sat_cnf tool internally → "The problem is satisfiable."
# POST to npdollars directly curl -sX POST https://npdollars.aws.monce.ai/cnf/solve \ -H "Content-Type: application/json" \ -d '{ "dimacs": "p cnf 3 2\n1 -2 0\n2 3 0", "budget": 10 }' # → {"result": "SAT", "assignment": [1, -2, 3]}
from monceai import SAT
result = SAT("p cnf 3 2\n1 -2 0\n2 3 0", budget=10)
result.result # "SAT"
result.assignment # [1, -2, 3]
result.tension # dictionary saturation
result.rounds # swarm rounds
When you ask the model to do both (train a classifier AND solve a SAT problem),
both tools fire in parallel via ThreadPoolExecutor. The model synthesizes both results into one answer.
snake_csv ████░░░░░░ 166ms → snakebatch.aws.monce.ai
sat_cnf ████████░░ 362ms → npdollars.aws.monce.ai
↑
wall clock: 362ms (not 528ms)