计算系统 | Info Church X.

#1 Complexity

Def asymptotic upper/lower bound

if when , , then g(n) is the AUB of f(n),

if when , , then g(n) is the ALB of f(n),

Def asymptotic tight bound

if , then g(n) is the ATB of f(n),

Example

Analysis of Recursion(Master Theorem)

Rmk

Rmk Master Theorem is valid only when

#2 Graph Basics

Def simple path: no identical nodes except the first&last ⇒ circle is a type of simple path

Def subgraph: some edges + all nodes of these edges. 子图中一条边的两个顶点必须也在子图中

Def weakly connected: 有向图的边都换成无向边后连通

Def strongly connected: 有向图自身任何两点间存在u→v和v→u的路径

Adjacency List

classify edges into four types: tree/forward/back/cross edge

Thm u在dfs树中的祖先，是搜索到u时栈里的节点

Thm 在无向图的dfs树中，没有cross edge

特别注意visit=1的位置。在bfs中，放入队列就需要标记为访问；但在最短路等问题中，取出队列才能标记为已访问

Topological Sort

Def DAG: acyclic directed graph

a graph may have multiple valid topological ordering

#3 Graph Algorithms

Strongly Connected Component

Def strongly connected component(SCC) maximal subgraph that is strongly connected

缩点之后变为DAG。因为如果有环则说明不是SCC。

Kosaraju’s Algorithm

Def reverse graph: reverse the direction of all edges

reverse graph has the same SCC group as the original graph

Def kernel graph: merge SCC into a single node

Thm 对图做dfs，输出后序访问序列。如果SCC1→SCC2有边（这也意味着反过来没有边）则在该序列中，SCC1最后的节点u1 在 SCC2最后的节点u2 之后。

intuition：SCC2访问完了之后u1才能从栈内弹出

pf 首先，u1（是SCC1中最早被访问的节点）被访问时，SCC只可能全部未访问或者全部已访问，证明如下

如果只访问了一部分，那么说明u2没有从栈内弹出，那么u2在dfs树上为u1的祖先，那么存在u2→u1，即SCC2→SCC1的路径，矛盾！

所以，分两类情况讨论。容易发现都满足。

基于此，算法实现如下：

Pass1: 对原图做dfs，得到post order

Pass2: 对反图做dfs，顺序按照post order从后往前。每次dfs出的块即为一个SCC

反图中SCC1←SCC2。Pass2保证了SCC1先被遍历。

Shortest Path

1）Single Source. 条件：无负环

Def relaxation: d[v]=min(d[v],d[u]+w[u→v])

我们只需要不断松弛，直到所有边都无法再松弛。

Bellman-Ford algorithm

松弛V-1次，每次都对所有边松弛一遍。由于最坏情况下最短路也只经过V-1条边。

条件：无负环

可以判断负环：如果V-1次松弛结束后仍有不等式未取等的，说明有负环

Dijkstra’s algorithm

greedy algorithm. we choose the node with currently the min dis to relax its neighbors.

条件：无负边

2）Multiple Source

Floyd-Warshall algorithm

令为除了头尾，中间节点标号均不超过k的最短距离

依次把k=1~n加入考量，

其实可以去掉上标直接在一个数组里更新

Minimum Spanning Tree(MST)

Prim’s algorithm

设当前连通点集为S，每次加入一条边权最小的、顶点分属S和V-S的边，更新点集

正确性证明：只要证明每一条加入的边都会出现在MST上

如果S和V-S之间的边e不在MST，而S和V-S又必须连通，故MST上会有另一条边e’。又，故将e’替换为e仍然为MST

Kruskal’s algorithm

将边排序，从小到大依次考量，只要两个顶点还未连结就将边加入MST

#4 Network Flow

Max-flow

Def flow network: connected, directed graph with two special vertices, Source and Sink

note: c(u,v) c(v,u) can both be positive

Def flow: f(u,v) that satisfy 1) f(u,v) ≤ c(u,v) 2) f(u,v) = -f(v,u) 3)

note: 2)规定了flow中（不是constrain）两节点连边一定只有一个是正值。这是因为如果两个都是正值，相当于单向流量（对最大流的贡献一样）。这样的规定在后面会带来方便。注意这样规定后，只有正值边是真的流量，负值边仅仅是一种表示

Def residual network

Discussion: r(v,u)=c(v,u)-f(v,u)=c(v,u)+f(u,v)。这表示如果已经从u→v流了f=f(u,v)，那么相应的v→u的最大流量就会加上f来表示有“反悔”的机会

前文2)的反对称性恰好保证了这一点

Def augmenting path: a path in residual network from s→t such that each edge r>0

Thm maxflow iff. no augmenting path in residual network

Ford-Fulkerson Algorithm

不断找augmenting path直到residual network中s无法到达t（即无法找到增广路）

，f为maxflow的数值

Edmonds-Karp Algorithm

改进F-F，每次找边数最少的增广路(bfs)。可以证明这样最多只需要VE次迭代

Dinic’s Algorithm

Def level graph: 只保留dis之差为1的边，其中dis为节点到s的最小边数

在level graph中，任意一条s→t的路径都是边数最少的

Def blocking flow: 在level graph中无法再找到增广路径

Discussion:

1)当前弧优化。如果节点v的flow已经用完或者v与u深度差不为1，下次搜索直接跳过

2)剪枝。如果在level graph中发现flow=Max，就不用再搜，直接返回

Min-cut

Def cut(S, T) s.t. ; the cost of the cut is

Note: 只计原图上S→T的流量，而不计入反向流量

Thm 对某个流f，以下3件事等价：

f是G上的最大流

剩余网络没有增广路

存在一个cut(S,T)，使cost(S,T)=|f|

proof 1⇒2：前面已经证明

2⇒3：在上s不能到达t。我们取S为所有s能到达的节点，T为剩下来的所有节点；S中所有的节点在剩余图上均不能到达T中任何一个节点。那么原图G上S→T的所有边一定都饱和了（所以才会反向从而使S无法到达T）。因此cost=|f|

3⇒1：对于一个流f，对于任意cut(S,T)，都有。因此如果满足(3)，那么f就是最大流

Corollary：如何找到min-cut。先跑出最大流，然后在最大流的剩余网络上找到s能到达的所有节点组成S，然后在原图上计算所有S→T的边的和

Variations

vertex capacity

要求一个节点也有最大流量的限制。把一个节点拆分成两个即可

bipartite matching二分图匹配

中间的边权是1或者inf都可以

flow有下界

把边权变为c(e)-l(e)。把每个节点u的入边边权之和的下界in(u)和出边边权之和的下界out(u)分到新的源漏S’T’上。这自然利用了流量非负的性质。

这样只要S’→u和u→T’是满流的，一定能把这些流量恰当地分配到各边上，即每条边加上l(e)，我们能得到一个可行流；反之如果S’T’间没法满流，则不存在可行流。

-如何得到有下界限制时的S→T的最大流？

跑完可行流之后，记录ST之间流量，删去S’T’和T→S这些附加边，然后在当前的剩余网络上跑S→T的最大流。这样的最大流叠加上之前的可行流一定是合法的最优解。

最大权闭合图

定义：子图内所有节点出边仍在该子图内，称为闭合图。最大权闭合图是闭合图中点权（有正有负）之和最大的

如果正收益，S->i(v)；如果负收益，i->T(-v)；上下级关系u->v(inf)

先假设fire掉所有正收益的人，看看要付出多少代价，对图做最小割。

如果保留S->i的边，代表fire掉i及其下属，此时必须割掉所有i的下属连到T的边，此时cost由fire负收益的下属带来；

如果不保留S->i的边，代表放弃fire掉i，此时i的下属到T的边不用割（除非ta是其他人的下属而被fire），cost由放弃fire正收益的i带来

因此总的收益就是所有正收益之和-代价的最小值

删除节点“节点最小割”

把一个节点分为两个x1和x2

S->x1(inf)；x2->T(inf)；x1->x2(v(x))表征删除点的代价

u→v的连边：u2->v1(inf)

这样保证了要经过一个节点x，就必须经过x1->x2。

#5 Tree Covering

Objection：用一些门组成的library实现某种布尔逻辑，使得总代价（门的面积）最小

Idea：把需要实现的布尔逻辑和library里的门都变成AND-NOT逻辑，即只有AND和NOT两种门。这样我们只需要在树上去匹配节点

具体而言，library中的gates只能匹配树上相同的节点；而library中的input可以在树上匹配任意节点x，如果x也是input则匹配完成，否则x还需要有一个相同的gate去匹配。

需要注意，library中的input可以随意匹配，但树上的input只能匹配input

Algorithm

Treeifying。把需要实现的逻辑和gate library都映射成AND-NOT树。如果有fan-out>1的就拆开分别处理。

Match。从根节点开始依次尝试匹配每一个library中的gate。如果所有节点都匹配上了，则把这个gate的input节点作为新的根重复匹配过程。

需要注意对称的gate只要尝试一次，非对称的gate要左右尝试两次。

Minimize cost。这个问题无后效性，所以在(2)中我们可以直接记录每个节点为根的子树的mincost，如果后续访问到直接查表即可。

其中表示第i个gate（如果能完全匹配上）的第j个input对应的树上的节点

Get covering method。在每个根节点存储给出最优解的gate即可

Complexity：，n为library大小，V为树上节点个数

#6 Linear Programming

standard form

（1） s.t.

（2） s.t.

Notes：

两种形式可以互相转换。（1）⇒（2）只要再添加一个变量，；（2）⇒（1）只需要用两个不等式

min{P}的问题只需要变成max{-P}即可

如果自变量约束是，可以把L放到中，并在max中加一常数，不改变问题的结构

如果自变量约束是，右侧不等式放在约束中即可

如果自变量没有约束，令，

在（2）中我们可以约定

综上，（1）（2）中任一形式可以表征所有的线性规划问题

简单起见，我们后面均基于（2）讨论

Def convex set:

线性规划的可行集S是凸集。

Def extreme point: a point can’t find s.t. (vertices of a convex set)

Thm If LP has optimal solutions in feasible set , then it has optimal solutions at extreme points.

Def basic solution: 的解中，对应（A的第i个列向量）均线性无关，则是一个basic solution，不为0的为基变量basic variable

Def basic feasible solution(BFS): a basic solution satisfy

显然BFS中非零分量个数≤rank(A)

Thm x is extreme point x is a BFS

暴力算法

假设A(m*n) x(n*1) b(m*1)，即有n个变量，m个约束

先求矩阵r=rank(A)，枚举所有在n列中取r列的可能性。对每一种可能，如果这些列向量线性无关，则组成，对应行的组成。

此时可知方程组有唯一解，对应的x（没有被选中的分量为0，其余同x’）是一个BFS。计算并更新答案。

Simplex Method

假设A(m*n) x(n*1) b(m*1)，即有n个变量，m个约束，n>m r=rank(A)，独立的约束只有r个

先找到一组基本可行解。找到A中线性无关的r个列向量，去掉其余列向量，解得x，其中最多有r个非零分量。设基变量为（其中可能有0）

用r个独立的约束，可以把r个基变量表达为其余n-r个变量的函数；进而可以将目标f表达为其余n-r个变量的函数

在f中找到一个非基本变量，其系数>0。尝试增加这个变量从而使得f变大。设m个约束下，最多能从0→，最紧的约束由带来。

交换和的地位，。新的r个基变量仍然可以表达为其余变量的函数，重复23过程，直到f中所有系数都小于0，此时f无法再增大

实际上，我们可以假设m=r。我们完全可以对A和b同时做线性变换，留下r个线性无关的约束，并不改变x的取值。

Tableau Form

假设当前表格满足：

(a)f表达为n-r个非基本变量的函数，因此r个对应r个基本变量

(b)r个基本变量在A中对应一个r维Identity。这是因为我们把r个基本变量表达为其余n-r个变量的函数，其系数为1

(c)基于(b)，右侧的b就是对应基本变量的值（非基本变量均=0）。r个约束分别只与一个基本变量有关。

接下来我们进行操作：

找一个，看最多能增大到多少。最多增大到，只计入的，因为负系数不构成约束——与同时增大即可。

，。具体发生了什么？

约束：

目标：

在表格上表现为，第i行乘，加到最后一行

注意的符号是相反的，所以

另外我们继续在A中进行行变换，把的那一列变成只有。这不会改变约束关系

做完12后，表格仍然满足(a)-(c)性质。

Initialization

我们怎么得到初始的BFS？（由前所述，我们只讨论Ax=b，并约定）

原问题：

我们求解一个辅助LP：

辅助LP的最优解一定是，否则表明原问题没有可行解。

而对辅助LP，初始BFS是trivial的：

注意这里基变量是x，因此需要先把目标函数中的w变成x，再进行单纯形法

Termination & Bland’s Rule

如果我们随意选择行和列，Simplex可能会死循环，因为当，LP可能在数次Pivot中始终无法进步而转圈

Bland’s Rule约定：

选择的列时，选最左边（编号最小）的

如果有多个相等，选择对应的基本变量在最左边（编号最小）的那个

在这套约定下，Simplex最多跑次

Duality

这里不能用kkt，因为kkt不考虑角点解，而LP全是角点解。但二者确实存在某种等价性

考虑原LP

我们想找到一组使得

显然这样的上界越紧越好，因此我们得到以下对偶LP

#7 Integer Linear Programming

与前面相同，问题可以表述为如下形式，只是x限制为整数

（如果b不是整数，则不能等价于Ax=b的形式，除非引入实数s）

Def LP relaxation 如果去掉整数限制，实数LP的解一定是ILP的上界

Def totally unimodular matrices全幺模矩阵(TU)：所有子方阵的行列式都是0,-1,1。自然

Col 若A是TU，则都是TU

Prop 判断TU的一个充分条件。(1)A每列最多两个非0 (2)我们可以按行分成两部分M_1,M_2，使得所有含2个非0的列j都满足

Thm 对实数LP问题，如果A是TU，，则所有BFS都是整数

Col 对实数LP问题，如果A是TU，，则所有BFS也是整数

pf 是TU，故加入松弛变量s后，

如果A不是TU怎么办？

Branch-and-bound Method(B&B)

对一个ILP问题，求解松弛LP

如果当前的松弛LP最优解是整数，则更新全局最优解，并结束

如果当前的松弛LP最优解不是整数

如果不大于当前的全局最优，则直接终止（因为松弛LP是ILP的上界）
如果大于当前的全局最优，则任选一个非整数变量，把问题分成和两个子问题，递归求解

Cutting Plane-Gomory Cuts

Idea：加入一些约束，去掉那些“更优”但不可行的分数解，这些约束成为Cutting Plane

事实上，我们不可能一下子找到所有的cutting plane，只能逐步添加。

接下来我们介绍Gomory Cuts

假设对当前ILP的松弛LP有一组解，其中一个基变量不是整数。我们添加如下约束：

该约束排除了

该约束不会排除任何整数解

对第m个约束，

而，（因为整数解）

从而

二式相减得证

这里[x]表示向下取证而非取整数，[-1/5]=-1

注意到这个约束由非基变量构成。

实际上，Branch-and-bound和cutting plain经常一起使用

#9 Binary Decision Diagram

Def BDD: 一个DAG. 每个节点对应一个变量，两个分支代表变量为0/1

Def ReducedOrderedBDD(ROBDD): 合并重复节点，将BDD化至最简，同时指定变量顺序

Simplify BDD(from BDtree)

维护一个lookup table，记录节点编号和儿子编号。先合并0和1。

依次查找节点，如果lookup table中有相同功能的节点，就将当前节点与该节点合并，否则加入table。特别的，如果两个分支到达的编号相同，则直接把儿子作为当前节点的编号

如果有多个不同的BDD，可以共用一些节点，化简方法同上

Construct BDD(from formula)

假设需要求F op G的ROBDD，并且我们已知F和G分别的ROBDD，伪代码如上。

每次提取当前变量作为根节点，按照香农展开，在F和G中将赋值为0/1（cofactoring），产生两个分支。两个分支递归求解，直到抵达最简单的表达式（）等，可以直接返回结果。

注意在所有分支中，look-up table是共用的，这样能防止冗余。

这套规则可以很容易扩展到k目运算符

Applications

Symbolic Simulation

基于一个电路，构造BDD，就等价的知道了该电路输出的表达式。

可以回答类似这样的问题：当a=0,b=1时，能不能取值令F=0？只要删去BDD中a=1,b=0的边，看是否有路径到0

Equivalance Checking

以相同顺序构造两个电路的ROBDD，如果ROBDD相同则电路等价。（等价于给电路套一个XNOR，然后验证输出恒为1）

如果有无关项怎么办？验证恒成立，其中x为取值，当x是无关项时为1

Min-cost SAT

对每个节点，取0和取1有不同的代价。寻找最小代价的SAT

假设每个节点SAT的最小代价（到“1”的最小代价）为

动态规划（或者记忆化搜索）计算，注意可能包括不止一个变量的取值，对那些没出现的变量，取其较小的代价

#10 Transition Systems

Def transition system

为状态集合，是初态的集合，为动作集合

定义转移，

为原子命题，可以理解为输出

L跟据原子命题给状态标号，

Def parallel actions

，

有两种，independent（结果与顺序无关）和dependent/competitive（结果与顺序有关）

Def predecessors & successors

successors同理

Def terminal state

Def execution fragment

Def maximal execution fragment

Def initial execution fragment

Def reachable states

Def program graph

为代码位置，为赋值动作，为初始位置集合

定义为当前变量Var的取值，为针对这组变量的一个布尔表达式

例如，

其中表示在这组取值下右式的布尔判断为True

表示动作的效果，

表示位置的转移，

表示变量初值满足的Conditions的集合

如何把Program Graph变成Transition System?

state = code location + relevant data

我们把作为状态，为变量的取值

存在当且仅当PG中存在且，它们是一一对应的

Equivalence Checking

求两个TS的乘积，只保留Act相同的→。

如果所有的bad state（输出不完全相同的态）都不可达，那么两个系统等价

#11 SAT

Def Atom原子命题：变量

Def Literal：变量或其补

Def Formula：由连接符connectives连起来的Literal/Formula

Def Connectives：

Note: 和的区别？

是需要判断是否为真的表达式；如果恒为真则可以写为

和同理

Def Interpretation：变量的一组取值

如果在这组取值下F为真，记为，否则记为

Def satisfiable（SAT）：存在； unsatisfiable（UNSAT）：不存在； valid：所有的I都满足

Thm Deduction Rules

Normal Forms

Def Negation Normal Form(NNF)

只有与或非，没有或，且“非”只出现在单个literal上

Def Disjunctive Normal Form(DNF)

where are literals

Def Conjunction Normal Form(CNF)

where are literals

Def equisatisfiability

F is SAT F’ is SAT

这不意味着！

Thm Tseitin’s Transformation

做了该变换之后，再将转化成与或非形式，就可以将任意公式转化成CNF

DPLL(CNF)

boolean constraint propagation

如果某clause只有一个literal，则将其赋值为1

pure literal propagation

如果某个literal没有“非”项，则将其赋值为1

如果以上两个步骤均无法进行，则尝试给一个literal赋值进行搜索

CDCL(CNF)

如何从conflict中学到东西？

each variable is either manual decided, or implied by other variables

Def implication graph

变量右上角表示其值的来源

在第二层我们得到了一个矛盾

Def conflict cut

把手动赋值的放在一边，冲突放在另一边

边界上的变量就是导致冲突的原因，将学习到的新clause加入SAT，然后回溯到该clause中第二大的level（这样才能使得它不冲突）

我们应该怎么切割（学习哪个clause）？

unique implication point

在implication point中的一个点，从最后一个manually decided节点到冲突的任意路径必须经过它

离冲突最近的UIP称为first UIP。一种启发式算法就是在first UIP之后做cut。

作如图切割后，我们学习到：，然后跳转到第0层

一般而言，这种切割方法能得到比较简短的clause

2-SAT

Def 每个clause只有两个literals

Thm

我们可以用图来表示”→”的关系

我们关心和的推断关系。如果二者能互相推出，就意味着，即SAT问题无法被满足。而二者能互相推出，等价于二者能互相到达，等价于二者在同一个SCC中。

因此我们只需要对implication graph作SCC，然后看是否出现以上情况就可以

#12 SMT

First-Order Logic(FOL)

账号

vscode左侧的remote

0037 xty+birth

cd ./workspace/sv-sampler-lab