BDD
BDD: 二叉判定圖（二分決策圖）
1.A new dynamic heuristic binary decision diagram ( BDD ) minimization algorithm is proposed.
提出了一種新的動(dòng)態(tài)啟發(fā)式二叉判定圖 ( BDD ) 最小化算法.
2.Ordered Binary Decision Diagram ( OBDD ) is one of the most efficient tools for computing network reliability.
有序二分決策圖 ( OBDD ) 是計(jì)算網(wǎng)絡(luò)可靠度最有效的工具之一.
wiki上的解釋：
https://en.wikipedia.org/wiki/Binary_decision_diagram
BDD是一種表達(dá)布爾函數(shù)的數(shù)據(jù)結(jié)構(gòu)温艇。在更抽象的層面上肆捕，BDD可以被看作是集合或關(guān)系的壓縮表示悬垃。與其他壓縮表示不同，操作直接在壓縮表示上執(zhí)行，即不進(jìn)行解壓縮。用于表示布爾函數(shù)的其他數(shù)據(jù)結(jié)構(gòu)包括否定范式egation normal form(NNF)和命題有向無環(huán)圖propositional directed acyclic graph(PDAG)。
定義：
布爾函數(shù)可以表示為根墓塌、有向、無圈圖奥额，該圖由多個(gè)決策節(jié)點(diǎn)和終端節(jié)點(diǎn)組成苫幢。有兩種類型的終端節(jié)點(diǎn)稱為0終端和1終端.
如果對BDD的圖應(yīng)用了以下兩條規(guī)則，則BDD被稱為“約簡”：
- 合并任何同構(gòu)子圖垫挨。
- 消除其兩個(gè)子為同構(gòu)的任何節(jié)點(diǎn)韩肝。
關(guān)于建立BDD
PROST planner在他的工程文件中找不到如何建立BDD的，他使用了一個(gè)開源的BDD包九榔，建立BDD哀峻。
Libraries: BuDDy (http://sourceforge.net/projects/buddy/)
A Binary Decision Diagram library, with :
many highly efficient vectorized BDD operations,
dynamic variable reordering,
automated garbage collection,
a C++ interface with automatic reference counting,
and much more.
Java版本的BDD-JavaBDD
http://javabdd.sourceforge.net/
JavaBDD is a Java library for manipulating BDDs (Binary Decision Diagrams). Binary decision diagrams are widely used in model checking, formal verification, optimizing circuit diagrams, etc. For an excellent overview of the BDD data structure, see this set of lecture notes by Henrik Reif Andersen.
課程的講義已經(jīng)找不到了。
http://javabdd.sourceforge.net/performance.html
javabdd的表現(xiàn)略差于BuDDy哲泊。這個(gè)javabadd就是根據(jù)BuDDy直接從C代碼翻譯過來的剩蟀。沒有進(jìn)行優(yōu)化，所以表現(xiàn)上略差切威。
我想還是能用上的育特。
為什么BDD可以用來檢測Reward lock?
這個(gè)問題我沒想清楚。
三值邏輯
https://zh.wikipedia.org/wiki/%E4%B8%89%E5%80%BC%E9%80%BB%E8%BE%91
https://en.wikipedia.org/wiki/Three-valued_logic
Kleene代數(shù)和論文中用的沒什么關(guān)系
https://en.wikipedia.org/wiki/Kleene_algebra
SLURM linux集群控制
SLURM
Slurm is an open source, fault-tolerant, and highly scalable cluster management and job scheduling system for large and small Linux clusters. Slurm requires no kernel modifications for its operation and is relatively self-contained. As a cluster workload manager, Slurm has three key functions. First, it allocates exclusive and/or non-exclusive access to resources (compute nodes) to users for some duration of time so they can perform work. Second, it provides a framework for starting, executing, and monitoring work (normally a parallel job) on the set of allocated nodes. Finally, it arbitrates contention for resources by managing a queue of pending work.
Available options are "slurm" and "sge" (for sun grid engine)
grid_engine = "slurm"
grid_engine = "sge"
Keller experiment.py use linux clusters for his experiments.
等我需要對比PROST的表現(xiàn)時(shí)先朦，就需要用到linux集群控制了缰冤。
