| 提要 | 第1-5页 |
| 摘要 | 第5-7页 |
| Abstract | 第7-12页 |
| 第1章 绪论 | 第12-24页 |
| ·研究背景和意义 | 第12-13页 |
| ·命题知识表示与推理 | 第13-16页 |
| ·命题逻辑相关概念 | 第13-14页 |
| ·命题推理问题 | 第14-16页 |
| ·命题公式的转化操作 | 第16页 |
| ·知识编译相关工作介绍 | 第16-22页 |
| ·知识编译方法的基本思想 | 第16-17页 |
| ·相关的命题目标语言介绍 | 第17-19页 |
| ·目标语言的评估方法 | 第19-21页 |
| ·知识编译与SAT求解之间的关系 | 第21-22页 |
| ·本文工作 | 第22-24页 |
| 第2章 带蕴含文字的有序二元决策图的定义 | 第24-32页 |
| ·基本动机 | 第24页 |
| ·BDD‐L的定义 | 第24-27页 |
| ·OBDD‐L的定义 | 第27-29页 |
| ·ROBDD‐L的定义 | 第29页 |
| ·OBDD‐LI与ROBDD‐LI的定义 | 第29-30页 |
| ·本章小结 | 第30-32页 |
| 第3章 OBDD‐L子集的完备性与规范性 | 第32-38页 |
| ·ROBDD‐LI的完备性与规范性 | 第32-34页 |
| ·线性时间的精简化 | 第34-36页 |
| ·本章小结 | 第36-38页 |
| 第4章 OBDD‐L及其子集的简洁性 | 第38-50页 |
| ·OBDD‐L中各个子集之间的简洁性比较 | 第38-48页 |
| ·OBDD‐L与其他语言的简洁性比较 | 第48-49页 |
| ·本章小结 | 第49-50页 |
| 第5章 OBDD‐L及其子集支持的逻辑操作 | 第50-86页 |
| ·OBDD‐L及其子集支持的多项式时间的操作算法 | 第50-67页 |
| ·一致性检测 | 第50页 |
| ·有效性检测 | 第50-52页 |
| ·蕴含子句判定 | 第52-54页 |
| ·判定被项蕴含 | 第54-55页 |
| ·模型计数 | 第55-56页 |
| ·模型枚举 | 第56-57页 |
| ·等价性判定 | 第57-58页 |
| ·调整 | 第58-60页 |
| ·计算最小度 | 第60-61页 |
| ·最小化 | 第61-63页 |
| ·OBDD‐L0支持的布尔操作 | 第63-64页 |
| ·单变量忽略 | 第64-67页 |
| ·OBDD‐L及其子集的易处理性评估 | 第67-72页 |
| ·一种新的处理ROBDD‐L_∞操作的思路 | 第72-77页 |
| ·一个ROBDD‐L_∞的合取算法 | 第77-84页 |
| ·本章小结 | 第84-86页 |
| 第6章 OBDD‐L子集的编译算法 | 第86-94页 |
| ·编译算法Build | 第86-88页 |
| ·编译算法BuildInfty | 第88-90页 |
| ·Build和BuildInfty中可使用的优化技术 | 第90-93页 |
| ·本章小结 | 第93-94页 |
| 第7章 实验结果 | 第94-100页 |
| 第8章 结论与展望 | 第100-104页 |
| ·本文工作总结 | 第100-101页 |
| ·进一步工作展望 | 第101-104页 |
| 参考文献 | 第104-110页 |
| 作者简介及在学期间所取得的科研成果 | 第110-112页 |
| 致谢 | 第112页 |