MILP 与 SMT

MILP

LP (Linear Programming): 线性规划, 变量连续取值.
IP (Integer Programming): 整数规划. 全部变量为 0-1 时, 是其中的 0-1 IP.
MILP (Mixed-Integer Linear Programming): 混合整数线性规划, 可以同时包含整数变量和连续变量.

找到好解与证明最优

以最小化问题为例:

Incumbent (UB): 目前找到的最好方案, 其目标值提供上界. 例如 $\mathrm{OPT}\leq 10$ .
Best Bound (LB): 已经证明的下界. 例如 $\mathrm{OPT}\geq 8$ .
Optimality Gap: 目前未消除的最优性不确定范围. 这里的绝对 gap 为 $UB-LB=2$ .

找到好解和证明它最优, 是两件事.

LP Relaxation 与剪枝

LP Relaxation: 去掉整数限制, 同时保留原目标和其余约束. 例如将 $x\in\{0,1\}$ 放松为 $0\leq x\leq 1$ .

可行域扩大, 因而对最小化问题可以提供下界:

\mathrm{OPT}_{\mathrm{LP}}\leq\mathrm{OPT}_{\mathrm{IP}}.

求解器 Pruning: 若某个 branch 的下界已经不小于 incumbent 的目标值 $UB$ , 就不能找到更好的解, 可以剪枝.

将逻辑写成 MILP

令 $a,b,z\in\{0,1\}$ .

1. 蕴含

a\Rightarrow b\quad\Longleftrightarrow\quad a\leq b.

它禁止 $a=1\land b=0$ . 例如 $\mathrm{send}\leq\mathrm{has}$ , 表示不能发送自己没有的数据.

2. AND

z=a\land b \quad\Longleftrightarrow\quad \begin{cases} z\leq a,\\ z\leq b,\\ z\geq a+b-1. \end{cases}

3. OR

z=a\lor b \quad\Longleftrightarrow\quad \begin{cases} z\geq a,\\ z\geq b,\\ z\leq a+b. \end{cases}

Big-M 理论

用足够大的 $M$ , 让某条约束在不需要时自动失效.

例如, 两个操作不能重叠, 开始时间为 $s_1,s_2$ , 持续时间为 $d_1,d_2$ :

(s_2\geq s_1+d_1)\lor(s_1\geq s_2+d_2).

引入 $z\in\{0,1\}$ , 写成:

\begin{cases} s_2\geq s_1+d_1-M(1-z),\\ s_1\geq s_2+d_2-Mz. \end{cases}

$z=1$ : 操作 1 在操作 2 前面.
$z=0$ : 操作 2 在操作 1 前面.

$M$ 的大小需要注意:

$M$ 太小: 可能删掉合法解.
$M$ 太大: LP 松弛可能变弱, 影响求解效率, 也可能带来数值问题.

可以考虑用合法的完工时间上界 $U$ 作为 $M$ . 这里要求 $s_i\geq 0$ 且 $s_i+d_i\leq U$ , 这样未选中的约束就能被放松.

形式化定义 AllGather 问题

设 $H$ 是时间步数, $E$ 是有向链路集合, $(u,v)\in E$ .

$h[k,v,t]$ : chunk $k$ 在时间点 $t$ 是否存在于节点 $v$ 上.
$s[k,u,v,t]$ : 在 $[t,t+1)$ 这个 step 上, 是否从 $u$ 向 $v$ 发送 chunk $k$ .
$h[\cdots],s[\cdots]\in\{0,1\}$ .

传输在下一时间点完成: 第 $t$ 步收到的数据, 从 $t+1$ 起可以使用.

初始态与终态

chunk $k$ 最初属于节点 $r(k)$ :

h[k,v,0]= \begin{cases} 1,&v=r(k),\\ 0,&v\neq r(k). \end{cases}

结束时, 每个节点拥有每个 chunk:

h[k,v,H]=1,\qquad\forall k,v.

1. 因果约束: send <= has

s[k,u,v,t]\leq h[k,u,t].

发送之前, $u$ 必须已经持有 chunk $k$ .

2. 反冗余约束 (optional)

s[k,u,v,t]\leq 1-h[k,v,t].

$u$ 向 $v$ 发 chunk $k$ 时, $v$ 在这一步开始时必须还没有这个数据, 避免向已经持有数据的节点重复发送.

3. 数据持有与接收

已经持有的数据继续保留:

h[k,v,t+1]\geq h[k,v,t].

收到数据后, 下一步持有:

h[k,v,t+1]\geq s[k,u,v,t], \qquad\forall u:(u,v)\in E.

同时加上上界:

h[k,v,t+1] \leq h[k,v,t] +\sum_{u:(u,v)\in E}s[k,u,v,t].

合起来就是:

\mathrm{next\_has} =\mathrm{old\_has}\ \mathrm{OR}\ \mathrm{received}.

4. Link 容量

\sum_k s[k,u,v,t]\leq 1.

对链路 $(u,v)$ , 在 $[t,t+1)$ 中最多发送一个 chunk.

固定 $H$ 时是在求可行解. 枚举 $H$ , 就可以把这个可行性问题用于搜索最少时间步数; 要证明最优, 需要证明更小的 $H$ 都不可行.

SAT

SAT: 求 Boolean 表达式是否存在满足的赋值.

CNF (Conjunctive Normal Form): 若干 clause 之间用 AND 连接, 每个 clause 内部用 OR 连接 literal.

Unit propagation: 在当前赋值下, 若一个 clause 只剩一个未定 literal, 其余 literal 都为 false, 就必须让这个 literal 为 true. 继续传播这些必然的赋值, 可以缩小搜索空间.

SMT

SMT (Satisfiability Modulo Theories): 在 Boolean 结构之外, 还检查整数, 实数等理论约束是否可以同时满足.

用 SMT 处理优化问题

Bounded Search: 设置搜索边界, 用 SAT/SMT 求解不同配置的可行性, 再调整配置, 缩小搜索范围. 前面枚举 $H$ 就是一个例子.
OMT (Optimization Modulo Theories): 在 SMT 约束上直接加入优化目标.

回顾 P 与 NP

P: 可以在多项式时间内求解的决策问题.
NP: 对于答案为 yes 的实例, 存在多项式长度的证书, 可以在多项式时间内验证.
$P\subseteq NP$ : 如果已经能在多项式时间内求解, 验证时可以直接运行求解算法.

对问题 $L$ , $x$ 表示它的一个具体 instance, $c$ 表示 certificate. NP 的验证关系可以写成:

x\in L\quad\Longleftrightarrow\quad\exists c:\ V_L(x,c)=1,

其中 $c$ 的长度以及验证时间都受 $|x|$ 的多项式限制.

3-SAT 既是 NP-hard, 又属于 NP, 因此是 NP-complete 问题.

Program Synthesis

手写稿中的流程:

[Spec + Sketch / DSL]
          ↓
   [Encoding: SMT]
          ↓
       [Solve]
          ↓
       [Model]
          ↓
[Decoding / Filling Template]
          ↓
   [Program / Schedule]

这里的 Model 是求解器给出的满足赋值. 将它解码或填入模板, 得到程序或调度. CEGIS (Counterexample-Guided Inductive Synthesis) 可以通过候选生成, 验证和反例反馈反复进行求解.