[INFO] CDCL 与 SMT 的层级澄清 + 学过未沉淀的元观察

时间: 2026-05-15
类型: 观察
来源: 与 Jane 的讨论（基于 INFO-036/037/039 的回顾）
置信度: 9/10
标签: #SAT #SMT #CDCL #DPLL #形式化方法 #元认知 #学过未沉淀

一、技术核心：CDCL 和 SMT 不在同一层级

常见混淆

把 CDCL 和 SMT 当成同级概念对比——错位。

正确的层级关系

	问题类（要解决什么）	算法/框架（怎么解）
纯布尔	SAT	CDCL
含理论	SMT	DPLL(T) / CDCL(T)

✅ SAT vs SMT：两个问题类对比
✅ CDCL vs DPLL(T)：两个算法框架对比
❌ CDCL vs SMT：错位（算法 vs 问题）

包含关系

SMT 求解器（如 Z3）
   ├── SAT 内核（用 CDCL 算法）        ← 处理布尔结构
   └── 理论求解器（T-solver）         ← 处理 x+y>5 这种
        ├── 线性算术求解器
        ├── 数组理论求解器
        └── ...
   通过 DPLL(T) 框架协作

CDCL 是 SMT 求解器的内核组件之一，不是替代关系，是包含关系。

一个好记的类比

CDCL ≈ "算盘的拨珠规则"（具体计算方法）
SAT ≈ "加减乘除"（一类问题）
SMT ≈ "工程数学问题"（更广的问题）
SMT 求解器（Z3）≈ "工程计算器"（装了算盘 + 各种专用电路）

二、元层观察：「读过但没刻进去」

现象

知识库里 SAT/SMT 主题的三条 INFO 都是 2024-12-19 同一天录入：

INFO-036：SAT/SMT 在 AI Agent 里的应用架构
INFO-037：CDCL / DPLL(T) 算法详解
INFO-039：SAT 用于规则一致性验证

典型的"打包学习"产物——一波读完、整理成高密度笔记、置信度 8-9/10。

但是

17 个月里：

没产出 RULE
没建 NODE
三条"待验证"字段全挂着没动
今天再被问"CDCL 和 SMT 的区别"——说明层级感没真正沉淀

INFO-037 当时其实把层级关系写得很清楚（表格分了"问题类"和"算法框架"两列）。整理过 ≠ 内化。

反模式命名

"读过但没刻进去"——这是个值得在未来观察的反模式。可能的演化方向：

多观察几次 → 提炼为 RULE-学完即试或 RULE-避免打包学习
现在记为 INFO，不预设结论

三、概念真正刻进去的方法

继续读理论不会让概念分清，动手 10 行 Z3 代码会：

from z3 import *

# SAT 问题（CDCL 解）—— 纯布尔
A, B, C = Bools('A B C')
s = Solver()
s.add(Or(A, Not(B)), Or(Not(A), C))
print(s.check())   # sat
print(s.model())   # 如 [A=True, B=False, C=True]

# SMT 问题（DPLL(T) 解）—— 含理论
x, y = Reals('x y')
s = Solver()
s.add(x + y > 5, x - y < 1, x > 0)
print(s.check())   # sat
print(s.model())   # 如 [x=3, y=3]

亲眼看到同一个 Solver() 在两种问题上分别用了不同内核机制——比读 100 遍文章都清楚。

呼应 INFO-095（逻辑链+落地行为）："落地行为是思维的动态试炼"。

四、待验证字段的诊断

三条原始 INFO 的"待验证"全部挂着 17 个月：

INFO	待验证项	状态
INFO-036	在 Janus 日程冲突检测中应用 SMT	17 个月未动
INFO-037	使用 Z3 实现 Janus 日程冲突检测	17 个月未动
INFO-039	规则健康度评估指标的实际有效性	17 个月未动

Janus 已不在主区（产品应用层在 2026-05 已隔离）。但 SAT/SMT 的认知应用还在——最值得做的不是再找新产品场景，是用 Z3 验证自己的 38 条 RULE 一致性。

这正好是 INFO-039 整篇文章的主旨被"重新瞄准目标"——从邮件规则系统转向 Robert 自己的认知规则系统。

五、新的"待验证"

替换上述三条已不可执行的待验证项：

用 Z3 写 5-10 条核心 RULE 的形式化表达 + 一致性检查
目标：这是 17 个月里第一次把 SAT/SMT 从笔记变成跑通的代码
应用 INFO-058 的"1cm 问题法"——不追求完整 RULE 引擎，只求最小可跑

关联

相关: INFO-20251219-036（SAT/SMT 应用架构）
相关: INFO-20251219-037（CDCL/DPLL(T) 算法详解——本条澄清的素材源头）
相关: INFO-20251219-039（SAT 规则一致性验证——可重新瞄准到自己 RULE 体系）
相关: INFO-20251219-058（1cm 问题法 / 跌撞前行）
相关: INFO-20251219-095（逻辑链 + 落地行为——"落地行为是思维的动态试炼"）
相关: INFO-20260115-118（认知系统五大盲区——"反例字段大多空着"是典型反例的同源问题）
触发规则: -
待验证: 用 Z3 写 5-10 条 RULE 的形式化表达 + 一致性检查