SAT规约到3SAT

爱喝白开水的木头人

13089人浏览 · 2018-04-10 16:05:49

爱喝白开水的木头人 · 2018-04-10 16:05:49 发布

SAT规约到3SAT

一、SAT、3SAT问题描述

SAT问题描述：

给定一个又穷的布尔变量集合X={x1,x2,⋯,xn},|X|=n<script type="math/tex" id="MathJax-Element-67">X=\{x_1, x_2, \cdots , x_n\}, |X|=n</script>，每个变量能取0或1，一组子句C={C1,C2,C3,⋯,Cm},|C|=m,C=C1∧C2∧⋯∧Cm<script type="math/tex" id="MathJax-Element-68">C=\{C_1, C_2, C_3,\cdots ,C_m\}, |C|=m,C=C_1\wedge C_2 \wedge \cdots \wedge C_m</script>每个Ci<script type="math/tex" id="MathJax-Element-69">C_i</script> 是由多个变量组成的析取范式，长度不限，即z1∨z2∨z3⋯∨zk<script type="math/tex" id="MathJax-Element-70">z_1\vee z_2 \vee z_3 \cdots \vee z_k </script>。问题：给定一个布尔变量集合X和子句集合C，是否存在一个真值赋值，使得C为真，即每个子句为真。

3SAT问题描述：

给定一个有穷的布尔变量集合X={x1,x2,⋯xn},|X|=n<script type="math/tex" id="MathJax-Element-71">X=\{x_1, x_2, \cdots x_n\}, |X|=n</script>, 每个变量能取0或1，一组子句C={C1,C2,⋯Cm},|C|=m，C=C1∧C2∧⋯∧Cm<script type="math/tex" id="MathJax-Element-72">C=\{C_1, C_2, \cdots C_m\}, |C|=m，C=C_1 \wedge C_2 \wedge \cdots \wedge C_m</script>，每个Ci<script type="math/tex" id="MathJax-Element-73">C_i</script> 是由三个变量组成的析取范式，即z1∨z2∨z3<script type="math/tex" id="MathJax-Element-74">z_1\vee z_2 \vee z_3</script>。问题：给定一个布尔变量集合X和子句集合C，是否存在一个真值赋值，使得C为真，即每个子句为真。
一个例子：
X={x1,x2,x3},C={C1,C2,C3},C1=x1∨x2¯∨x3,C2=x1¯∨x2¯∨x3,C3=x1¯∨x2∨x3¯<script type="math/tex" id="MathJax-Element-75">X=\{x_1, x_2, x_3\}, C=\{C_1, C_2, C_3\}, C_1=x_1 \vee \bar {x_2} \vee x_3, C_2=\bar{x_1} \vee \bar{x_2}\vee{x_3},C_3=\bar{x_1}\vee x_2 \vee \bar{x_3}</script>
则存在一个真值赋值：x1=1,x2=1,x3=1<script type="math/tex" id="MathJax-Element-76">x_1=1, x_2=1, x_3=1</script>,使得C=1<script type="math/tex" id="MathJax-Element-77">C=1</script>

二、证明

1、证明3SAT是NP问题

3SAT的实例为X={x1,x2,⋯,xn},C={C1,C2,⋯,Cm}<script type="math/tex" id="MathJax-Element-1062">X=\{x_1, x_2, \cdots, x_n\} , C=\{C_1, C_2,\cdots, C_m\}</script>证书为对每个变量的赋值，我们只要验证每个子句都为真即可，很明显这个过程是多项式时间的。

2、给出规约过程。

给定一个SAT的实例：X={x1,x2,⋯,xn},C={C1,C2,⋯,Cm},Ci=zi,1∨zi,2∨zi,3⋯∨zi,k<script type="math/tex" id="MathJax-Element-1063">X=\{x_1,x_2,\cdots ,x_n\}, C=\{C_1, C_2, \cdots, C_m\}, C_i=z_{i, 1}\vee z_{i, 2}\vee z_{i, 3}\cdots \vee z_{i, k}</script>，我们要将这个问题的实例变成3SAT的实例X′,C′<script type="math/tex" id="MathJax-Element-1064">X',C'</script>。对于每个Ci<script type="math/tex" id="MathJax-Element-1065">C_i</script>，有以下四种情况：

|Ci|=1<script type="math/tex" id="MathJax-Element-1066">|C_i|=1</script>，则创建2个变量：yi,1,yi,2<script type="math/tex" id="MathJax-Element-1067">y_{i, 1}, y_{i,2}</script>，使得C′i=(zi,1∨yi,1∨yi,2¯)∧(zi,1∨yi,1∨yi,2)∧(zi,1∨yi,1¯∨yi,2¯)∧(zi,1∨yi,1¯∨yi,2)<script type="math/tex" id="MathJax-Element-1068">C_{i}^{'}=(z_{i,1}\vee y_{i,1}\vee \bar {y_{i,2}})\wedge (z_{i,1}\vee y_{i,1}\vee {y_{i,2}})\wedge(z_{i,1}\vee \bar{y_{i,1}}\vee \bar {y_{i,2}})\wedge(z_{i,1}\vee \bar{y_{i,1}}\vee {y_{i,2}})</script>
|Ci|=2<script type="math/tex" id="MathJax-Element-1069">|C_i|=2</script>，则创建1个变量：yi,1<script type="math/tex" id="MathJax-Element-1070">y_{i,1}</script> ，使得C′i=(zi,1∨zi,2∨yi,1)∧(zi,1∨zi,2∨yi,1¯)<script type="math/tex" id="MathJax-Element-1071">C_i^{'}=(z_{i,1}\vee z_{i,2}\vee y_{i,1})\wedge (z_{i,1}\vee z_{i,2}\vee \bar {y_{i,1}})</script>
|Ci|=3<script type="math/tex" id="MathJax-Element-1072">|C_i|=3</script>，则不变即可。
|Ci|≥4<script type="math/tex" id="MathJax-Element-1073">|C_i|\ge 4 </script>，假设为k<script type="math/tex" id="MathJax-Element-1074">k</script>，则添加 $k - 3$ <script type="math/tex" id="MathJax-Element-1075">k-3</script>个变量，使得

$C' i = (z i, 1 \lor z i, 2 \lor y i, 1) \land (y i, 1 ¯ ¯ ¯ ¯ ¯ ¯ ¯ \lor z i, 3 \lor y i, 2) \land (y i, 2 ¯ ¯ ¯ ¯ ¯ ¯ ¯ \lor z i, 4 \lor y i, 3) \land \dots \land (y i, k - 3 ¯ ¯ ¯ ¯ ¯ ¯ ¯ ¯ ¯ ¯ ¯ \lor z i, k - 1 \lor z i, k)$ <script type="math/tex; mode=display" id="MathJax-Element-1076"> C_i^{'}=(z_{i,1}\vee z_{i,2}\vee y_{i,1}) \wedge (\overline{y_{i,1}}\vee z_{i,3} \vee y_{i,2})\wedge(\overline{y_{i,2}}\vee z_{i,4}\vee y_{i,3})\wedge \cdots \wedge (\overline {y_{i,k-3}}\vee z_{i, k-1} \vee z_{i,k}) </script>

3、证明此规约是多项式时间的。

对于每个子句Ci,C′i<script type="math/tex" id="MathJax-Element-1077">C_i, C_i^{'}</script>比Ci<script type="math/tex" id="MathJax-Element-1078">C_i</script>多了最多k−3<script type="math/tex" id="MathJax-Element-1079">k-3</script>个变量，因此多个m(k−3)<script type="math/tex" id="MathJax-Element-1080">m(k-3)</script>个变量和m(k−3)<script type="math/tex" id="MathJax-Element-1081">m(k-3)</script>个子句。接下来我们证明C′<script type="math/tex" id="MathJax-Element-1082">C^{'}</script>是可满足的当且仅当C是可满足的。

4、对于每个SAT的实例，如果存在一个真值赋值，则每个子句Ci<script type="math/tex" id="MathJax-Element-1083">C_i</script>一定有一个literal为1，即zi,1∨zi,2∨⋯∨zi,k<script type="math/tex" id="MathJax-Element-1084">z_{i,1}\vee z_{i,2}\vee \cdots \vee z_{i,k}</script>中一定有一个为1，

(1) |Ci|=1<script type="math/tex" id="MathJax-Element-1085">|C_i|=1</script>，则zi,1=1<script type="math/tex" id="MathJax-Element-1086">z_{i,1}=1</script>，因此不论yi,1,yi,2<script type="math/tex" id="MathJax-Element-1087">y_{i,1},y_{i,2}</script>为何值，C′i=1<script type="math/tex" id="MathJax-Element-1088">C_i^{'}=1</script>
(2)|Ci|=2<script type="math/tex" id="MathJax-Element-1089">|C_i|=2</script>，则zi,1∨zi,2=1<script type="math/tex" id="MathJax-Element-1090">z_{i,1}\vee z_{i,2}=1</script>，不论yi,1<script type="math/tex" id="MathJax-Element-1091">y_{i,1}</script>为何值，C′i=1<script type="math/tex" id="MathJax-Element-1092">C_i^{'}=1</script>
(3)|Ci|=3<script type="math/tex" id="MathJax-Element-1093">|C_i|=3</script>，则C′i=1<script type="math/tex" id="MathJax-Element-1094">C_i^{'}=1</script>
(4)|Ci|≥4<script type="math/tex" id="MathJax-Element-1095">|C_i|\ge 4</script>，则假设：
- zi,1∨zi,2=1,则yi,j=0(j=1,2,3,⋯,k−3)<script type="math/tex" id="MathJax-Element-1096">z_{i,1}\vee z_{i,2}=1, 则y_{i,j}=0(j=1,2,3,\cdots ,k-3)</script>，因此C′i=1<script type="math/tex" id="MathJax-Element-1097">C_i^{'}=1</script>

zi,k−1∨zi,k=1,则yi,j=1(j=1,2,3,⋯,k−3)<script type="math/tex" id="MathJax-Element-1098">z_{i,k-1}\vee z_{i,k}=1,则y_{i,j}=1(j=1,2,3,\cdots ,k-3)</script>，因此C′i=1<script type="math/tex" id="MathJax-Element-1099">C_i^{'}=1</script>
zi,j=1(2<j<k−1),则yi,a¯¯¯¯¯¯¯=0(a≤j−2),yi,a=0(a≥j−1)<script type="math/tex" id="MathJax-Element-1100">z_{i,j}=1(2

因此得到C′<script type="math/tex" id="MathJax-Element-1102">C^{'}</script>的真值赋值t′<script type="math/tex" id="MathJax-Element-1103">t^{'}</script>

5、假设t′<script type="math/tex" id="MathJax-Element-1104">t^{'}</script>是C′<script type="math/tex" id="MathJax-Element-1105">C^{'}</script>的真值赋值，很容易得出C存在真值赋值：
当C′i=(zi,1∨yi,1∨yi,2¯¯¯¯¯¯¯)∧(zi,1∨yi,1∨yi,2)∧(zi,1∨yi,1¯¯¯¯¯¯¯∨yi,2¯¯¯¯¯¯¯)∧(zi,1∨yi,1¯¯¯¯¯¯¯∨yi,2)=1<script type="math/tex" id="MathJax-Element-1106">C_{i}^{'}=(z_{i,1}\vee y_{i,1}\vee \overline {y_{i,2}})\wedge (z_{i,1}\vee y_{i,1}\vee {y_{i,2}})\wedge(z_{i,1}\vee \overline{y_{i,1}}\vee \overline {y_{i,2}})\wedge(z_{i,1}\vee \overline{y_{i,1}}\vee {y_{i,2}})=1</script>，则必须要zi,1=1<script type="math/tex" id="MathJax-Element-1107">z_{i,1}=1</script>

当C′i=(zi,1∨zi,2∨yi,1)∧(zi,1∨zi,2∨yi,1¯¯¯¯¯¯¯)=1<script type="math/tex" id="MathJax-Element-1108">C_i^{'}=(z_{i,1}\vee z_{i,2}\vee y_{i,1})\wedge (z_{i,1}\vee z_{i,2}\vee \overline {y_{i,1}})=1</script>，则必须有zi,1∨zi,2=1<script type="math/tex" id="MathJax-Element-1109">z_{i,1}\vee z_{i,2}=1</script>

当C′i=(zi,1∨zi,2∨yi,1)∧(yi,1¯¯¯¯¯¯¯∨zi,3∨yi,2)∧(yi,2¯¯¯¯¯¯¯∨zi,4∨yi,3)∧⋯∧(yi,k−3¯¯¯¯¯¯¯¯¯¯¯∨zi,k−1∨zi,k)<script type="math/tex" id="MathJax-Element-1110">C_i^{'}=(z_{i,1}\vee z_{i,2}\vee y_{i,1}) \wedge (\overline{y_{i,1}}\vee z_{i,3} \vee y_{i,2})\wedge(\overline{y_{i,2}}\vee z_{i,4}\vee y_{i,3})\wedge \cdots \wedge (\overline {y_{i,k-3}}\vee z_{i, k-1} \vee z_{i,k})</script>，
假设zi,1∨zi,2∨zi,3,⋯,zi,k=0<script type="math/tex" id="MathJax-Element-1111">z_{i,1}\vee z_{i,2}\vee z_{i,3}, \cdots , z_{i,k}=0</script>，且C′I=1<script type="math/tex" id="MathJax-Element-1112">C_I^{'}=1</script>，则yi,1=1,yi,1¯¯¯¯¯¯¯=0<script type="math/tex" id="MathJax-Element-1113">y_{i,1}=1, \overline{y_{i,1}} =0</script>，以此类推得出yi,k−3¯¯¯¯¯¯¯¯¯¯¯=0<script type="math/tex" id="MathJax-Element-1114">\overline{y_{i, k-3}}=0</script>，使得最后(yi,k−3¯¯¯¯¯¯¯¯¯¯¯∨zi,k−1∨zi,k)=0<script type="math/tex" id="MathJax-Element-1115">(\overline{y_{i,k-3}}\vee z_{i,k-1} \vee z_{i,k})=0</script>，与C′i=1<script type="math/tex" id="MathJax-Element-1116">C_i^{'}=1</script>矛盾。