有序二叉決策圖及應用

前言
第1章 布爾表達式及其描述
1．1 布爾函數
1．1．1 布爾代數
1．1．2 布爾表達式
1．1．3 布爾函數
1．1．4 布爾函數的范式
1．2 命題公式
1．2．1 命題與聯結詞
1．2．2 合式公式
1．2．3 命題公式的范式
1．2．4 命題公式與布爾函數
1．3 邏輯電路
1．3．1 基本邏輯門
1．3．2 邏輯電路的布爾函數
1．4 布爾表達式的其他描述形式
1．4．1 真值表
1．4．2 決策樹
1．4．3 二叉決策圖
參考文獻
第2章 有序二叉決策圖
2．1 OBDD及其規(guī)范型
2．1．1 OBDD的定義
2．1．2 OBDD的性質
2．2 OBDD的簡化算法
2．2．1 OBDD的簡化
2．2．2 簡化算法
2．3 OBDD的構造及操作
2．3．1 OBDD的構造
2．3．2 OBDD的操作
2．3．3 補邊OBDD
2．4 OBDD的變量序
2．4．1 OBDD的最小化
2．4．2 OBDD的重排序
2．4．3 OBDD的變量序算法
參考文獻
第3章 零壓縮二叉決策圖
3．1 ZBDD及其性質
3．1．1 組合集合及其表示
3．1．2 ZBDD的定義
3．1．3 ZBDD的性質
3．2 ZBDD的構造及基本操作
3．2．1 ZBDD的操作
3．2．2 ZBDD的構造
3．2．3 補邊ZBDD
3．3 一元Cube集合代數
3．3．1 基本概念
3．3．2 基本運算
3．3．3 算法實現
3．3．4 皇后問題的求解
3．4 二元Cube集合代數
3．4．1 二元Cube集的表示
3．4．2 基本操作及算法
3．4．3 數字電路設計
3．5 多項式的隱式表示
3．5．1 變量次數的表示
3．5．2 多項式系數的表示
3．5．3 算術操作的算法實現
參考文獻
第4章 代數決策圖
4．1 ADD及其性質
4．1．1 ADD的定義
4．1．2 ADD的矩陣表示
4．2 ADD基本操作
4．2．1 布爾操作
4．2．2 算術操作
4．2．3 提取操作
4．3 矩陣乘法計算
4．3．1 準環(huán)和半環(huán)
4．3．2 半環(huán)上的矩陣乘算法
4．3．3 準環(huán)上的矩陣乘算法
參考文獻
第5章 邊值二叉決策圖
5．1 EVBDD及其性質
5．1．1 EVBDD的定義
5．1．2 EVBDD的規(guī)范性
5．2 操作及其算法
5．2．1 Apply操作
5．2．2 操作的性質
5．3 整數線性規(guī)劃求解
5．3．1 0—1整數規(guī)劃求解算法
5．3．2 改進算法
5．3．3 minimize函數
5．4 函數分解
5．4．1 函數分解的定義
5．4．2 無交集函數分解
參考文獻
第6章 二叉矩量圖
6．1 BMD定義及性質
6．1．1 函數分解規(guī)則
6．1．2 BMD的定義
6．1．3 BMD的規(guī)范性
6．1．4 *BMD的定義
6．1．5 *BMD的構造算法
6．2 *BMD的操作算法
6．2．1 整數函數的表示
6．2．2 *BMD的加法操作
6．2．3 *BMD的乘法和冪操作
6．2．4 布爾函數的表示及操作
6．2．5 仿射置換
6．3 算術電路驗證
參考文獻
第7章 時間變量決策圖
7．1 差分約束
7．1．1 差分約束表達式
7．1 _2差分約束系統(tǒng)
7．2 差分決策圖
7．2．1 有序差分決策圖
7．2．2 局部簡化DDD
7．2．3 路徑簡化DDD
7．2．4 完全簡化DDD
7．3 DDD的構造及操作
7．3．1 DDD的構造
7．3．2 RDDD上的操作
7．4 賦時二叉決策圖
7．4．1 賦時布爾函數
7．4．2 賦時布爾函數BDD
7．4．3 賦時二叉決策圖
參考文獻
第8章 應用專題
8．1 符號模型檢驗
8．1．1 計算樹邏輯
8．1．2 CTL的模型檢驗
8．1．3 CTL的符號模型檢驗
8．2 網絡優(yōu)化
8．2．1 網絡最大流問題
8．2．2 0—1網絡最大流問題的符號算法
8．2．3 最大流問題的符號算法
8．3 裝配序列規(guī)劃
8．3．1 裝配序列的符號表示
8．3．2 裝配序列的符號生成
8．3．3 基于MIPs的裝配序列生成
8．4 Petri網分析
8．4．1 基于OBDD的符號分析
8．4．2 Petri網調度的符號算法
參考文獻