Upload solver_assistant_v3.py

solver_assistant_v3.py

@@ -0,0 +1,1788 @@
+#!/usr/bin/env python3
+"""
+solver_assistant_v3.py
+
+Natural language -> structured instance -> exact solver -> verified answer.
+JSON schema interface for LLM front-ends.
+Bench mode: instances with analytically-known optima.
+Cross-verifier: B&B vs independent exhaustive DFS (MAX-CUT).
+Stress test harness.
+
+No downloads. No network. Pure standard library.
+
+Usage:
+    python3 solver_assistant_v3.py                     # interactive REPL
+    python3 solver_assistant_v3.py "your problem"      # one-shot
+    python3 solver_assistant_v3.py --demo              # built-in demos
+    python3 solver_assistant_v3.py --stress            # stress test
+    python3 solver_assistant_v3.py --stress --trials 100
+    python3 solver_assistant_v3.py --bench             # analytic-optimum bench
+    python3 solver_assistant_v3.py --cross             # B&B vs DFS (MAX-CUT)
+    python3 solver_assistant_v3.py --cross --sizes 14,16,18,20,22
+    python3 solver_assistant_v3.py --json '{"type":"maxcut","edges":[["A","B",3]]}'
+    python3 solver_assistant_v3.py --help
+"""
+
+import itertools
+import json
+import math
+import random
+import re
+import sys
+import time
+
+
+# =============================================================================
+# SOLVERS
+# =============================================================================
+
+def cut_value(W, side):
+    n = len(W)
+    return sum(W[i][j]
+               for i in range(n) for j in range(i + 1, n)
+               if side[i] != side[j])
+
+
+def greedy_cut(W, seed=0):
+    n = len(W)
+    rng = random.Random(seed)
+    order = list(range(n))
+    rng.shuffle(order)
+    side = [0] * n
+    assigned = [False] * n
+    for v in order:
+        to0 = sum(W[v][u] for u in range(n) if assigned[u] and side[u] == 0)
+        to1 = sum(W[v][u] for u in range(n) if assigned[u] and side[u] == 1)
+        side[v] = 0 if to1 >= to0 else 1
+        assigned[v] = True
+    return cut_value(W, side), side
+
+
+def local_search_maxcut(W, side, passes=10):
+    n = len(W)
+    side = side[:]
+    cur = cut_value(W, side)
+    for _ in range(passes):
+        improved = False
+        for v in range(n):
+            Wv = W[v]
+            sv = side[v]
+            gain = 0
+            for u in range(n):
+                if u == v:
+                    continue
+                if side[u] == sv:
+                    gain += Wv[u]
+                else:
+                    gain -= Wv[u]
+            if gain > 0:
+                side[v] ^= 1
+                cur += gain
+                improved = True
+        if not improved:
+            break
+    return cur, side
+
+
+def warm_start_maxcut(W, restarts=64, seed=0):
+    best_val, best_side = -1, None
+    for r in range(restarts):
+        v, s = greedy_cut(W, seed=seed * 1000 + r)
+        v, s = local_search_maxcut(W, s, passes=5)
+        if v > best_val:
+            best_val, best_side = v, s
+    return best_val, best_side
+
+
+def brute_force_maxcut(W):
+    n = len(W)
+    best = -1
+    best_side = None
+    for mask in range(1 << n):
+        side = [(mask >> i) & 1 for i in range(n)]
+        v = cut_value(W, side)
+        if v > best:
+            best = v
+            best_side = side
+    return best, best_side
+
+
+def maxcut_bb(W, time_limit, warm, warm_side):
+    n = len(W)
+    side = [-1] * n
+    order = sorted(range(n), key=lambda v: -sum(W[v]))
+    st = {"best": float(warm), "best_side": list(warm_side),
+          "nodes": 0, "aborted": False}
+    t0 = time.perf_counter()
+
+    def ub():
+        fc = 0.0
+        for i in range(n):
+            si = side[i]
+            if si < 0:
+                continue
+            Wi = W[i]
+            for j in range(i + 1, n):
+                sj = side[j]
+                if sj >= 0 and si != sj:
+                    fc += Wi[j]
+        free = [v for v in range(n) if side[v] < 0]
+        extra = 0.0
+        for v in free:
+            Wv = W[v]
+            wa = wb = 0.0
+            for u in range(n):
+                w = Wv[u]
+                if not w:
+                    continue
+                su = side[u]
+                if su == 0:
+                    wa += w
+                elif su == 1:
+                    wb += w
+            extra += wa if wa > wb else wb
+        for a in range(len(free)):
+            Wv = W[free[a]]
+            for b in range(a + 1, len(free)):
+                extra += Wv[free[b]]
+        return fc + extra
+
+    def rec():
+        if st["aborted"]:
+            return
+        st["nodes"] += 1
+        if (st["nodes"] & 0x3FF) == 0 and (time.perf_counter() - t0) > time_limit:
+            st["aborted"] = True
+            return
+        if ub() <= st["best"] + 1e-9:
+            return
+        v = -1
+        for x in order:
+            if side[x] < 0:
+                v = x
+                break
+        if v < 0:
+            val = cut_value(W, side)
+            if val > st["best"]:
+                st["best"] = val
+                st["best_side"] = side[:]
+            return
+        for s in (0, 1):
+            side[v] = s
+            rec()
+            side[v] = -1
+            if st["aborted"]:
+                return
+
+    rec()
+    st["seconds"] = time.perf_counter() - t0
+    return st
+
+
+def maxcut_dfs_exact(W, time_limit=60.0):
+    """
+    Independent exact MAX-CUT by exhaustive DFS.
+
+    Fix vertex 0 to side 0 (S/T symmetry halves the search). DFS over
+    remaining vertices, maintaining the cut value incrementally.
+
+    Shares no code with maxcut_bb: different algorithm, no upper bound,
+    no warm start, no pruning. Genuinely independent cross-check.
+    Returns (best_value, best_mask, aborted_flag).
+    """
+    n = len(W)
+    if n == 0:
+        return 0, 0, False
+
+    neighbors = []
+    total_to_earlier = [0] * n
+    for v in range(n):
+        ns = [(u, W[v][u]) for u in range(v) if W[v][u]]
+        neighbors.append(ns)
+        total_to_earlier[v] = sum(w for _, w in ns)
+
+    best = [-1]
+    best_mask = [0]
+    aborted = [False]
+    t0 = time.perf_counter()
+
+    def rec(v, mask, cut):
+        if aborted[0]:
+            return
+        if (v & 0xFF) == 0 and (time.perf_counter() - t0) > time_limit:
+            aborted[0] = True
+            return
+        if v == n:
+            if cut > best[0]:
+                best[0] = cut
+                best_mask[0] = mask
+            return
+        to_1 = 0
+        for u, w in neighbors[v]:
+            if mask & (1 << u):
+                to_1 += w
+        to_0 = total_to_earlier[v] - to_1
+        rec(v + 1, mask, cut + to_1)
+        rec(v + 1, mask | (1 << v), cut + to_0)
+
+    rec(1, 0, 0)
+    return best[0], best_mask[0], aborted[0]
+
+
+def solve_maxcut(W, names, time_limit=30.0):
+    n = len(W)
+    t0 = time.perf_counter()
+    if n <= 20:
+        val, side = brute_force_maxcut(W)
+        method = "brute force"
+        status = "OPTIMAL (proven)"
+    else:
+        warm, warm_side = warm_start_maxcut(W, restarts=64, seed=0)
+        res = maxcut_bb(W, time_limit, warm, warm_side)
+        val, side = res["best"], res["best_side"]
+        method = f"branch and bound ({res['nodes']:,} nodes)"
+        status = ("TIMEOUT (best found is lower bound)" if res["aborted"]
+                  else "OPTIMAL (proven)")
+    t = time.perf_counter() - t0
+    check = cut_value(W, side)
+    partition = {
+        "S": [names[i] for i in range(n) if side[i] == 0],
+        "T": [names[i] for i in range(n) if side[i] == 1],
+    }
+    return {
+        "value": val,
+        "partition": partition,
+        "verify": check == val,
+        "method": method,
+        "status": status,
+        "seconds": t,
+    }
+
+
+# --- SAT ---------------------------------------------------------------
+
+def verify_sat(clauses, assignment):
+    for c in clauses:
+        satisfied = False
+        for lit in c:
+            v = abs(lit)
+            if v in assignment and assignment[v] == (lit > 0):
+                satisfied = True
+                break
+        if not satisfied:
+            return False
+    return True
+
+
+def dpll(clauses, n, assignment, deadline, nodes):
+    nodes[0] += 1
+    if (nodes[0] & 0xFF) == 0 and time.perf_counter() > deadline:
+        raise TimeoutError
+
+    while True:
+        unit = None
+        for c in clauses:
+            satisfied = False
+            unassigned = []
+            for lit in c:
+                v = abs(lit)
+                if v in assignment:
+                    if assignment[v] == (lit > 0):
+                        satisfied = True
+                        break
+                else:
+                    unassigned.append(lit)
+            if satisfied:
+                continue
+            if not unassigned:
+                return None
+            if len(unassigned) == 1:
+                unit = unassigned[0]
+                break
+        if unit is None:
+            break
+        assignment[abs(unit)] = (unit > 0)
+
+    pos, neg = set(), set()
+    for c in clauses:
+        for lit in c:
+            v = abs(lit)
+            if v in assignment:
+                continue
+            (pos if lit > 0 else neg).add(v)
+    pure_pos = pos - neg
+    pure_neg = neg - pos
+    if pure_pos or pure_neg:
+        new_assign = dict(assignment)
+        for v in pure_pos:
+            new_assign[v] = True
+        for v in pure_neg:
+            new_assign[v] = False
+        return dpll(clauses, n, new_assign, deadline, nodes)
+
+    all_sat = True
+    for c in clauses:
+        satisfied = False
+        for lit in c:
+            v = abs(lit)
+            if v in assignment and assignment[v] == (lit > 0):
+                satisfied = True
+                break
+        if not satisfied:
+            all_sat = False
+            break
+    if all_sat:
+        for v in range(1, n + 1):
+            if v not in assignment:
+                assignment[v] = True
+        return assignment
+
+    counts = {}
+    for c in clauses:
+        for lit in c:
+            v = abs(lit)
+            if v not in assignment:
+                counts[v] = counts.get(v, 0) + 1
+    if not counts:
+        return None
+    var = max(counts, key=counts.get)
+
+    for val in (True, False):
+        new_assign = dict(assignment)
+        new_assign[var] = val
+        result = dpll(clauses, n, new_assign, deadline, nodes)
+        if result is not None:
+            return result
+    return None
+
+
+def solve_sat(clauses, n_vars, time_limit=30.0):
+    deadline = time.perf_counter() + time_limit
+    nodes = [0]
+    t0 = time.perf_counter()
+    try:
+        result = dpll(clauses, n_vars, {}, deadline, nodes)
+        t = time.perf_counter() - t0
+        if result is None:
+            return {
+                "satisfiable": False,
+                "model": None,
+                "verify": True,
+                "method": f"DPLL ({nodes[0]:,} nodes)",
+                "status": "UNSAT (proven)",
+                "seconds": t,
+            }
+        ok = verify_sat(clauses, result)
+        return {
+            "satisfiable": True,
+            "model": {v: result[v] for v in range(1, n_vars + 1)},
+            "verify": ok,
+            "method": f"DPLL ({nodes[0]:,} nodes)",
+            "status": "SAT (model verified)",
+            "seconds": t,
+        }
+    except TimeoutError:
+        t = time.perf_counter() - t0
+        return {
+            "satisfiable": None,
+            "model": None,
+            "verify": False,
+            "method": f"DPLL ({nodes[0]:,} nodes)",
+            "status": "TIMEOUT",
+            "seconds": t,
+        }
+
+
+# --- SUBSET-SUM --------------------------------------------------------
+
+def subset_sum_mim(arr, target):
+    n = len(arr)
+    half = n // 2
+    left, right = arr[:half], arr[half:]
+
+    def all_sums(a):
+        out = []
+        for mask in range(1 << len(a)):
+            s = 0
+            for i in range(len(a)):
+                if mask & (1 << i):
+                    s += a[i]
+            out.append((s, mask))
+        return out
+
+    L = all_sums(left)
+    R = all_sums(right)
+    R.sort()
+
+    for s, m in L:
+        need = target - s
+        lo, hi = 0, len(R)
+        while lo < hi:
+            mid = (lo + hi) // 2
+            if R[mid][0] < need:
+                lo = mid + 1
+            else:
+                hi = mid
+        if lo < len(R) and R[lo][0] == need:
+            return m | (R[lo][1] << half)
+    return None
+
+
+def brute_force_subset_sum(arr, target):
+    n = len(arr)
+    for mask in range(1 << n):
+        s = sum(arr[i] for i in range(n) if mask & (1 << i))
+        if s == target:
+            return mask
+    return None
+
+
+def solve_subset_sum(arr, target):
+    t0 = time.perf_counter()
+    mask = subset_sum_mim(arr, target)
+    t = time.perf_counter() - t0
+    if mask is None:
+        return {
+            "found": False,
+            "subset": None,
+            "verify": True,
+            "method": "meet-in-the-middle",
+            "status": "NO EXACT SUBSET",
+            "seconds": t,
+        }
+    chosen = [arr[i] for i in range(len(arr)) if mask & (1 << i)]
+    return {
+        "found": True,
+        "subset": chosen,
+        "verify": sum(chosen) == target,
+        "method": "meet-in-the-middle",
+        "status": "FOUND (verified)",
+        "seconds": t,
+    }
+
+
+# --- TSP ---------------------------------------------------------------
+
+def held_karp(D):
+    n = len(D)
+    INF = float("inf")
+    size = 1 << n
+    dp = [[INF] * n for _ in range(size)]
+    parent = [[-1] * n for _ in range(size)]
+    dp[1][0] = 0.0
+
+    for mask in range(size):
+        row = dp[mask]
+        for i in range(n):
+            if not (mask & (1 << i)):
+                continue
+            ci = row[i]
+            if ci == INF:
+                continue
+            Di = D[i]
+            for j in range(n):
+                if mask & (1 << j):
+                    continue
+                nm = mask | (1 << j)
+                nc = ci + Di[j]
+                if nc < dp[nm][j]:
+                    dp[nm][j] = nc
+                    parent[nm][j] = i
+
+    full = size - 1
+    best = INF
+    end = -1
+    for i in range(n):
+        c = dp[full][i] + D[i][0]
+        if c < best:
+            best = c
+            end = i
+
+    path = []
+    mask = full
+    i = end
+    while i != -1:
+        path.append(i)
+        p = parent[mask][i]
+        mask ^= (1 << i)
+        i = p
+    path.reverse()
+    return best, path
+
+
+def brute_force_tsp(points):
+    n = len(points)
+    best_cost = float("inf")
+    best_tour = None
+    for perm in itertools.permutations(range(1, n)):
+        tour = (0,) + perm
+        cost = sum(math.dist(points[tour[i]], points[tour[(i + 1) % n]])
+                   for i in range(n))
+        if cost < best_cost:
+            best_cost = cost
+            best_tour = list(tour)
+    return best_cost, best_tour
+
+
+def solve_tsp(points, time_limit=60.0):
+    n = len(points)
+    if n > 18:
+        return {
+            "tour": None, "length": None, "verify": False,
+            "method": "Held-Karp refused",
+            "status": f"TOO LARGE (n={n} > 18)", "seconds": 0.0,
+        }
+    D = [[math.dist(points[i], points[j]) for j in range(n)] for i in range(n)]
+    t0 = time.perf_counter()
+    cost, tour = held_karp(D)
+    t = time.perf_counter() - t0
+    s = sum(D[tour[k]][tour[(k + 1) % n]] for k in range(n))
+    return {
+        "tour": tour, "length": cost,
+        "verify": abs(s - cost) < 1e-6,
+        "method": "Held-Karp DP",
+        "status": "OPTIMAL (proven)",
+        "seconds": t,
+    }
+
+
+# =============================================================================
+# TEXT PARSERS
+# =============================================================================
+
+class ParseError(Exception):
+    pass
+
+
+EDGE_RE = re.compile(
+    r"([A-Za-z][A-Za-z0-9_]*|\d+)\s*[-=:]\s*([A-Za-z][A-Za-z0-9_]*|\d+)"
+    r"\s*(?:[:=]\s*(-?\d+))?"
+)
+
+
+def parse_maxcut(text):
+    edges = []
+    for m in EDGE_RE.finditer(text):
+        u, v, w = m.group(1), m.group(2), m.group(3)
+        edges.append((u, v, int(w) if w is not None else 1))
+    if not edges:
+        raise ParseError("No edges found. Try: max cut on A-B:3, B-C:5")
+    names = []
+    for u, v, _ in edges:
+        if u not in names:
+            names.append(u)
+        if v not in names:
+            names.append(v)
+    index = {n: i for i, n in enumerate(names)}
+    n = len(names)
+    W = [[0] * n for _ in range(n)]
+    for u, v, w in edges:
+        i, j = index[u], index[v]
+        W[i][j] = w
+        W[j][i] = w
+    return W, names
+
+
+CLAUSE_RE = re.compile(r"\(([^()]+)\)")
+
+
+def parse_sat(text):
+    raw_clauses = CLAUSE_RE.findall(text)
+    if not raw_clauses:
+        m = re.search(
+            r"(?:sat|3[\s-]?sat|formula|clauses?)\s*[:=]?\s*(.+)$",
+            text, re.I | re.S,
+        )
+        rest = m.group(1).strip() if m else text
+        raw_clauses = re.split(r"\s+and\s+", rest, flags=re.I)
+
+    raw_clauses = [c for c in (r.strip() for r in raw_clauses) if c]
+    if not raw_clauses:
+        raise ParseError(
+            "No clauses found. Try: sat (x1 or -x2 or x3) and (x2 or x3)"
+        )
+
+    parsed = []
+    var_names = set()
+    for raw in raw_clauses:
+        raw = raw.strip().strip("()").strip()
+        if not raw:
+            continue
+        parts = re.split(r"\s+(?:or|\|)\s+|\s*,\s*", raw, flags=re.I)
+        clause = []
+        for p in parts:
+            p = p.strip()
+            if not p:
+                continue
+            neg = False
+            while p and p[0] in "-~!":
+                neg = not neg
+                p = p[1:].strip()
+            if not p:
+                raise ParseError("Empty literal in clause")
+            if re.match(r"^([A-Za-z_]*)(\d+)$", p) or \
+               re.match(r"^[A-Za-z_]\w*$", p):
+                var_names.add(p)
+                clause.append((p, neg))
+            else:
+                raise ParseError(f"Cannot parse literal: {p!r}")
+        if clause:
+            parsed.append(clause)
+
+    if not parsed:
+        raise ParseError("Could not parse any clauses.")
+
+    name_to_int = {name: i + 1 for i, name in enumerate(sorted(var_names))}
+    int_clauses = [
+        tuple((name_to_int[n] if not neg else -name_to_int[n])
+              for n, neg in c)
+        for c in parsed
+    ]
+    return int_clauses, len(name_to_int), name_to_int
+
+
+LIST_RE = re.compile(r"\[([^\]]+)\]")
+
+
+def parse_subset_sum(text):
+    m = LIST_RE.search(text)
+    if m:
+        nums = [int(x) for x in re.split(r"[,\s]+", m.group(1)) if x.strip()]
+    else:
+        nums = [int(x) for x in re.findall(r"-?\d+", text)]
+    if not nums:
+        raise ParseError("No numbers found. Try: subset sum [3, 7, 1] target 4")
+    target = None
+    for pat in [r"(?:target|sum to|summing to|equal(?:s| to)?|=)\s*(-?\d+)",
+                r"(-?\d+)\s*$"]:
+        tm = re.search(pat, text, re.I)
+        if tm:
+            target = int(tm.group(1))
+            break
+    defaulted = False
+    if target is None:
+        target = sum(nums) // 2
+        defaulted = True
+    return nums, target, defaulted
+
+
+PAIR_RE = re.compile(
+    r"\(\s*(-?\d+(?:\.\d+)?(?:[eE][+-]?\d+)?)\s*,\s*"
+    r"(-?\d+(?:\.\d+)?(?:[eE][+-]?\d+)?)\s*\)"
+)
+
+
+def parse_tsp(text):
+    pairs = PAIR_RE.findall(text)
+    if not pairs:
+        raise ParseError(
+            "No coordinates found. Try: tsp (0,0) (1,2) (3,1) (2,4)"
+        )
+    points = [(float(a), float(b)) for a, b in pairs]
+    if len(points) < 3:
+        raise ParseError("TSP needs at least 3 points.")
+    return points
+
+
+# =============================================================================
+# JSON SCHEMA INTERFACE  (LLM adapter point)
+# =============================================================================
+
+def _require(d, key, typ, ctx):
+    if key not in d:
+        raise ValueError(f"{ctx}: missing field {key!r}")
+    v = d[key]
+    if not isinstance(v, typ):
+        raise ValueError(
+            f"{ctx}: field {key!r} must be {typ.__name__}, "
+            f"got {type(v).__name__}"
+        )
+    return v
+
+
+def _validate_maxcut_schema(d):
+    edges = _require(d, "edges", list, "maxcut")
+    if not edges:
+        raise ValueError("maxcut: 'edges' list is empty")
+    names = []
+    parsed = []
+    for i, e in enumerate(edges):
+        if not isinstance(e, (list, tuple)) or len(e) not in (2, 3):
+            raise ValueError(
+                f"maxcut: edge {i} must be [u, v] or [u, v, w], got {e!r}"
+            )
+        u, v = e[0], e[1]
+        w = e[2] if len(e) == 3 else 1
+        if not isinstance(w, int) or w < 0:
+            raise ValueError(
+                f"maxcut: edge {i} weight must be non-negative int, got {w!r}"
+            )
+        for x in (u, v):
+            if not isinstance(x, (str, int)):
+                raise ValueError(f"maxcut: vertex {x!r} must be str or int")
+            if x not in names:
+                names.append(x)
+        parsed.append((u, v, w))
+    n = len(names)
+    index = {nm: i for i, nm in enumerate(names)}
+    W = [[0] * n for _ in range(n)]
+    for u, v, w in parsed:
+        i, j = index[u], index[v]
+        W[i][j] = w
+        W[j][i] = w
+    return W, names
+
+
+def _validate_sat_schema(d):
+    clauses = _require(d, "clauses", list, "sat")
+    if not clauses:
+        raise ValueError("sat: 'clauses' list is empty")
+    n_vars = d.get("n_vars")
+    if n_vars is not None and not isinstance(n_vars, int):
+        raise ValueError("sat: 'n_vars' must be int if present")
+    max_var = 0
+    int_clauses = []
+    for i, c in enumerate(clauses):
+        if not isinstance(c, (list, tuple)) or len(c) < 1:
+            raise ValueError(f"sat: clause {i} must be a non-empty list")
+        clause = []
+        for lit in c:
+            if not isinstance(lit, int) or lit == 0:
+                raise ValueError(
+                    f"sat: literal {lit!r} in clause {i} must be nonzero int"
+                )
+            max_var = max(max_var, abs(lit))
+            clause.append(lit)
+        int_clauses.append(tuple(clause))
+    if n_vars is None:
+        n_vars = max_var
+    elif n_vars < max_var:
+        raise ValueError(
+            f"sat: 'n_vars'={n_vars} but literal refers to var {max_var}"
+        )
+    return int_clauses, n_vars
+
+
+def _validate_subset_sum_schema(d):
+    nums = _require(d, "numbers", list, "subset_sum")
+    if not nums:
+        raise ValueError("subset_sum: 'numbers' list is empty")
+    for i, x in enumerate(nums):
+        if not isinstance(x, int):
+            raise ValueError(f"subset_sum: number {i} must be int, got {x!r}")
+    target = d.get("target")
+    if target is None:
+        target = sum(nums) // 2
+        defaulted = True
+    else:
+        if not isinstance(target, int):
+            raise ValueError("subset_sum: 'target' must be int")
+        defaulted = False
+    return nums, target, defaulted
+
+
+def _validate_tsp_schema(d):
+    pts = _require(d, "points", list, "tsp")
+    if len(pts) < 3:
+        raise ValueError("tsp: need at least 3 points")
+    out = []
+    for i, p in enumerate(pts):
+        if not isinstance(p, (list, tuple)) or len(p) != 2:
+            raise ValueError(f"tsp: point {i} must be [x, y], got {p!r}")
+        x, y = p
+        if not isinstance(x, (int, float)) or not isinstance(y, (int, float)):
+            raise ValueError(f"tsp: point {i} coords must be numeric")
+        out.append((float(x), float(y)))
+    return out
+
+
+def dispatch_from_json(schema, verbose=True):
+    if not isinstance(schema, dict):
+        raise ValueError("schema must be a dict")
+    kind = schema.get("type")
+    if kind is None:
+        raise ValueError("schema missing 'type' field")
+    kind = str(kind).lower()
+
+    if kind == "maxcut":
+        W, names = _validate_maxcut_schema(schema)
+        if verbose:
+            n_edges = sum(1 for i in range(len(W))
+                          for j in range(i + 1, len(W)) if W[i][j])
+            print(f"  [json] maxcut: {len(names)} vertices, {n_edges} edges")
+        r = solve_maxcut(W, names, time_limit=30.0)
+        if verbose:
+            _report_maxcut(r)
+        return r
+
+    if kind == "sat":
+        clauses, n_vars = _validate_sat_schema(schema)
+        if verbose:
+            print(f"  [json] sat: {n_vars} variables, {len(clauses)} clauses")
+        r = solve_sat(clauses, n_vars, time_limit=30.0)
+        if verbose:
+            _report_sat(r)
+        return r
+
+    if kind == "subset_sum":
+        nums, target, defaulted = _validate_subset_sum_schema(schema)
+        if verbose:
+            note = " (target defaulted to half-total)" if defaulted else ""
+            print(f"  [json] subset_sum: {len(nums)} numbers, "
+                  f"target={target}{note}")
+        r = solve_subset_sum(nums, target)
+        if verbose:
+            _report_subset_sum(r)
+        return r
+
+    if kind == "tsp":
+        pts = _validate_tsp_schema(schema)
+        if verbose:
+            print(f"  [json] tsp: {len(pts)} points")
+        r = solve_tsp(pts, time_limit=60.0)
+        if verbose:
+            _report_tsp(r)
+        return r
+
+    raise ValueError(f"unknown schema type: {kind!r}")
+
+
+# =============================================================================
+# TEXT FRONT-END
+# =============================================================================
+
+def detect_kind(text):
+    t = text.lower()
+    if re.search(r"\b(max[\s-]?cut|maximum cut|maxcut)\b", t):
+        return "maxcut"
+    if re.search(r"\b(3[\s-]?sat|sat\b|satisfiab)", t):
+        return "sat"
+    if re.search(r"\b(subset[\s-]?sum|partition|sum to|target sum)\b", t):
+        return "subset_sum"
+    if re.search(r"\b(tsp|travell?ing salesman|shortest tour|best tour)\b", t):
+        return "tsp"
+    return None
+
+
+def _report_maxcut(r):
+    print(f"  method: {r['method']}  ({r['seconds']:.2f}s)")
+    print(f"  status: {r['status']}")
+    print(f"  best cut value: {r['value']}")
+    print(f"  partition S: {r['partition']['S']}")
+    print(f"  partition T: {r['partition']['T']}")
+    print(f"  verify: {'OK' if r['verify'] else 'FAIL'}")
+
+
+def _report_sat(r):
+    print(f"  method: {r['method']}  ({r['seconds']:.2f}s)")
+    print(f"  status: {r['status']}")
+    if r["satisfiable"]:
+        true_vars = [v for v in r["model"] if r["model"][v]]
+        print(f"  model true vars: {true_vars}")
+    print(f"  verify: {'OK' if r['verify'] else 'FAIL'}")
+
+
+def _report_subset_sum(r):
+    print(f"  method: {r['method']}  ({r['seconds']:.2f}s)")
+    print(f"  status: {r['status']}")
+    if r["found"]:
+        print(f"  subset: {r['subset']}")
+        print(f"  sum: {sum(r['subset'])}")
+    print(f"  verify: {'OK' if r['verify'] else 'FAIL'}")
+
+
+def _report_tsp(r):
+    print(f"  method: {r['method']}  ({r['seconds']:.2f}s)")
+    print(f"  status: {r['status']}")
+    if r["tour"] is not None:
+        print(f"  tour: {r['tour']}")
+        print(f"  length: {r['length']:.4f}")
+    print(f"  verify: {'OK' if r['verify'] else 'FAIL'}")
+
+
+def dispatch(text, verbose=True):
+    kind = detect_kind(text)
+    if kind is None:
+        if verbose:
+            print("  Could not identify problem type.")
+            print("  Supported keywords:")
+            print("    'max cut' / 'maxcut'      -> MAX-CUT")
+            print("    'sat' / '3-sat'            -> Boolean satisfiability")
+            print("    'subset sum' / 'target'    -> SUBSET-SUM")
+            print("    'tsp' / 'tour'             -> Traveling salesman")
+        return None
+
+    if verbose:
+        print(f"  detected: {kind.upper()}")
+
+    if kind == "maxcut":
+        try:
+            W, names = parse_maxcut(text)
+        except ParseError as e:
+            if verbose:
+                print(f"  parse error: {e}")
+            return None
+        if verbose:
+            n_edges = sum(1 for i in range(len(W))
+                          for j in range(i + 1, len(W)) if W[i][j])
+            print(f"  parsed: {len(names)} vertices, {n_edges} edges")
+        r = solve_maxcut(W, names, time_limit=30.0)
+        if verbose:
+            _report_maxcut(r)
+        return r
+
+    if kind == "sat":
+        try:
+            clauses, n_vars, name_to_int = parse_sat(text)
+        except ParseError as e:
+            if verbose:
+                print(f"  parse error: {e}")
+            return None
+        if verbose:
+            print(f"  parsed: {n_vars} variables, {len(clauses)} clauses")
+        r = solve_sat(clauses, n_vars, time_limit=30.0)
+        if r["satisfiable"] and r["model"] is not None:
+            inv = {v: k for k, v in name_to_int.items()}
+            r["model"] = {inv[v]: r["model"][v] for v in r["model"]}
+        if verbose:
+            _report_sat(r)
+        return r
+
+    if kind == "subset_sum":
+        try:
+            nums, target, defaulted = parse_subset_sum(text)
+        except ParseError as e:
+            if verbose:
+                print(f"  parse error: {e}")
+            return None
+        if verbose:
+            note = " (defaulted to half-total)" if defaulted else ""
+            print(f"  parsed: {len(nums)} numbers, target = {target}{note}")
+        r = solve_subset_sum(nums, target)
+        if verbose:
+            _report_subset_sum(r)
+        return r
+
+    if kind == "tsp":
+        try:
+            pts = parse_tsp(text)
+        except ParseError as e:
+            if verbose:
+                print(f"  parse error: {e}")
+            return None
+        if verbose:
+            print(f"  parsed: {len(pts)} points")
+        r = solve_tsp(pts, time_limit=60.0)
+        if verbose:
+            _report_tsp(r)
+        return r
+
+    return None
+
+
+# =============================================================================
+# BENCH INSTANCES
+# =============================================================================
+
+def pigeonhole_clauses(m, n):
+    """PHP(m, n): m pigeons, n holes. UNSAT iff m > n."""
+    def var(i, j):
+        return (i - 1) * n + j
+    clauses = []
+    for i in range(1, m + 1):
+        clauses.append([var(i, j) for j in range(1, n + 1)])
+    for j in range(1, n + 1):
+        for i1 in range(1, m + 1):
+            for i2 in range(i1 + 1, m + 1):
+                clauses.append([-var(i1, j), -var(i2, j)])
+    return clauses, m * n
+
+
+def bench_maxcut():
+    out = []
+
+    for n in [4, 5, 6, 7, 8]:
+        names = [f"v{i}" for i in range(n)]
+        edges = [[names[i], names[j], 1]
+                 for i in range(n) for j in range(i + 1, n)]
+        out.append((f"K_{n} complete, unit weights",
+                    {"type": "maxcut", "edges": edges},
+                    (n * n) // 4,
+                    "analytic: floor(n^2/4)"))
+
+    for n in [4, 6, 8, 10]:
+        names = [f"v{i}" for i in range(n)]
+        edges = [[names[i], names[(i + 1) % n], 1] for i in range(n)]
+        out.append((f"C_{n} cycle, unit weights",
+                    {"type": "maxcut", "edges": edges},
+                    n, "analytic: n for even cycle"))
+
+    for n in [5, 7, 9]:
+        names = [f"v{i}" for i in range(n)]
+        edges = [[names[i], names[(i + 1) % n], 1] for i in range(n)]
+        out.append((f"C_{n} cycle, unit weights",
+                    {"type": "maxcut", "edges": edges},
+                    n - 1, "analytic: n-1 for odd cycle"))
+
+    for n in [5, 6, 7, 8]:
+        names = [f"v{i}" for i in range(n)]
+        edges = [[names[i], names[i + 1], 1] for i in range(n - 1)]
+        out.append((f"P_{n} path, unit weights",
+                    {"type": "maxcut", "edges": edges},
+                    n - 1, "analytic: n-1"))
+
+    for m, n in [(3, 3), (4, 4), (3, 5)]:
+        left = [f"L{i}" for i in range(m)]
+        right = [f"R{j}" for j in range(n)]
+        edges = [[li, rj, 1] for li in left for rj in right]
+        out.append((f"K_{{{m},{n}}} complete bipartite",
+                    {"type": "maxcut", "edges": edges},
+                    m * n, "analytic: all edges cuttable"))
+
+    return out
+
+
+def bench_sat():
+    out = []
+
+    out.append(("trivial unit clause (x1)",
+                {"type": "sat", "n_vars": 1, "clauses": [[1]]},
+                True, "x1=True"))
+
+    out.append(("(x1 | x2) & -x1",
+                {"type": "sat", "n_vars": 2, "clauses": [[1, 2], [-1]]},
+                True, "x1=False, x2=True"))
+
+    out.append(("(x1) & (-x1)",
+                {"type": "sat", "n_vars": 1, "clauses": [[1], [-1]]},
+                False, "contradiction"))
+
+    clauses, n_vars = pigeonhole_clauses(3, 2)
+    out.append(("PHP(3,2) pigeonhole",
+                {"type": "sat", "n_vars": n_vars, "clauses": clauses},
+                False, "pigeonhole: 3 pigeons, 2 holes"))
+
+    clauses, n_vars = pigeonhole_clauses(4, 3)
+    out.append(("PHP(4,3) pigeonhole",
+                {"type": "sat", "n_vars": n_vars, "clauses": clauses},
+                False, "pigeonhole: 4 pigeons, 3 holes"))
+
+    clauses = [[1, 2, 3], [-1, 2, 4], [-2, -3, 4]]
+    out.append(("3-SAT with known model (4 vars)",
+                {"type": "sat", "n_vars": 4, "clauses": clauses},
+                True, "model 1=T 2=T 3=F 4=T"))
+
+    return out
+
+
+def bench_subset_sum():
+    """Instances with subset-sum answers provable by hand."""
+    out = []
+
+    # Powers of 2: unique binary encoding for every target in [0, 127]
+    nums = [1, 2, 4, 8, 16, 32, 64]
+    out.append(("powers of 2, target=100",
+                {"type": "subset_sum", "numbers": nums, "target": 100},
+                True, "100 = 64 + 32 + 4"))
+    out.append(("powers of 2, target=127",
+                {"type": "subset_sum", "numbers": nums, "target": 127},
+                True, "127 = 1+2+4+8+16+32+64"))
+    out.append(("powers of 2, target=0",
+                {"type": "subset_sum", "numbers": nums, "target": 0},
+                True, "empty subset"))
+    out.append(("powers of 2, target=200",
+                {"type": "subset_sum", "numbers": nums, "target": 200},
+                False, "200 > total(127)"))
+
+    # {1,...,10} is subset-sum complete: every integer in [0,55] achievable.
+    # Only targets outside that range are provably UNSAT.
+    nums = list(range(1, 11))  # total = 55
+    out.append(("1..10, target=28",
+                {"type": "subset_sum", "numbers": nums, "target": 28},
+                True, "10 + 9 + 8 + 1 = 28"))
+    out.append(("1..10, target=55",
+                {"type": "subset_sum", "numbers": nums, "target": 55},
+                True, "the entire set"))
+    out.append(("1..10, target=60",
+                {"type": "subset_sum", "numbers": nums, "target": 60},
+                False, "60 > total(55)"))
+    out.append(("1..10, target=-1",
+                {"type": "subset_sum", "numbers": nums, "target": -1},
+                False, "all numbers positive"))
+
+    return out
+
+def bench_tsp():
+    out = []
+
+    for a, b in [(10, 10), (10, 20), (5, 12)]:
+        pts = [[0, 0], [a, 0], [a, b], [0, b]]
+        out.append((f"rectangle {a}x{b} corners",
+                    {"type": "tsp", "points": pts},
+                    2.0 * (a + b),
+                    f"perimeter 2*({a}+{b})"))
+
+    for n in [4, 5, 6]:
+        pts = [[i * 10, 0] for i in range(n)]
+        out.append((f"{n} collinear, spacing 10",
+                    {"type": "tsp", "points": pts},
+                    2.0 * 10 * (n - 1),
+                    "2*(max-min) for collinear"))
+
+    return out
+
+
+# =============================================================================
+# BENCH MODE
+# =============================================================================
+
+def run_bench(verbose=True):
+    print()
+    print("=" * 78)
+    print("BENCH MODE -- instances with analytically-known optima")
+    print("=" * 78)
+
+    total = 0
+    passed = 0
+
+    print()
+    print("  MAX-CUT:")
+    for name, schema, expected, source in bench_maxcut():
+        r = dispatch_from_json(schema, verbose=False)
+        got = r["value"]
+        ok = (got == expected)
+        total += 1
+        if ok:
+            passed += 1
+        if verbose:
+            tag = "PASS" if ok else "FAIL"
+            print(f"    [{tag}] {name:<36} solver={got:>5} "
+                  f"expected={expected:>5}  ({source})")
+
+    print()
+    print("  SAT:")
+    for name, schema, expected, source in bench_sat():
+        r = dispatch_from_json(schema, verbose=False)
+        got = r["satisfiable"]
+        ok = (got == expected)
+        total += 1
+        if ok:
+            passed += 1
+        if verbose:
+            tag = "PASS" if ok else "FAIL"
+            print(f"    [{tag}] {name:<36} solver={str(got):<5} "
+                  f"expected={str(expected):<5}  ({source})")
+
+    print()
+    print("  SUBSET-SUM:")
+    for name, schema, expected, source in bench_subset_sum():
+        r = dispatch_from_json(schema, verbose=False)
+        got = r["found"]
+        ok = (got == expected)
+        total += 1
+        if ok:
+            passed += 1
+        if verbose:
+            tag = "PASS" if ok else "FAIL"
+            print(f"    [{tag}] {name:<36} solver={str(got):<5} "
+                  f"expected={str(expected):<5}  ({source})")
+
+    print()
+    print("  TSP:")
+    for name, schema, expected, source in bench_tsp():
+        r = dispatch_from_json(schema, verbose=False)
+        got = r["length"]
+        ok = (got is not None and abs(got - expected) < 1e-6)
+        total += 1
+        if ok:
+            passed += 1
+        if verbose:
+            tag = "PASS" if ok else "FAIL"
+            gs = f"{got:.4f}" if got is not None else "None"
+            print(f"    [{tag}] {name:<36} solver={gs:>9} "
+                  f"expected={expected:>9.4f}  ({source})")
+
+    print()
+    print(f"  BENCH TOTAL: passed {passed}/{total}")
+    print("=" * 78)
+    return passed == total
+
+
+# =============================================================================
+# CROSS-VERIFY MODE
+# =============================================================================
+
+def run_cross(sizes=None, seed=0, dfs_time_limit=60.0, bb_time_limit=60.0,
+              verbose=True):
+    """Cross-verify MAX-CUT B&B against independent exhaustive DFS."""
+    if sizes is None:
+        sizes = [14, 16, 18, 20, 22]
+
+    print()
+    print("=" * 78)
+    print("CROSS-VERIFY -- MAX-CUT: B&B vs independent exhaustive DFS")
+    print("=" * 78)
+    print(f"  B&B time limit per instance    : {bb_time_limit:.0f}s")
+    print(f"  DFS time limit per instance    : {dfs_time_limit:.0f}s")
+    print()
+
+    rng = random.Random(seed)
+    results = []
+
+    print(f"  {'n':>3} {'edges':>6} {'B&B':>8} {'B&B(s)':>8} "
+          f"{'DFS':>8} {'DFS(s)':>8} {'verdict':>10}")
+    print("  " + "-" * 62)
+
+    for n in sizes:
+        schema = _rand_maxcut(n, rng.randint(0, 10**9))
+        W, _ = _validate_maxcut_schema(schema)
+        edges = sum(1 for i in range(n) for j in range(i + 1, n) if W[i][j])
+
+        # B&B
+        t0 = time.perf_counter()
+        warm, warm_side = warm_start_maxcut(W, restarts=64, seed=0)
+        bb_res = maxcut_bb(W, bb_time_limit, warm, warm_side)
+        bb_time = time.perf_counter() - t0
+        bb_val = bb_res["best"]
+        bb_aborted = bb_res["aborted"]
+
+        # DFS
+        t0 = time.perf_counter()
+        dfs_val, _, dfs_aborted = maxcut_dfs_exact(W, time_limit=dfs_time_limit)
+        dfs_time = time.perf_counter() - t0
+
+        if dfs_aborted and bb_aborted:
+            verdict = "both to"
+            agree = None
+        elif dfs_aborted:
+            verdict = "DFS to"
+            agree = None
+        elif bb_aborted:
+            verdict = "B&B to"
+            agree = None
+        elif bb_val == dfs_val:
+            verdict = "AGREE"
+            agree = True
+        else:
+            verdict = "DISAGREE"
+            agree = False
+
+        dfs_str = f"{dfs_val}" if not dfs_aborted else ">t"
+        bb_str = f"{bb_val}"
+        print(f"  {n:>3} {edges:>6} {bb_str:>8} {bb_time:>8.2f} "
+              f"{dfs_str:>8} {dfs_time:>8.2f} {verdict:>10}")
+
+        results.append((n, bb_val, dfs_val, bb_aborted, dfs_aborted, agree))
+
+    n_agree = sum(1 for r in results if r[5] is True)
+    n_disagree = sum(1 for r in results if r[5] is False)
+    n_timeout = sum(1 for r in results if r[5] is None)
+
+    print()
+    print(f"  AGREEMENT: {n_agree}   DISAGREEMENT: {n_disagree}   "
+          f"TIMEOUT-ON-ONE-SIDE: {n_timeout}")
+    print("=" * 78)
+    return n_disagree == 0
+
+
+# =============================================================================
+# STRESS TEST HARNESS
+# =============================================================================
+
+def _rand_maxcut(n, seed, wmax=10, density=1.0):
+    rng = random.Random(seed)
+    names = [f"v{i}" for i in range(n)]
+    edges = []
+    for i in range(n):
+        for j in range(i + 1, n):
+            if rng.random() < density:
+                edges.append([names[i], names[j], rng.randint(1, wmax)])
+    return {"type": "maxcut", "edges": edges}
+
+
+def _rand_sat(n, ratio, seed):
+    rng = random.Random(seed)
+    m = max(1, int(round(n * ratio)))
+    clauses = []
+    for _ in range(m):
+        vs = rng.sample(range(1, n + 1), min(3, n))
+        clauses.append([v if rng.random() < 0.5 else -v for v in vs])
+    return {"type": "sat", "n_vars": n, "clauses": clauses}
+
+
+def _rand_subset_sum(n, maxval, seed):
+    rng = random.Random(seed)
+    nums = [rng.randint(1, maxval) for _ in range(n)]
+    return {"type": "subset_sum", "numbers": nums, "target": sum(nums) // 2}
+
+
+def _rand_tsp(n, seed, span=100.0):
+    rng = random.Random(seed)
+    pts = [[rng.uniform(0, span), rng.uniform(0, span)] for _ in range(n)]
+    return {"type": "tsp", "points": pts}
+
+
+def schema_to_text(schema):
+    kind = schema["type"]
+    if kind == "maxcut":
+        parts = []
+        for e in schema["edges"]:
+            if len(e) == 3:
+                parts.append(f"{e[0]}-{e[1]}:{e[2]}")
+            else:
+                parts.append(f"{e[0]}-{e[1]}")
+        return "max cut on " + ", ".join(parts)
+    if kind == "sat":
+        clauses = ["(" + " or ".join(str(x) for x in c) + ")"
+                   for c in schema["clauses"]]
+        return "sat " + " and ".join(clauses)
+    if kind == "subset_sum":
+        nums = ", ".join(str(x) for x in schema["numbers"])
+        if "target" in schema and schema["target"] is not None:
+            return f"subset sum [{nums}] target {schema['target']}"
+        return f"subset sum [{nums}]"
+    if kind == "tsp":
+        pts = " ".join(f"({p[0]!r},{p[1]!r})" for p in schema["points"])
+        return "tsp " + pts
+    raise ValueError(f"unknown type: {kind!r}")
+
+
+def _schema_equivalent(a, b):
+    if a["type"] != b["type"]:
+        return False, "type mismatch"
+    t = a["type"]
+
+    if t == "maxcut":
+        def key(e):
+            u, v = e[0], e[1]
+            w = e[2] if len(e) == 3 else 1
+            if str(u) > str(v):
+                u, v = v, u
+            return (str(u), str(v), w)
+        return sorted(key(e) for e in a["edges"]) == \
+               sorted(key(e) for e in b["edges"]), "edge set differs"
+
+    if t == "sat":
+        def norm(c):
+            return tuple(sorted(set(c)))
+        ca = sorted(norm(c) for c in a["clauses"])
+        cb = sorted(norm(c) for c in b["clauses"])
+        na = a.get("n_vars") or max((abs(x) for c in a["clauses"] for x in c),
+                                    default=0)
+        nb = b.get("n_vars") or max((abs(x) for c in b["clauses"] for x in c),
+                                    default=0)
+        return ca == cb and na == nb, f"clauses or n_vars ({na} vs {nb})"
+
+    if t == "subset_sum":
+        return a["numbers"] == b["numbers"] and a["target"] == b["target"], \
+            "numbers or target differ"
+
+    if t == "tsp":
+        pa = sorted((round(x, 12), round(y, 12)) for x, y in a["points"])
+        pb = sorted((round(x, 12), round(y, 12)) for x, y in b["points"])
+        return pa == pb, "point set differs"
+
+    return False, "unknown type"
+
+
+def stress_solvers(trials, seed, verbose):
+    rng = random.Random(seed)
+    report = {"passed": 0, "failed": 0, "notes": []}
+
+    for t in range(trials):
+        n = rng.randint(4, 10)
+        schema = _rand_maxcut(n, rng.randint(0, 10**9))
+        W, names = _validate_maxcut_schema(schema)
+        r = solve_maxcut(W, names, time_limit=5.0)
+        bf, _ = brute_force_maxcut(W)
+        if r["value"] != bf:
+            report["failed"] += 1
+            report["notes"].append(f"maxcut n={n}: {r['value']} vs {bf}")
+        else:
+            report["passed"] += 1
+        if verbose:
+            print(f"    maxcut  n={n:>2}  solver={r['value']:>5}  bf={bf:>5}  "
+                  f"{'OK' if r['value']==bf else 'FAIL'}")
+
+    for t in range(trials):
+        n = rng.randint(3, 9)
+        ratio = rng.choice([3.0, 4.0, 4.26, 5.0])
+        schema = _rand_sat(n, ratio, rng.randint(0, 10**9))
+        clauses, n_vars = _validate_sat_schema(schema)
+        r = solve_sat(clauses, n_vars, time_limit=5.0)
+        bf_sat = False
+        for mask in range(1 << n_vars):
+            assign = {v + 1: bool(mask & (1 << v)) for v in range(n_vars)}
+            if verify_sat(clauses, assign):
+                bf_sat = True
+                break
+        if r["satisfiable"] != bf_sat:
+            report["failed"] += 1
+            report["notes"].append(
+                f"sat n={n}: {r['satisfiable']} vs {bf_sat}")
+        elif r["satisfiable"] and not r["verify"]:
+            report["failed"] += 1
+            report["notes"].append("sat: verify failed")
+        else:
+            report["passed"] += 1
+        if verbose:
+            print(f"    sat     n={n:>2} r={ratio:<5}  "
+                  f"solver={r['satisfiable']}  bf={bf_sat}  "
+                  f"{'OK' if r['satisfiable']==bf_sat else 'FAIL'}")
+
+    for t in range(trials):
+        n = rng.randint(4, 12)
+        schema = _rand_subset_sum(n, 30, rng.randint(0, 10**9))
+        nums, target, _ = _validate_subset_sum_schema(schema)
+        r = solve_subset_sum(nums, target)
+        bf_found = brute_force_subset_sum(nums, target) is not None
+        if r["found"] != bf_found:
+            report["failed"] += 1
+            report["notes"].append(f"ssum n={n}: {r['found']} vs {bf_found}")
+        elif r["found"] and not r["verify"]:
+            report["failed"] += 1
+            report["notes"].append("ssum: verify failed")
+        else:
+            report["passed"] += 1
+        if verbose:
+            print(f"    ssum    n={n:>2}  solver={r['found']}  "
+                  f"bf={bf_found}  "
+                  f"{'OK' if r['found']==bf_found else 'FAIL'}")
+
+    for t in range(trials):
+        n = rng.randint(4, 7)
+        schema = _rand_tsp(n, rng.randint(0, 10**9))
+        pts = _validate_tsp_schema(schema)
+        r = solve_tsp(pts, time_limit=5.0)
+        bf_cost, _ = brute_force_tsp(pts)
+        if abs(r["length"] - bf_cost) > 1e-6:
+            report["failed"] += 1
+            report["notes"].append(
+                f"tsp n={n}: {r['length']:.6f} vs {bf_cost:.6f}")
+        else:
+            report["passed"] += 1
+        if verbose:
+            print(f"    tsp     n={n:>2}  solver={r['length']:.6f}  "
+                  f"bf={bf_cost:.6f}  "
+                  f"{'OK' if abs(r['length']-bf_cost)<1e-6 else 'FAIL'}")
+
+    return report
+
+
+def stress_parsers(trials, seed, verbose):
+    rng = random.Random(seed)
+    report = {"passed": 0, "failed": 0, "notes": []}
+
+    for t in range(trials):
+        kind = rng.choice(["maxcut", "sat", "subset_sum", "tsp"])
+        if kind == "maxcut":
+            schema = _rand_maxcut(rng.randint(3, 8), rng.randint(0, 10**9))
+        elif kind == "sat":
+            schema = _rand_sat(rng.randint(3, 8),
+                               rng.choice([3.0, 4.0, 4.26]),
+                               rng.randint(0, 10**9))
+        elif kind == "subset_sum":
+            schema = _rand_subset_sum(rng.randint(3, 10), 50,
+                                      rng.randint(0, 10**9))
+        else:
+            schema = _rand_tsp(rng.randint(3, 7), rng.randint(0, 10**9))
+
+        text = schema_to_text(schema)
+        parsed = None
+        try:
+            if kind == "maxcut":
+                W, names = parse_maxcut(text)
+                parsed = {"type": "maxcut", "edges": []}
+                for i in range(len(W)):
+                    for j in range(i + 1, len(W)):
+                        if W[i][j]:
+                            parsed["edges"].append([names[i], names[j],
+                                                    W[i][j]])
+            elif kind == "sat":
+                clauses, n_vars, _ = parse_sat(text)
+                parsed = {"type": "sat", "n_vars": n_vars,
+                          "clauses": [list(c) for c in clauses]}
+            elif kind == "subset_sum":
+                nums, target, _ = parse_subset_sum(text)
+                parsed = {"type": "subset_sum", "numbers": nums,
+                          "target": target}
+            else:
+                pts = parse_tsp(text)
+                parsed = {"type": "tsp",
+                          "points": [[x, y] for x, y in pts]}
+            ok, msg = _schema_equivalent(schema, parsed)
+        except ParseError as e:
+            ok, msg = False, f"parse error: {e}"
+
+        if ok:
+            report["passed"] += 1
+        else:
+            report["failed"] += 1
+            report["notes"].append(
+                f"{kind} round-trip: {msg}\n"
+                f"      schema: {schema}\n"
+                f"      text:   {text}\n"
+                f"      parsed: {parsed}"
+            )
+        if verbose:
+            print(f"    {kind:<10} {'OK' if ok else 'FAIL'}  "
+                  f"{'' if ok else msg}")
+
+    return report
+
+
+def stress_json(trials, seed, verbose):
+    rng = random.Random(seed)
+    report = {"passed": 0, "failed": 0, "notes": []}
+
+    for t in range(trials):
+        kind = rng.choice(["maxcut", "sat", "subset_sum", "tsp"])
+        if kind == "maxcut":
+            schema = _rand_maxcut(rng.randint(3, 8), rng.randint(0, 10**9))
+        elif kind == "sat":
+            schema = _rand_sat(rng.randint(3, 8), 4.0,
+                               rng.randint(0, 10**9))
+        elif kind == "subset_sum":
+            schema = _rand_subset_sum(rng.randint(3, 10), 50,
+                                      rng.randint(0, 10**9))
+        else:
+            schema = _rand_tsp(rng.randint(3, 7), rng.randint(0, 10**9))
+
+        text = schema_to_text(schema)
+        r_json = dispatch_from_json(schema, verbose=False)
+        r_text = dispatch(text, verbose=False)
+
+        if kind == "maxcut":
+            agree = r_json["value"] == r_text["value"]
+            msg = f"values {r_json['value']} vs {r_text['value']}"
+        elif kind == "sat":
+            agree = r_json["satisfiable"] == r_text["satisfiable"]
+            msg = (f"satisfiable {r_json['satisfiable']} vs "
+                   f"{r_text['satisfiable']}")
+        elif kind == "subset_sum":
+            agree = r_json["found"] == r_text["found"]
+            msg = f"found {r_json['found']} vs {r_text['found']}"
+        else:
+            jl, tl = r_json["length"], r_text["length"]
+            if jl is None or tl is None:
+                agree = jl == tl
+            else:
+                agree = abs(jl - tl) < 1e-6
+            msg = f"length {jl} vs {tl}"
+
+        if agree and r_json.get("verify"):
+            report["passed"] += 1
+        else:
+            report["failed"] += 1
+            report["notes"].append(
+                f"{kind} json-vs-text: {msg} "
+                f"(verify={r_json.get('verify')})"
+            )
+        if verbose:
+            print(f"    {kind:<10} "
+                  f"{'OK' if (agree and r_json.get('verify')) else 'FAIL'}  "
+                  f"{msg}")
+
+    return report
+
+
+def run_stress(trials=20, seed=0, verbose=True):
+    print()
+    print("=" * 78)
+    print(f"STRESS TEST   trials per class per suite = {trials}")
+    print("=" * 78)
+
+    print()
+    print("  Suite 1: solvers vs brute force")
+    r1 = stress_solvers(trials, seed, verbose)
+    print(f"  -> passed {r1['passed']}  failed {r1['failed']}")
+    for n in r1["notes"][:10]:
+        print(f"     ! {n}")
+
+    print()
+    print("  Suite 2: schema -> text -> schema round-trip")
+    r2 = stress_parsers(trials * 2, seed + 1, verbose)
+    print(f"  -> passed {r2['passed']}  failed {r2['failed']}")
+    for n in r2["notes"][:5]:
+        print(f"     ! {n}")
+
+    print()
+    print("  Suite 3: dispatch_from_json vs dispatch")
+    r3 = stress_json(trials, seed + 2, verbose)
+    print(f"  -> passed {r3['passed']}  failed {r3['failed']}")
+    for n in r3["notes"][:5]:
+        print(f"     ! {n}")
+
+    total_pass = r1["passed"] + r2["passed"] + r3["passed"]
+    total_fail = r1["failed"] + r2["failed"] + r3["failed"]
+    print()
+    print(f"  TOTAL: passed {total_pass}  failed {total_fail}")
+    print("=" * 78)
+    return total_fail == 0
+
+
+# =============================================================================
+# DEMOS
+# =============================================================================
+
+DEMOS = [
+    ("MAX-CUT, 6 vertices, weighted",
+     "max cut on A-B:3, B-C:5, C-A:2, C-D:4, D-E:7, E-F:1, F-A:6, B-E:2"),
+    ("3-SAT, mixed variable names",
+     "sat (x1 or -x2 or x3) and (a or x2 or -x3) and (-a or b or x1)"),
+    ("SUBSET-SUM, find exact half",
+     "subset sum [3, 7, 1, 8, 2, 11, 5, 4] target 20"),
+    ("TSP, 6 cities in the plane",
+     "tsp (0,0) (10,0) (10,10) (0,10) (5,5) (2,8)"),
+]
+
+
+def run_demo():
+    print()
+    print("=" * 78)
+    print("DEMO -- one instance per problem class")
+    print("=" * 78)
+    for label, text in DEMOS:
+        print()
+        print(f"### {label}")
+        print(f"input: {text}")
+        print()
+        dispatch(text, verbose=True)
+        print()
+        print("-" * 78)
+
+
+# =============================================================================
+# CLI
+# =============================================================================
+
+BANNER = r"""
++------------------------------------------------------------------------+
+|           SOLVER-BACKED OPTIMIZATION ASSISTANT  v3                     |
+|                                                                        |
+|  NL front-end -> exact solvers -> verified answers.                    |
+|  Bench mode with analytically-known optima.                            |
+|  Cross-verifier: B&B vs independent DFS (MAX-CUT).                     |
+|                                                                        |
+|  Examples:                                                             |
+|    max cut on A-B:3, B-C:5, C-A:2                                      |
+|    sat (x1 or -x2 or x3) and (x2 or x3) and (-x1 or -x3)               |
+|    subset sum [3, 7, 1, 8, 2, 11] target 15                            |
+|    tsp (0,0) (10,0) (10,10) (0,10) (5,5)                               |
+|                                                                        |
+|  Commands:  demo, stress [N], bench, cross [sizes], help, quit         |
++------------------------------------------------------------------------+
+"""
+
+
+def _parse_sizes_arg(s):
+    return [int(x.strip()) for x in s.split(",") if x.strip()]
+
+
+def interactive():
+    print(BANNER)
+    while True:
+        try:
+            line = input("> ").strip()
+        except (EOFError, KeyboardInterrupt):
+            print()
+            break
+        if not line:
+            continue
+        low = line.lower()
+        if low in ("quit", "exit", "q"):
+            break
+        if low == "help":
+            print(BANNER)
+            continue
+        if low == "demo":
+            run_demo()
+            continue
+        if low == "bench":
+            run_bench(verbose=True)
+            continue
+        if low == "cross" or low.startswith("cross "):
+            m = re.match(r"cross\s+([\d,\s]+)$", low)
+            sizes = _parse_sizes_arg(m.group(1)) if m else None
+            run_cross(sizes=sizes, verbose=True)
+            continue
+        if low.startswith("stress"):
+            m = re.match(r"stress\s*(\d+)?", low)
+            n = int(m.group(1)) if m and m.group(1) else 20
+            run_stress(trials=n, seed=0, verbose=False)
+            continue
+        print()
+        try:
+            dispatch(line, verbose=True)
+        except Exception as e:
+            print(f"  error: {type(e).__name__}: {e}")
+        print()
+
+
+def main():
+    args = sys.argv[1:]
+    if not args:
+        interactive()
+        return
+
+    if args[0] in ("-h", "--help"):
+        print(__doc__)
+        return
+
+    if args[0] == "--demo":
+        run_demo()
+        return
+
+    if args[0] == "--bench":
+        ok = run_bench(verbose=True)
+        sys.exit(0 if ok else 1)
+
+    if args[0] == "--cross":
+        sizes = None
+        i = 1
+        while i < len(args):
+            if args[i] == "--sizes" and i + 1 < len(args):
+                sizes = _parse_sizes_arg(args[i + 1])
+                i += 2
+            else:
+                i += 1
+        ok = run_cross(sizes=sizes, verbose=True)
+        sys.exit(0 if ok else 1)
+
+    if args[0] == "--stress":
+        trials = 20
+        verbose = False
+        i = 1
+        while i < len(args):
+            if args[i] == "--trials" and i + 1 < len(args):
+                trials = int(args[i + 1])
+                i += 2
+            elif args[i] == "-v":
+                verbose = True
+                i += 1
+            else:
+                i += 1
+        ok = run_stress(trials=trials, seed=0, verbose=verbose)
+        sys.exit(0 if ok else 1)
+
+    if args[0] == "--json":
+        if len(args) < 2:
+            print("usage: --json '<schema>'")
+            sys.exit(1)
+        try:
+            schema = json.loads(args[1])
+        except json.JSONDecodeError as e:
+            print(f"invalid JSON: {e}")
+            sys.exit(1)
+        try:
+            dispatch_from_json(schema, verbose=True)
+        except ValueError as e:
+            print(f"schema error: {e}")
+            sys.exit(1)
+        return
+
+    dispatch(" ".join(args), verbose=True)
+
+
+if __name__ == "__main__":
+    main()