BDD
BDD: 二叉判定图（二分决策图）
1.A new dynamic heuristic binary decision diagram ( BDD ) minimization algorithm is proposed.
提出了一种新的动态启发式二叉判定图 ( BDD ) 最小化算法.
2.Ordered Binary Decision Diagram ( OBDD ) is one of the most efficient tools for computing network reliability.
有序二分决策图 ( OBDD ) 是计算网络可靠度最有效的工具之一.
wiki上的解释：
https://en.wikipedia.org/wiki/Binary_decision_diagram
BDD是一种表达布尔函数的数据结构。在更抽象的层面上，BDD可以被看作是集合或关系的压缩表示。与其他压缩表示不同，操作直接在压缩表示上执行，即不进行解压缩。用于表示布尔函数的其他数据结构包括否定范式egation normal form(NNF)和命题有向无环图propositional directed acyclic graph(PDAG)。
定义：
布尔函数可以表示为根、有向、无圈图，该图由多个决策节点和终端节点组成。有两种类型的终端节点称为0终端和1终端.
如果对BDD的图应用了以下两条规则，则BDD被称为“约简”：
- 合并任何同构子图。
- 消除其两个子为同构的任何节点。
关于建立BDD
PROST planner在他的工程文件中找不到如何建立BDD的，他使用了一个开源的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.
课程的讲义已经找不到了。
http://javabdd.sourceforge.net/performance.html
javabdd的表现略差于BuDDy。这个javabadd就是根据BuDDy直接从C代码翻译过来的。没有进行优化，所以表现上略差。
我想还是能用上的。
为什么BDD可以用来检测Reward lock?
这个问题我没想清楚。
三值逻辑
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代数和论文中用的没什么关系
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的表现时，就需要用到linux集群控制了。
