有序二叉決策圖及應(yīng)用

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