Integrate Constraint Solvers (e.g. Z3)

[bitfieldz]

Hi,

Very cool, very interesting project.

Having experimented with it a bit, at a very high level, seems like the main PAI 'algorithm' extracts constraints from the user's prompt, attempts to proactively solve for those constraints. Has been very effective in my experience so far.

I am wondering if integration with a constraint solver, e.g. z3, has been considered, perhaps via an MCP, like this one.

I haven't experimented with constraint solvers in an AI context yet (on my TODO list), but I wonder if they could be leveraged in the PAI context to increase overall speed, token efficiency, and maybe even confidence in outcome validation. (On the other hand, I could also see such an integration adding a level of determinism/specificity which ends up being _un_helpful. :) )

Curious to hear others' thoughts & experiences!

[docxology]

Great proposal, @spirotot — we built it.

The formal_verification module in Codomyrmex now integrates Z3 as a constraint solver backend, modeled after the mcp-solver 6-tool interface pattern you referenced. It lives at src/codomyrmex/formal_verification/ and provides:

What's implemented:

• Z3 SMT solver backend with the full mcp-solver interface (clear_model, add_item, delete_item, replace_item, get_model, solve_model)
• ISC verification bridge (verify_criteria_consistency()) — takes PAI Algorithm criteria directly and checks them for mutual satisfiability. It automatically extracts numeric constraints from natural language descriptions ("response time under 200ms" → var < 200)
• 6 MCP tools so Claude Code agents can build and solve constraint models interactively during Algorithm execution
• 59 unit tests covering solver operations, ISC verification, MCP tools, regex pattern extraction, edge cases, and error handling
• Runnable PAI agent example (scripts/agents/z3_pai_example.py) — demonstrates ISC verification, conflict detection, and interactive MCP workflow in ~150 lines

On your three hypothesized benefits:

1. Speed — Confirmed. Z3 solves practical ISC constraint sets (5-20 criteria) in single-digit milliseconds. The overhead of translating criteria and invoking the solver is negligible compared to a single LLM call.

2. Token efficiency — The most interesting benefit in practice. When an ISC set is unsatisfiable (conflicting requirements), the solver catches it in OBSERVE before the Algorithm wastes tokens attempting BUILD/EXECUTE on an impossible criteria set. Early conflict detection is genuinely valuable.

3. Validation confidence — Nuanced. For criteria with numeric constraints ("under 200ms", "at least 100 users", "between 0.1 and 0.5"), Z3 provides mathematical proof of consistency. For qualitative criteria ("code is well-structured"), the solver correctly skips them. The result is a mix of deterministic and heuristic verification — which is actually the right answer.

On the rigidity concern — you were right to flag it. We explicitly designed the solver as advisory, not blocking. verify_criteria_consistency() always returns an ISCVerificationResult — it never raises on UNSAT, never blocks the AI from proceeding. The agent sees the analysis and decides how to act. This preserves the flexibility that makes the Algorithm effective while adding deterministic confidence where it applies.

The module supports Real types for float constraints (e.g., "error rate under 0.5"), handles criteria without IDs gracefully, and reports exactly which criteria were analyzed vs. skipped and why.

Architecturally, the backend is pluggable — Z3 is the primary backend, with PySAT and ASP planned for different constraint domains.

Thanks for the insight connecting ISC extraction to constraint satisfaction. It's a natural fit.