网站开发类比赛,晋中网站建设价格,建设银行个人网站官网,承德网站建设方案前言
SAT 问题简介
SAT是可满足性、适定性(Satisfiability)问题的简称。一般形式为k-适定性问题或k-可满足性问题#xff0c;简称 k-SAT。
何为布尔可满足性问题#xff1f;给定一条真值表达式#xff0c;包含逻辑变量、逻辑与、逻辑或以及非运算符#xff0c;如#x…前言
SAT 问题简介
SAT是可满足性、适定性(Satisfiability)问题的简称。一般形式为k-适定性问题或k-可满足性问题简称 k-SAT。
何为布尔可满足性问题给定一条真值表达式包含逻辑变量、逻辑与、逻辑或以及非运算符如 ( a ∧ ¬ b ∧ ( ¬ ( c ∨ d ∨ ¬ a ) ∨ ( b ∧ ¬ d ) ) ) ∨ ( ¬ ( ¬ ( ¬ b ∨ a ) ∧ c ) ∧ d ) (a\wedge\neg b\wedge(\neg(c\vee d\vee\neg a)\vee(b\wedge\neg d)))\vee(\neg(\neg(\neg b\vee a)\wedge c)\wedge d) (a∧¬b∧(¬(c∨d∨¬a)∨(b∧¬d)))∨(¬(¬(¬b∨a)∧c)∧d)
是否存在一组对这些变量的赋值使得整条式子最终的运算结果为 t r u e true true若可以那么这个性质被称为这条逻辑公式的可满足性satisfiability如何快速高效地判断任意指定逻辑公式的可满足性是理论计算机科学中的一个重要的问题也是第一个被证明为NP-完全NP-completeNPC的问题。
当 k 2 k2 k2时可满足性问题是NPC问题因此我们一般只研究 k 2 k2 k2的情况。
2-SAT算法
通常所说的2-SAT问题往往需要我们处理对于 n n n个布尔变量 { x n } ( x i ∈ { 0 , 1 } ) \{x_n\}\left(x_i\in\{0,1\}\right) {xn}(xi∈{0,1})的 m m m个限制。 其每个限制都形如一个 ∨ \vee ∨运算符连接的两个简单限制条件简单限制条件为 x i t r u e x_itrue xitrue记作 x i x_i xi或 x i f a l s e x_ifalse xifalse记作 ¬ x i \neg x_i ¬xi因此限制条件一共有四种 s k x i ∨ x j s_kx_i\vee x_j skxi∨xj s k ¬ x i ∨ x j s_k\neg x_i\vee x_j sk¬xi∨xj s k x i ∨ ¬ x j s_kx_i\vee\neg x_j skxi∨¬xj s k ¬ x i ∨ ¬ x j s_k\neg x_i\vee \neg x_j sk¬xi∨¬xj
我们需要满足 ⋀ m i 1 s i t r u e \underset{i1}{\overset m{ \bigwedge }}s_itrue i1⋀msitrue 也就是需要每一个 s k s_k sk都为真。
其处理方法为 首先建图对变量 x i x_i xi建立两个点 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1表示选 x i 0 x_i0 xi0或 x i 1 x_i1 xi1然后在新图上对每个限制按照如下方式连边。 例如对于限制 s k s_k sk我们讨论这条限制下 a , b ∈ { 0 , 1 } a,b\in\{0,1\} a,b∈{0,1} x i a x_ia xia时是否一定有 x j b x_jb xjb如果一定有就连有向边 x i , a → x j , b x_{i,a}\rightarrow x_{j,b} xi,a→xj,b。 同理我们讨论 x j a x_ja xja是否一定有 x i b x_ib xib如果一定有就连有向边 x j , a → x i , b x_{j,a}\rightarrow x_{i,b} xj,a→xi,b
感性理解这张图如果 x i , a x_{i,a} xi,a可达 x j , b x_{j,b} xj,b则说明 x i a x_ia xia可以推出 x j b x_jb xjb或者说 x i a x_ia xia蕴含了 x j b x_jb xjb。
因此我们知道这个可满足性问题无解的充要条件为存在 i i i使得 x i , 0 x_{i,0} xi,0和 x i , 1 x_{i,1} xi,1处于同一个强连通分量内这意味着 x i 0 x_i0 xi0推出 x i 1 x_i1 xi1同时 x i 1 x_i1 xi1推出 x i 0 x_i0 xi0因此无解。
因此我们可以使用Tarjan算法求强连通分量来判断2-SAT问题是否有解事实上我们还可以输出一组可行解。 具体方法如下首先对我们建图的图求强连通分量缩点得到一张DAG然后对DAG进行拓扑排序则 x i x_i xi对应的两个节点中对应的强连通分量拓扑序较为靠后的节点对应的权值是 x i x_i xi取得的权值。 其原理是如果 x i a x_ia xia会推出 x i b x_ib xib那么就不能选 x i a x_ia xia此时只能选 x i b x_ib xib。
这样我们就用Tarjan算法取得了可满足性问题的 O ( n m ) O(nm) O(nm)做法。
具体的连边方式
首先所有限制都可以转化为 x i a ⇒ x j b x_ia\Rightarrow x_jb xia⇒xjb的形式进行连边这里记录一些经典的连边方式这样就不需要每次做转化了。 x i a ⇒ x j b x_ia\Rightarrow x_jb xia⇒xjb x i , a → x j , b x_{i,a}\rightarrow x_{j,b} xi,a→xj,b x j , ¬ b → x i , ¬ a x_{j,\neg b}\rightarrow x_{i,\neg a} xj,¬b→xi,¬a a ∨ b a\vee b a∨b a 0 → b 1 a_0\rightarrow b_1 a0→b1 b 0 → a 1 b_0\rightarrow a_1 b0→a1 ¬ a ∨ b \neg a\vee b ¬a∨b a 1 → b 1 a_1\rightarrow b_1 a1→b1 b 0 → a 0 b_0\rightarrow a_0 b0→a0 ¬ a ∨ ¬ b \neg a\vee\neg b ¬a∨¬b a 1 → b 0 a_1\rightarrow b_0 a1→b0 b 1 → a 0 b_1\rightarrow a_0 b1→a0 a t r u e atrue atrue 转化为 a 0 ⇒ a 1 a0\Rightarrow a1 a0⇒a1 a 0 → a 1 a_0\rightarrow a_1 a0→a1 a f a l s e afalse afalse 转化为 a 1 ⇒ a 0 a1\Rightarrow a0 a1⇒a0 a 1 → a 0 a_1\rightarrow a_0 a1→a0 a b ab ab 转化为 a 1 ⇒ b 1 a1\Rightarrow b1 a1⇒b1且 a 0 ⇒ b 0 a0\Rightarrow b0 a0⇒b0 a ̸ b a\notb ab a ⊗ b a\otimes b a⊗b 转化为 a 0 ⇒ b 1 a0\Rightarrow b1 a0⇒b1且 a 1 ⇒ b 0 a1\Rightarrow b0 a1⇒b0 x 1 , x 2 , x 3 , . . . x_1,x_2,x_3,... x1,x2,x3,...至多一个为真 转化为 x 1 1 ⇒ x 2 0 x_11\Rightarrow x_20 x11⇒x20且 x 1 1 ⇒ x 3 0 x_11\Rightarrow x_30 x11⇒x30…且 x 2 1 ⇒ x 1 0 x_21\Rightarrow x_10 x21⇒x10且 x 2 1 ⇒ x 3 0 x_21\Rightarrow x_30 x21⇒x30…且 x 3 1 ⇒ x 1 0 x_31\Rightarrow x_10 x31⇒x10且 x 3 1 ⇒ x 2 0 x_31\Rightarrow x_20 x31⇒x20…… 注意这样连出来的边数是 O ( m 2 ) O(m^2) O(m2)级别的 x 1 , x 2 , x 3 , . . . x_1,x_2,x_3,... x1,x2,x3,...至多 k 1 k1 k1个为真 2-sat一般不能做 x 1 , x 2 , x 3 , . . . x_1,x_2,x_3,... x1,x2,x3,...至少 k ≥ 1 k\geq 1 k≥1个为真 2-sat一般不能做 x 1 , x 2 , x 3 , . . . x_1,x_2,x_3,... x1,x2,x3,...恰好 k ≥ 1 k\geq 1 k≥1个为真 2-sat一般不能做
其中一些限制条件也可以在连边的时候判掉。
2-SAT原理
我们现在有 n n n个布尔变量称为 { x n } ( x i ∈ { 0 , 1 } ) \{x_n\}\left(x_i\in \{0,1\}\right) {xn}(xi∈{0,1})现在给出 m m m条限制每一条限制都形如 当 x i a x_ia xia时有 x j b x_jb xjb a , b ∈ { 0 , 1 } a,b\in\{0,1\} a,b∈{0,1} 即 x i a ⇒ x j b x_ia\Rightarrow x_jb xia⇒xjb
接下来说一下如何求解这个问题。
图的建立
点的意义
我们使用图论方法对这个问题进行求解按照经典套路我们需要在图上定义一个集合然后把原问题的意义在集合内体现出来。
具体来说我们有一个集合 S S S同时在图上有 2 n 2n 2n个点其中每个比尔变量 x i x_i xi对应两个点一个叫做 x i , 0 x_{i,0} xi,0另一个叫做 x i , 1 x_{i,1} xi,1。 我们规定 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1当中只能恰好有一个属于集合 S S S如果 x i , 0 ∈ S x_{i,0}\in S xi,0∈S则 x i 0 x_i0 xi0如果 x i , 1 ∈ S x_{i,1}\in S xi,1∈S则 x i 1 x_i1 xi1。
我们知道根据限制能够推出一些关系例如如果 x i , a ∈ S x_{i,a}\in S xi,a∈S那么一定有 x j , b ∈ S x_{j,b}\in S xj,b∈S我们希望用边表示这一种关系因此我们规定对于任意元素 u ∈ S u\in S u∈S u u u在图上可达的所有点 v v v均属于 S S S。
边的意义
刚才已经定义了图中的点以及集合 S S S。现在具体说一下图中的边是如何连接的 对于限制 x i a ⇒ x j b x_ia\Rightarrow x_jb xia⇒xjb
我们考虑一个一个向着集合 S S S内添加元素的过程我们必然是找到一个点 u u u加入集合然后将 u u u的所有后继加入 S S S然后把这些后继的所有后继加入 S S S… 由于我们知道 x i a x_ia xia时 x j b x_jb xjb因此对于这个限制我们在图上连边 x i , a → x j , b x_{i,a}\rightarrow x_{j,b} xi,a→xj,b这样就似乎可以表示这个限制了。 注意连边方式到这里还不完全正确
此时我们会得到一个暴力算法
枚举一个未被确定的变量 x i x_i xi先选择 x i , 0 x_{i,0} xi,0然后检查 x i , 0 x_{i,0} xi,0可达的所有点我们将会选中他们。 如果发生冲突即存在 x j , 0 , x j , 1 ∈ S x_{j,0},x_{j,1}\in S xj,0,xj,1∈S那么就说明 x i ̸ 0 x_i\not0 xi0回溯。 如果 x i , 0 x_{i,0} xi,0不能选那么就选择 x i , 1 x_{i,1} xi,1然后检查 x i , 1 x_{i,1} xi,1的可达点检查是否有冲突如果没有就选上它们否则就说明无解。
但是我们会发现这个算法是会错的举例来说对于以下两个限制 y 0 ⇒ x 1 y0\Rightarrow x1 y0⇒x1 y 1 ⇒ x 1 y1\Rightarrow x1 y1⇒x1
我们会连出这张图 但是如果我们一开始选择 x 0 x_0 x0后来就会发现无论选择 y 0 y_0 y0还是 y 1 y_1 y1都会有矛盾此时就输出无解显然是不对的。
这样会出错是因为对于这样的一条限制 y 0 ⇒ x 1 y0\Rightarrow x1 y0⇒x1来说选择 x x x的值是会对 y y y的值产生影响的具体来说如果 x 0 x0 x0这就说明 y ̸ 0 y\not0 y0即 y 1 y1 y1。
换句话说命题 y 0 ⇒ x 1 y0\Rightarrow x1 y0⇒x1的逆否命题 x ̸ 1 ⇒ y ̸ 0 x\not1\Rightarrow y\not 0 x1⇒y0即 x 0 ⇒ y 1 x0\Rightarrow y1 x0⇒y1具有和原命题一致的真假性因此选择 x x x的值可能会对 y y y造成影响因此我们需要进一步讨论 x a ⇒ y b xa\Rightarrow yb xa⇒yb说明了 x , y x,y x,y之间的那些关系
当我们选择了 x a x_a xa时必然有 y b y_b yb当我们选择了 x ¬ a x_{\neg a} x¬a时这条限制不提供任何约束即有可能选择 y b y_b yb或 y ¬ b y_{\neg b} y¬b当我们选择了 y b y_b yb时这条限制不提供任何约束即有可能选择 x a x_a xa或 x ¬ a x_{\neg a} x¬a当我们选择了 y ¬ b y_{\neg b} y¬b时必然有 x ¬ a x_{\neg a} x¬a
因此事实上对于限制 x i a ⇒ x j b x_ia\Rightarrow x_{j}b xia⇒xjb来说我们应该连接两条边 x i , a → x j , b x_{i,a}\rightarrow x_{j,b} xi,a→xj,b x j , ¬ b → x i , ¬ a x_{j,\neg b}\rightarrow x_{i,\neg a} xj,¬b→xi,¬a
此时我们再进行刚才的暴力算法我们就获得了时间复杂度为 O ( n ⋅ m ) O(n\cdot m) O(n⋅m)的2-sat问题的dfs做法。值得一提的是这种做法还能同时让我们获得2-sat问题字典序最小的解。
接下来简要对暴力做法的正确性进行说明
首先我们证明解的充分性即我们求出的解确实是原问题的一组解 首先我们知道对于一个限制 x i a ⇒ x j b x_{i}a\Rightarrow x_{j}b xia⇒xjb这个限制被违反当且仅当 x i , a , x j , ¬ b ∈ S x_{i,a},x_{j,\neg b}\in S xi,a,xj,¬b∈S。
如果说在算法过程中 x i , a x_{i,a} xi,a比 x j , ¬ b x_{j,\neg b} xj,¬b先选的话发生这种情况一定不可能因为我们选择 x i , a x_{i,a} xi,a时根据连边一定选择了 x j , b x_{j,b} xj,b因此后来无法选择 x j , ¬ b x_{j,\neg b} xj,¬b了矛盾。 如果 x i , a x_{i,a} xi,a比 x j , ¬ b x_{j,\neg b} xj,¬b后选的话这种情况还是不可能因为根据连边的方式如果我们选择了 x j , ¬ b x_{j,\neg b} xj,¬b我们一定选择了 x i , ¬ a x_{i,\neg a} xi,¬a不可能再选择 x i , a x_{i,a} xi,a因此仍然矛盾。
因此我们就证明我们构造出的一组解满足所有限制条件因此是一组合法解。
接下来我们证明解的必要性即有解的时候我们一定能够构造出一组解。 只需证明逆否命题即如果我们构造不出一组解此时这个问题无解。 我们考虑求解过程在决定变量 x i x_i xi的取值时报告了无解。 此时必然是因为发生了矛盾首先讨论选取 x i , 0 x_{i,0} xi,0时候的情况矛盾即存在元素 x j , 0 , x j , 1 ∈ S x_{j,0},x_{j,1}\in S xj,0,xj,1∈S。 此时有两种情况第一种情况是 x j , 0 , x j , 1 x_{j,0},x_{j,1} xj,0,xj,1都是在 x i , 0 x_{i,0} xi,0加入集合 S S S后加入集合的此时显然选择 x i , 0 x_{i,0} xi,0会同时推出 x j 0 x_j0 xj0和 x j 1 x_j1 xj1因此 x i ̸ 0 x_i\not0 xi0。
第二种情况是 x j , a x_{j,a} xj,a是在 x i , 0 x_{i,0} xi,0加入集合 S S S前加入集合的而 x j , ¬ a x_{j,\neg a} xj,¬a是因为加入 x i , 0 x_{i,0} xi,0而加入集合 S S S的换句话说存在路径使得 x i , 0 ⇝ x j , ¬ a x_{i,0}\rightsquigarrow x_{j,\neg a} xi,0⇝xj,¬a这种情况不存在这是因为如果存在路径使得 x i , 0 ⇝ x j , ¬ a x_{i,0}\rightsquigarrow x_{j,\neg a} xi,0⇝xj,¬a由于接下来说到的性质2我们必然知道存在一条路径使得 x j , a ⇝ x i , 1 x_{j,a}\rightsquigarrow x_{i,1} xj,a⇝xi,1因此当 x j , a ∈ S x_{j,a}\in S xj,a∈S后 x i , 1 ∈ S x_{i,1}\in S xi,1∈S这与 x i x_i xi取值未确定矛盾因此第二种情况不存在。
不可能存在一种情况使得 x j , 0 , x j , 1 x_{j,0},x_{j,1} xj,0,xj,1在加入 x i , 0 x_{i,0} xi,0前都在集合 S S S内因为这违反 S S S的定义。
同理我们知道如果在选择 x i , 1 x_{i,1} xi,1的时候发生矛盾只可能是因为 x i ̸ 1 x_i\not1 xi1。此时我们就得知了 x i ̸ 0 x_i\not0 xi0且 x i ̸ 1 x_i\not1 xi1因此得到这个可满足性问题无解。
QED.
线性算法
接下来我们说一下这个问题的线性算法线性算法是这样的
对建出来的图缩强连通分量这样会得到一张DAG如果存在点 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1在一个强连通分量内则说明无解。否则有解对DAG拓扑排序 x i x_i xi的取值是它对应的两个点 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1对应的强连通分量中拓扑序较靠后的那个点的取值。
证明
接下来我们证明一下线性算法的正确性。
性质1
边的对称性 对于任意一条有向边 ( x i , a , x j , b ) (x_{i,a},x_{j,b}) (xi,a,xj,b)都存在有向边 ( x j , ¬ b , x i , ¬ a ) (x_{j,\neg b},x_{i,\neg a}) (xj,¬b,xi,¬a)我们称为其对称边。
证明 回忆建图的方式这条性质是显然成立的。
性质2
路径的对称性 对于任意一条从 x i , a x_{i,a} xi,a到 x j , b x_{j,b} xj,b的路径必然存在对应的一条路径从 x j , ¬ b x_{j,\neg b} xj,¬b到 x i , ¬ a x_{i,\neg a} xi,¬a。
证明 我们找到从 x i , a x_{i,a} xi,a到 x j , b x_{j,b} xj,b的路径上的每一条边的对称边显然它们拼成一条从 x j ¬ b x_{j\neg b} xj¬b到 x i , ¬ a x_{i,\neg a} xi,¬a的路径。
算法1
我们可以据此提出一个求解2-sat问题的算法
对建出来的图缩强连通分量这样会得到一张DAG如果存在点 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1在一个强连通分量内则说明无解。否则有解我们通过如下过程构造解 找到一个没有确定的 x i x_i xi由于 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1不强连通因此不可能存在二者相互可达。如果有 x i , 0 ⇝ x i , 1 x_{i,0}\rightsquigarrow x_{i,1} xi,0⇝xi,1那就令 x i , 1 ∈ S x_{i,1}\in S xi,1∈S。否则说明一定有 x i , 1 ⇝ x i , 0 x_{i,1}\rightsquigarrow x_{i,0} xi,1⇝xi,0或者 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1互相不可达此时令 x i , 0 ∈ S x_{i,0}\in S xi,0∈S。如果此时我们有 x i , a ∈ S x_{i,a}\in S xi,a∈S那就说明有 x i , ¬ a ∉ S x_{i,\neg a}\notin S xi,¬a∈/S。同时说明 x i , a x_{i,a} xi,a的所有后继都属于 S S S把它们加入 S S S。同时说明 x i , ¬ a x_{i,\neg a} xi,¬a的所有前驱都不属于 S S S。直到所有的变量取值都确定此时我们得到了一组可行解。
定理1
缩点后得到的DAG满足没有任何一个 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1强连通是原问题有解的必要条件。
证明其逆否命题 如果存在 x i , 0 , x i , 1 x_{i,0},x_{i,1} xi,0,xi,1强连通那么我们沿着 x i , 0 ⇝ x i , 1 ⇝ x i , 0 x_{i,0}\rightsquigarrow x_{i,1}\rightsquigarrow x_{i,0} xi,0⇝xi,1⇝xi,0的回路走上面的边对应的限制条件就说明当 x i 0 x_{i}0 xi0时 x i 1 x_i1 xi1并且当 x i 1 x_i1 xi1时 x i 0 x_i0 xi0此时显然无解。
QED.
定理2
按照上述算法1流程构造出的解是原问题的一组解。
证明 如果这组解不是原问题的一组解那么一定存在至少一个限制被违背了设这个限制是 x i a ⇒ x j b x_ia\Rightarrow x_jb xia⇒xjb这个限制被违反必须有 x i a x_ia xia且 x j ¬ b x_j\neg b xj¬b。
假如说 x i , a x_{i,a} xi,a比 x j , ¬ b x_{j,\neg b} xj,¬b后晚加入集合当我们加入 x j , ¬ b x_{j,\neg b} xj,¬b时由于这条限制对应连出的边 x i , ¬ a x_{i,\neg a} xi,¬a一定也会被加入集合因此 x i , a x_{i,a} xi,a不可能加入集合矛盾。
否则说明 x i , a x_{i,a} xi,a比 x j , ¬ b x_{j,\neg b} xj,¬b先加入集合但是这也不可能因为当我们加入 x i , a x_{i,a} xi,a时由于这条限制对应连出的边 x j , b x_{j,b} xj,b也一定加入集合因此 x j , b x_{j,b} xj,b不可能加入集合矛盾。
QED.
定理3
根据定理1定理2我们证明了 算法1能够求出一组解是原问题有解的充要条件。它求出的解是原问题的一组解。
定理4
容易发现Tarjan算法拓扑排序求解2-sat问题的过程事实上在模拟算法1因此其的正确性也有保证。
后记
于是皆大欢喜。
