cognitive-anchor：把结论钉死在硬约束上

分工：cognitive-core 负责拆问题、定框架；cognitive-anchor 负责把判据符号化，用求解器硬算结论。 anchor 的输出不允许 LLM 自由发挥——这正是防摇摆的架构保证。

什么时候用

• 有 ≥3 个 0/1 判据（可行性、预算、时间、风险……）同时起作用
• 用户反复改条件、结论一直摇摆，需要稳定答案
• 需要每个结论都可回放、可复核（推理链可复现）
• 需要多轮对齐：每轮新增信息，检查推荐档是否变化
• 需要"博弈分支表"：把所有可能组合按优先级列出

工作流（六步）

1. 拆判据：把用户的话翻译成 0/1 变量，格式 变量:含义。例：x:可行性,y:预算充足,z:时间允许,w:风险可控
2. 写约束：把条件转成硬约束（分号分隔的 z3 表达式）。语法见 references/format.md
3. 定档位：把候选决策写成互斥谓词，如 做:x+y+z+w>=4; 观望:x+y+z+w==3; 不做:x+y+z+w<3
4. 求解：运行脚本（见下）
5. 读结果：看 解总数 / 档位票数 / 变量频率 / 分支表 / 推荐档；留意 [警告] 行（截断、未覆盖、无解）
6. 多轮对齐：用户新增信息 → 追加约束重解 → 对比推荐；档位变了就提示"标准未稳，先别下最终结论"

脚本

python3 scripts/solve.py \
  --declare "x:可行性,y:预算充足,z:时间允许,w:风险可控" \
  --constraints "x+y+z+w>=3; Implies(y==0,w==1); Implies(z==0,And(x==1,w==1))" \
  --decisions "做:x+y+z+w>=4; 观望:x+y+z+w==3; 不做:x+y+z+w<3" \
  --rounds "|y==0" \
  --max-solutions 100

• --rounds：多轮对齐。段数=轮数，第 1 段通常留空（只用基础约束）；"|y==0" = 第二轮追加预算紧张；"| |z==0" = 第三轮追加（第二轮不追加）
• --as-json：输出 JSON（含 schema_version 与 warnings，供下游技能/脚本解析）
• --selftest：跑内置验收（18 项 PASS/FAIL 断言，覆盖沙箱逃逸、全角输入、截断、无解、rounds 语义等），改脚本后必须重跑
• --version：查看脚本版本

输入容错（v2.0）：全角标点（：，；｜（））自动归一化，用户口语化粘贴的符号化文本无需手动转换。

依赖：z3-solver（pip install z3-solver）。脚本在无 z3 环境会报 ImportError，先装依赖。

硬规则

1. 最终结论必须来自 solve.py 输出，agent 不得自行下最终判断（只能解释结果）
2. 每轮输出必须保留：解总数 + 各档票数（可复核）
3. 档位谓词必须互斥（区间划分）；并列票数时用分支表优先序裁决并在回复中说明
4. 变量/约束/档位写好后，把"人话 ↔ 符号"的翻译过程讲给用户听（透明可校验）
5. 档位漂移时明确提示，不掩盖
6. [v2.0] 出现 [警告] 必须转告用户：截断（解空间过大只统计前 N 个）、未覆盖（有解没命中任何档）、无解（约束矛盾）——不许悄悄忽略
7. [v2.0] 表达式只走脚本白名单：agent 不得为了绕过报错而拼接属性访问、Lambda 等构造（脚本会拒绝）；写不出来就拆成多条简单约束

输出格式（给用户）

【决策问题】一句话
【符号化】变量含义 + 硬约束（人话版）
【求解结果】第N轮：满足解 X 个；档位票数：做=a 观望=b 不做=c → 推荐「档位」
【分支表】按优先级前几条
【收敛状态】两轮一致=已收敛 / 不一致=标准未稳

无解轮次时，【求解结果】改为说明"约束矛盾"并给出脚本输出的放宽建议，不得硬给推荐。

扩展点（当前未实现，如实说明）

• 多模态→符号：图片/图表/视频先由 agent 用视觉/文档技能提取结构化事实，再翻译成变量约束；翻译层当前是 agent 手写，未接视觉模型
• 概率加权博弈树剪枝：当前是全枚举（确定逻辑）；要做概率加权，用变量频率作先验、加权重排序，参考 GenGamer 论文思路自行扩展
• 外部记忆：当前多轮对齐仅在单次调用内累积约束；跨会话记忆未实现

验收

python3 scripts/solve.py --selftest 全 PASS 即通过。v2.0 覆盖：有解、推荐正确、多轮收敛、分支表有序、截断标志、全角归一化、rounds 位置语义、无解引导、Distinct 档位可用、沙箱逃逸拒绝（属性访问 / MRO 遍历 / Lambda）、未声明变量拒绝。