笔记：ABC 中 AIG rewriting 在做什么

来源

• Berkeley ABC 文档与源码中 rewriting / refactoring 相关通道路径
• 经典 AIG rewriting 文献（笔记级摘要，非逐句翻译）

问题意识

组合逻辑优化常在 And-Inverter Graph 上做局部改写：用更小或更深更优的子图替换等价锥，同时尽量保持功能等价。

要点

1. 局部窗口：选取根节点与若干层扇入，枚举或启发式搜索候选替换结构。
2. 代价函数：节点数、逻辑级、后续映射友好度；AI4EDA 可把代价预测器换成学习模型，但替换仍需等价。
3. 等价保证：结构性改写通常依赖预先证明的库或在线等价检查；不能只信评分网络。

与形式化的接口

• 改写前后锥：miter + SAT 是常用闭环。
• 学习型提议器输出「候选子图」时，SAT/BDD 不通过则丢弃，不进入提交集合。

待跟进

• 对照一篇具体 rewriting 论文的实验设置，补表格
• 在笔记中链到本站 /github 里 ABC 相关收藏（若收录）

疑问

在含 don’t-care 的外部条件时，局部等价是否应放宽为「在关心集合上等价」？若放宽，如何把关心集合编码进 miter？

← 返回 Notes