2-2 组合优化问题-常用模型与通用求解器

组合优化问题常用模型

组合优化问题常常难以求解，我们可以把这些转化为目前已经有成熟求解器的模型。

1. 可满足性问题（Satisfiability, SAT）

上一节已经讲过，SAT 是一个 NPC 问题，很多NP难的组合优化问题都可以归约到SAT。用SAT问题求解另一问题的过程，称作SAT编码。下面给出k-图着色的判定问题归约到SAT的编码方式。

例1. k-图着色问题（k-coloring problem）：判定一个无向图 G = ( V , E ) G=(V,E) G=(V,E) 是否可以由 k 种不同的颜色对 V 中所有的顶点着色，其中 E 中任意一条边的两个顶点不能着同一种颜色。判定是否存在一种着色方案满足要求。

编码方式：

定义变量 x i , j x_{i,j} xi,j 表示对G中第i个顶点着第j种颜色，共有 k|V| 个变量。
为了保证图中每个顶点都着色，定义子句：
c i = ⋁ 1 ≤ j ≤ k x i , j c_{i}=\bigvee_{1 \leq j \leq k} x_{i, j} ci=1≤j≤k⋁xi,j
表明每个顶点至少有一种颜色，这样的子句共有 |V| 条。
为了保证图中任意两条边的颜色不同，定义如下子句：
c i , j , k ′ = ¬ x i , k ∨ ¬ x j , k c_{i, j, k}^{\prime}=\neg x_{i, k} \vee \neg x_{j, k} ci,j,k′=¬xi,k∨¬xj,k
其中i，j表示E中的边，k表示某种着色。这样的子句共有k|E|条。

这样就得到了一个k-图着色问题可行的SAT编码。

上面给出的编码简单直接，但并不是最好的编码。但我们可以由此得出编码SAT问题的思路：

 1. 考虑约束变量的定义和个数2. 考虑问题的条件可以用什么子句表达3. 考虑问题的对称性

目前的SAT求解器有 MiniSAT（主流）, Glucose, Maple, ReasonLS等。

2. SAT的变形（MaxSAT, partial MaxSAT, weighted partial MaxSAT）

MaxSAT 问题是SAT问题的变形。

MaxSAT： 给定一个CNF公式，找到一个完备赋值，满足给定的 CNF 公式 F 中最多的子句。

当F中所有的子句都可以被满足的时候，MaxSAT就等同于SAT问题。

partial MaxSAT： 假如将子句分为硬字句和软子句两部分，partial MaxSAT
问题需要尽可能的满足更多的软子句并满足所有的硬字句。

例2. 找图G=（V，E）中的最大团，可以按照如下的策略将其编码成partial MaxSAT 问题：

对每一个G中的顶点定义一个变量 x i x_i xi，表示该顶点是否在团中。共有 |V| 个这样的变量。
定义一条硬子句，满足图中任意一堆不相邻的顶点，不能都在团中：
c i , j = ¬ x i ∨ ¬ x j c_{i, j}=\neg x_{i} \vee \neg x_{j} ci,j=¬xi∨¬xj
定义一条软子句，使得一个团中有尽可能多的顶点：
c i ′ = x i c_{i}^{\prime}=x_{i} ci′=xi
此时如果得到一个最优解，就得到了最大团。

weighted partial MaxSAT： 为 partial MaxSAT 问题中的每一条边赋予一个权值，求解目标转化为满足所有的硬子句，并且使满足的软子句的权值之和最大。

经过以上的描述，可以看出SAT问题和其变形问题都可以作为一个通用求解器。
但是，SAT 的表述能力限制于命题逻辑。
还有表述能力更强的 CSP 和SMT 问题和相应的求解器，分别可以用来求解约束满足问题和一阶逻辑相关的问题。

3. 约束满足问题（CSP）

Constraint Satisfication Problem, CSP: 约束满足问题定义为一组对象，这些对象需要满足一定的条件约束。CSP 一般描述为三元对(X,D,C)，包含变量集合 X = { X 1 , X 2 , ⋯ , X n } X=\left\{X_{1}, X_{2}, \cdots, X_{n}\right\} X={X1,X2,⋯,Xn}，变量的定义域 D = { D 1 , D 2 , ⋯ , D n } D=\left\{D_{1}, D_{2}, \cdots, D_{n}\right\} D={D1,D2,⋯,Dn} ，和一个约束集合 C = { C 1 , C 2 , ⋯ , C n } \mathrm{C}=\left\{\mathrm{C}_{1}, \mathrm{C}_{2}, \cdots, \mathrm{C}_{n}\right\} C={C1,C2,⋯,Cn}。
其中每个变量 X i X_i Xi 可以在非空的定义域Di中取出。限制条件Cj依序对应一对 <tj,Rj>，tj是n维变量，Rj是从定义域Dj映射到子集合上的n维关系。
变量有对应的评估函数f，从变量映射到值域。如果 f ( x 1 ) , … , f ( x n ) ∈ R j f(x_1),\ldots,f(x_n) \in R_j f(x1),…,f(xn)∈Rj, 那么f满足 < ( t 1 , … , t n ) , R j > <(t_1,\ldots,t_n),R_j> <(t1,…,tn),Rj>的条件限制。

对于CSP问题，我们称赋值是无矛盾的当且仅当一个评估不违反任何的条件限制，称赋值是完备的当且仅当一个评估包含了所有变量。一个赋值是无矛盾且完备的，那么这个评估就是CSP问题的一个解。

例3. 4皇后问题：判定是否可以将皇后互无冲突地放在4*4的棋盘上。无冲突指任何两个皇后不能在同一对角线或者行列上。

首先确定变量的个数和取值，再确定变量之间的关系。

变量集合 X = { x 1 , x 2 , x 3 , x 4 } X=\left\{x_{1}, x_{2},x_3 , x_{4}\right\} X={x1,x2,x3,x4}，xi表示第i列的皇后所在的行。
xi的取值范围 Di={1，2，3，4}
根据任何两个皇后不在同一行列和同一对角线的约束：
x i ≠ x j , ( 0 < i < j ≤ n ) ∣ x i − x j ∣ ≠ ∣ i − j ∣ , ( 0 < i < j ≤ n ) x_i\neq x_j, (0<i<j\le n)\\ |x_i-x_j|\neq |i-j|, (0<i<j\le n) xi=xj,(0<i<j≤n)∣xi−xj∣=∣i−j∣,(0<i<j≤n)

x1和x2的约束条件可写为：<(x1,x2),{(1,3),(1,4),(2,4),(3,1),(4,1)}>

CSP 可以比 SAT 更紧凑地表达多取值的约束问题。

4. 多理论下的可满足性问题（SMT）

Satisfiability Modulo Theories，SMT: 判定一阶逻辑公式在组合背景理论下的可满足问题，比SAT更强。

一节逻辑可以强力描述现实世界中的绝大多数问题，求解能力强于命题逻辑。

一般SMT求解器可以处理的理论包括：

未解释函数（Uninterpreted Function，UF）主要包括一些没有经过解释的函数符号和它们的参数。
例4. a = b ∧ b = f ( c ) ∧ ¬ ( g ( a ) = g ( f ( c ) ) ) a=b \wedge b=f(c) \wedge \neg(g(a)=g(f(c))) a=b∧b=f(c)∧¬(g(a)=g(f(c)))表示了一个由带符号的未解释函数组成的公式
线性实数演算（Linear real arithmetic,LRA）和线性整数演算（Linear Integer arithmetic,LIA）可以表示为 a 1 x 1 + ⋯ + a n x n ⋈ c a_{1} x_{1}+\cdots+a_{n} x_{n} \bowtie c a1x1+⋯+anxn⋈c，其中 ⋈ \bowtie ⋈可以表示 = 、 ≠ 、 ⩽ 、 ⩾ =、 \neq 、 \leqslant 、 \geqslant =、=、⩽、⩾等符号。
非线性实数演算（non-liner real arithmetic，NRA）和非线性整数演算（non-linear integer arithmetic，NIA）的公式则可以表示任意的数学表达式
实数差分逻辑（difference logic over the reals, RDL）和整数差分逻辑（difference logic
over the integers, IDL）一般可以表示成 x − y ⋈ c x-y \bowtie c x−y⋈c的形式
数组和位向量。用于处理计算机中的数据结构

线性规划与整数线性规划

运筹学中的通用模型（Linear Programming, LP）, 一般形式为
min ⁡ c ′ x s.t. { A x = b x ≥ 0 \begin{aligned} &\min c^{\prime} x\\ &\text { s.t. }\left\{\begin{array}{c} A x=b \\ x \geq 0 \end{array}\right. \end{aligned} minc′x s.t. {Ax=bx≥0

SAT求解技术简介

完备性（complete）算法：对于给定的一组CNF公式，一定能够证明其可满足性。一般采用回溯+推理
不完备（incomplete）算法：仅证明一组公式是可满足的，不能证明一个公式是不可满足的。一般采用局部搜索

归结原理（Resolution rule）: 如果一个CNF公式 F 包含两个子句 x ∨ α x \vee \alpha x∨α 和 ¬ x ∨ β \neg x \vee \beta ¬x∨β，那么公式 F 可以推出 α ∨ β \alpha \vee \beta α∨β。
归结原理是一个充分且完备的规则。

完备的SAT求解算法的主要框架是回溯粗略，比较有代表性的算法有DPLL和CDCL