Property-Directed Reachability / IC3

Frame 序列不变量 ​

对布尔转移系统 $I(x),T(x,x^{\prime })$ 和安全性质 $P(x)$，PDR 维护公式序列

$$F_0,F_1,\dots ,F_k$$

满足

$$F_0=I,F_i\Rightarrow P,F_i\Rightarrow F_{i+1},F_i(x)\wedge T(x,x^{\prime })\Rightarrow F_{i+1}(x^{\prime }).$$

$F_i$ 过近似至多 $i$ 步可达状态。序列随下标变弱，允许状态增加；每个 frame 内不断学习子句，公式则变强。

若某相邻层语义相等 $F_i=F_{i+1}$，相对归纳条件给出

$$F_i\wedge T\Rightarrow F_i^{\prime },$$

加上 $I\Rightarrow F_i$ 与 $F_i\Rightarrow P$，得到归纳不变式公理库不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。，证明安全。

从坏状态建立 obligation ​

算法先询问可满足性公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。

$$F_k(x)\wedge T(x,x^{\prime })\wedge \mathrm{\neg }P(x^{\prime }).$$

若 SAT，得到一个可能一步进入坏状态的 predecessor cube $c$，形成层 $k$ 的 proof obligation $(c,k)$。算法递归检查 $c$ 是否从 $F_{k-1}$ 有前驱。

若 obligation 一直追到层 $0$ 并与初态相交，沿保存的 SAT 模型反向连接，就得到真实反例路径。若某层前驱查询 UNSAT，则当前 cube 在该层不可到达，可以学习阻塞子句。

这不是普通反向 BFS：frame 是可达集的逻辑外包络，obligation 是具体或部分状态 cube，SAT 求解器隐式处理大量状态。

子句泛化与阻塞 ​

设当前待阻塞义务为 $(c,i)$，其中 $c(x)$ 描述第 $i$ 层要排除的状态集合。算法查询

$$F_{i-1}(x)\wedge T(x,x^{\prime })\wedge c(x^{\prime })$$

若查询 SAT，模型在当前状态变量 $x$ 上给出前驱 cube $p(x)$；算法先递归阻塞 $(p,i-1)$，成功后再处理原义务 $(c,i)$。若查询 UNSAT，则 $c$ 没有来自 $F_{i-1}$ 的前驱。此时可把 $c$ 泛化为文字更少的 cube $g\subseteq c$，但必须重新验证

$$F_{i-1}(x)\wedge T(x,x^{\prime })\Rightarrow \mathrm{\neg }g(x^{\prime }).$$

验证通过后，把子句 $\mathrm{\neg }g$ 加入 $F_1,\dots ,F_i$；这既阻塞当前后继 cube，也保持 $F_j\Rightarrow F_{j+1}$ 的层间关系。全文中 $c$ 始终表示当前待阻塞的后继，$p$ 只表示 SAT 查询返回的前驱。

SAT 求解器的 unsat core 可帮助删除 cube 中不必要的文字，得到更一般的阻塞子句，一次排除更多状态。泛化必须重新验证相对归纳查询；凭启发式删文字可能连真实可达状态一起排除。

例如 cube 指定十个变量，core 只依赖锁位和两个程序计数器，学到的子句便覆盖所有其他变量赋值。这是 PDR 不逐状态枚举的关键来源。

推送与收敛 ​

若子句 $c\in F_i$ 满足

$$F_i(x)\wedge T(x,x^{\prime })\Rightarrow c(x^{\prime }),$$

它可推送到 $F_{i+1}$。算法周期性尝试推送全部子句；当一层所有约束都能推到下一层且两层相同，获得固定点。

有限布尔状态系统上，理想化 IC3 过程完备：最终找到反例或归纳不变式。实际性能高度依赖 obligation 顺序、generalization、clause subsumption 与 SAT 增量接口。

“frame 数不再增加”不等于收敛；必须检查某对相邻 frame 公式语义等价或子句集合在规范管理下相同。

与 BMC 的差别 ​

BMC 前向展开固定长度路径，UNSAT 通常只有边界意义。PDR 的查询围绕归纳阻塞，目标是主动合成一个全局不变式；它也会生成反例，但不是“更快的 BMC”同义词。

PDR 对 safety/reachability 最自然。一般 LTL 需先做监控器或自动机产品转成安全/接受问题，公平 liveness 不能直接套原始 frame 不变量。

无限状态 SMT-PDR 可能不终止，量词和理论泛化也可能不完备。有限布尔模型上的保证不能无条件推广到软件整数与堆。

一个阻塞子句例子 ​

设安全性质禁止 $pc=C\wedge lock=0$。SAT 查询发现抽象 cube 还包含无关数据位 $d_1,d_2$。检查前驱后，unsat core 表明只需 $pc=C\wedge lock=0$ 就不可从上一 frame 到达，于是学习

$$pc\ne C\vee lock=1.$$

这条子句同时阻塞所有数据位组合，比逐一排除完整 cube 更强。若 core 还依赖上一层特有子句，它只相对于该 frame 归纳，不能直接提升到所有层。

子句管理还要做 subsumption：强子句可删除被其蕴含的弱子句，但反向删除会扩大 frame 并可能重新引入坏状态。语法文字数少不自动代表逻辑更强。

参考资料

• Aaron R. Bradley, “SAT-Based Model Checking without Unrolling,” VMCAI, 2011, pp. 70–87。
• Niklas Eén, Alan Mishchenko, and Robert Brayton, “Efficient Implementation of Property Directed Reachability,” FMCAD, 2011, pp. 125–134。
• Aaron R. Bradley and Zohar Manna, The Calculus of Computation, Springer, 2007, Chs. 12–14。