SAT問題子句消去法快速求解

姜詠江，陳躍

（1. 對(duì)外經(jīng)濟(jì)貿(mào)易大學(xué)離退休處，北京朝陽(yáng)，100013；2. 西安交通大學(xué)，陜西西安，710000）

SAT問題子句消去法快速求解

姜詠江1，陳躍2

（1. 對(duì)外經(jīng)濟(jì)貿(mào)易大學(xué)離退休處，北京朝陽(yáng)，100013；2. 西安交通大學(xué)，陜西西安，710000）

布爾可滿足性問題（SAT）是最基本的NPC問題，直接涉及到集成電路設(shè)計(jì)優(yōu)化、生物基因、人工智能、互聯(lián)網(wǎng)等諸多領(lǐng)域的快速計(jì)算。給出了一種子句消去法，運(yùn)用限位數(shù)、子句塊和關(guān)聯(lián)段等概念，探索出了用確定法則快速求出SAT滿足解的計(jì)算方法，為純離散變量計(jì)算找到了一種新途徑。

SAT問題；限位數(shù)；子句消去法；子句塊；關(guān)聯(lián)段；多項(xiàng)式時(shí)間復(fù)雜度

引言

P/NP問題是世界難題。這個(gè)問題最早要追溯到上個(gè)世紀(jì)50年代[1]，是由數(shù)學(xué)家?guī)鞝柼亍じ绲聽栂蛴?jì)算機(jī)發(fā)明人之一馮·諾依曼提出的。1971年，斯提芬·庫(kù)克給出了NP類問題的定義[2]，并指出：只要NP-complete一類問題其中之一存在多項(xiàng)式時(shí)間復(fù)雜度算法，就可以認(rèn)定NP=P。斯提芬·庫(kù)克的觀點(diǎn)已被學(xué)術(shù)界廣泛接受[3]。

SAT問題被認(rèn)為是NP-complete一類問題中最基本的問題[4]，直接涉及到集成電路設(shè)計(jì)優(yōu)化、生物基因、人工智能、互聯(lián)網(wǎng)等諸多領(lǐng)域的快速計(jì)算，但以往沒有學(xué)者找到SAT的多項(xiàng)式時(shí)間復(fù)雜度的快速算法。本文給出的子句消去法能夠快速準(zhǔn)確地求出SAT滿足解。

1 SAT問題與限位數(shù)

SAT問題可以用數(shù)碼0和1來表示，這與限位數(shù)理論關(guān)系密切。

1.1 SAT問題定義

“邏輯變量和變量非形式組成的多項(xiàng)式若干個(gè)，求它們與運(yùn)算結(jié)果為真的解問題”就是SAT問題，每個(gè)邏輯多項(xiàng)式叫子句。嚴(yán)格定義如下：

1.2 SAT問題的0和1表示

合取范式CNF可用數(shù)碼“0”表示xij'，用“1”表示xij。那么，式（1）的CNF就可通過表1的形式來表達(dá)。

表 1 CNF的0和1表示

表1的表頭是邏輯變量，每一行是一個(gè)子句。子句與子句之間是邏輯與運(yùn)算的關(guān)系，子句的列與列之間是邏輯或的關(guān)系。每列的0和1為表頭邏輯變量的表現(xiàn)值。

從表1可以看到，只要將邏輯變量設(shè)定為0（或1），那么這個(gè)變量所在的一列表現(xiàn)值為0（或1）的子句的邏輯值一定是1。那么就可以將這些值為1的子句消去，剩下的部分不會(huì)影響到CNF=1的繼續(xù)求解。將CNF的所有變量均如此設(shè)定后，如果沒有子句剩下，那么就可以斷定設(shè)定的變量值全體即是CNF=1的一個(gè)滿足解?？上У氖牵@種設(shè)定方法具有隨機(jī)性，并不能一次性確定出CNF=1的解。這需要一套準(zhǔn)確無誤設(shè)定變量值的方法，才能保證其不具有隨機(jī)性。為此，需要找出CNF的特有結(jié)構(gòu)關(guān)系。

定義2 變量相同的子句組成子句塊，這些變量所有可能子句組成的子句塊稱作完全塊。

1.3 限位數(shù)與子句塊

位數(shù)一定的數(shù)稱作限位數(shù)。限位數(shù)的無效0不能省略[5]。易知k位二進(jìn)制數(shù)共有2k個(gè)。顯然，k個(gè)變量組成的完全塊共有2k個(gè)子句，超過這個(gè)數(shù)就會(huì)出現(xiàn)子句重復(fù)。

表2是3位二進(jìn)制完全塊，共有8個(gè)子句。

表2 3位完全塊

定理1 完全塊CNF=1無解。

證明：不失一般性，從表2容易看出，k位完全塊每一個(gè)變量的0和1表現(xiàn)值都有2k-1個(gè)。這一特征表明，無論如何設(shè)定完全塊邏輯變量的值，都不可能使所有的子句值為1，即總有值為0的子句。證畢。

進(jìn)一步分析完全塊，可見每一個(gè)子句都有一個(gè)反碼數(shù)，這樣的兩個(gè)子句就稱作互反子句。容易知道，不是互反子句至少有一位數(shù)碼相同。因此，子句塊中不存在反子句的子句表現(xiàn)值一定能將這個(gè)子句塊的全部子句消去。還可見，如果非完全塊有一個(gè)變量有2k-1個(gè)0或1，這個(gè)變量不設(shè)定這個(gè)表現(xiàn)值，那么就剩下了k-1個(gè)變量的完全塊，就會(huì)造成無法設(shè)定變量值使得CNF=1。

定義3 變量只有一個(gè)值不使CNF=1無解，這個(gè)值稱作變量唯一解。

定理2 非完全塊的變量有2k-1個(gè)0（或1）表現(xiàn)值是變量唯一解。

證明：不失一般性，從表2容易看出，k位非完全塊變量有2k-1個(gè)0（或1）表現(xiàn)值。若設(shè)定0（或1）為這個(gè)變量值，那么這個(gè)變量的表現(xiàn)值為1（或0）的子句，不考慮這個(gè)變量不構(gòu)成完全塊，反之，為0（或1）子句就構(gòu)成完全塊。因此，變量的2k-1個(gè)0（或1）表現(xiàn)值是變量唯一解。證畢。

定義4 子句塊通過相同變量關(guān)聯(lián)組成關(guān)聯(lián)段。

定義5 設(shè)定變量值，依據(jù)定理2消去子句，若關(guān)聯(lián)段剩余子句塊沒有變量矛盾值，則稱設(shè)定值為這個(gè)變量的可選解。

表3是依據(jù)定理2，對(duì)表1設(shè)定x9=1，x10=0消去相關(guān)子句后，得到的剩余部分（淺灰色列已設(shè)定）。這部分均沒有子句塊的變量唯一解，于是需要測(cè)試變量的可選解。

令x1=1，考慮消去子句（橫向紋理所示）后，出現(xiàn)x3在子句塊x2x3中有唯一解0，而在子句塊x3x4中有唯一解1，如此一來，無論如何都不可能確定x3的值使CNF=1。說明x1沒有可選解1。

表3 x1=1不是可選解

再對(duì)x1測(cè)試可選解0，沒有出現(xiàn)變量值矛盾的情況。說明0是變量x1的唯一解。設(shè)定x1=0，消去相關(guān)的子句，就得到了可以繼續(xù)求解的表4。

表4 設(shè)定變量唯一解消去子句

2 子句消去法求解與驗(yàn)證

有了變量唯一解和變量可選解的概念，就可以通過先設(shè)定它們的值，求出CNF=1的滿足解。

2.1 基本規(guī)則

用子句消去法求CNF=1的滿足解要用到兩條規(guī)則。

規(guī)則1：子句塊變量有唯一解必須首先設(shè)定。

依據(jù)定理2，表1中的子句塊x10和子句塊x8x9有唯一解x10=0和x9=1，消去值為1的那些子句，就得到表3（不包括左上角的x1=1）。

規(guī)則2：變量有唯一可選解必須優(yōu)先設(shè)定。

通過表3對(duì)x1=1的檢測(cè)可知，1不是這個(gè)變量的可選解。同理檢測(cè)可知x1=0是可選解。則設(shè)定x1=0，消去相關(guān)子句，得到表4后還可繼續(xù)求解。

2.2 快速判定可選解

表4中剩下的子句塊中沒有變量唯一解，需要像測(cè)試x1一樣，檢查這些變量是否有唯一可選解。這個(gè)過程實(shí)際上無需檢測(cè)所有變量。

引理1 若非完全塊中沒有變量唯一解，則至少?zèng)]有一對(duì)互反子句。

證明：在k個(gè)變量的非完全塊中，沒有變量唯一解也即無任一變量有2k-1個(gè)相同表現(xiàn)值，從完全塊可知，這至少要有一對(duì)互反子句不存在方可。

引理2 不在子句塊中互反子句的任意一個(gè)作為塊變量值，都可使子句塊的全部子句值為1。

證明：因?yàn)樽泳鋲K中的子句都不是這對(duì)互反子句的反子句，那么至少有一個(gè)位置的數(shù)碼與它們相同。因而用這對(duì)互反子句的任意一個(gè)作為子句塊變量設(shè)定值，都可使子句塊的全部子句值為1。

引理3 CNF=1有解，這個(gè)解也是子集的解。

證明：顯然，CNF=1的解使每個(gè)子句值為1，因而這個(gè)CNF的子集子句的值也都是1。

定義6 檢測(cè)變量可選解所涉及的關(guān)聯(lián)段稱為變量關(guān)聯(lián)段。

定理3 沒有變量唯一解的非完全塊，非關(guān)聯(lián)變量都有2個(gè)可選解。

證明：根據(jù)引理1，沒有變量唯一解的非完全塊，一定有互反子句能夠消去這個(gè)子句塊的全部子句。那么，非關(guān)聯(lián)變量不論設(shè)定0或1值，都只消去本子句塊的子句，與其它子句塊無關(guān)，因而不會(huì)出現(xiàn)剩余完全塊，知此定理成立。

定理3減少了要判斷可選解變量的數(shù)量，提高了計(jì)算速度。

定理4 每個(gè)變量都有2個(gè)可選解的CNF，任選一個(gè)變量設(shè)定值，消去剩余子句塊變量唯一解子句，最終可得CNF=1的解。

證明：根據(jù)變量關(guān)聯(lián)段的定義，設(shè)定一個(gè)變量可選解，消去一些子句，未被消去變量的關(guān)聯(lián)段剩下了原變量關(guān)聯(lián)段的子集，依據(jù)引理3，這并不影響剩余變量的可選解數(shù)量。因而可再如此設(shè)定剩余變量的值，消去相關(guān)子句，最終可得CNF=1的滿足解。

2.3 子句消去法解題

根據(jù)規(guī)則1和規(guī)則2，以及定理4，很容易計(jì)算出SAT的滿足解。作為例子，繼續(xù)計(jì)算最初表1給出的CNF=1的滿足解。

通過檢驗(yàn)知，關(guān)聯(lián)變量x3和x6都有2個(gè)可選解。則依據(jù)定理3知，所有的剩余變量都有2個(gè)可選解。為此任意設(shè)定x3=0，得到x2唯一解0，消去相關(guān)子句后得到表5。

表5 x3=0，x2=0消去相關(guān)子句

表5剩下的變量仍然都有2個(gè)可選解，繼續(xù)設(shè)定x6=1，消去子句。進(jìn)而得到x5=0這個(gè)變量唯一解。消去相關(guān)子句，得到表6。

表6 x6=1，x5=0消去相關(guān)子句

最終可設(shè)定x7=1，或者x8=0消去相關(guān)子句，得到最后的滿足解如表7上方一行所示，*號(hào)表示該變量取值0或1均可。

2.4 CNF=1滿足解驗(yàn)證

對(duì)于子句消去法計(jì)算得到的全體變量值是否是CNF=1的解，是可以驗(yàn)證的。一種辦法是將每個(gè)變量求出的值（*可以任意取值0或1），代入CNF的邏輯表達(dá)式，檢驗(yàn)最終結(jié)果是否是CNF=1。

表7 CNF=1的解驗(yàn)證

不妨介紹一個(gè)簡(jiǎn)單的驗(yàn)證方法，即將所求解值置入原題（表1）的上面，檢驗(yàn)每一行是否有與其變量值相同的子句表現(xiàn)值。若有，則將子句消去，若最終沒有子句剩下，就說明得到的解完全正確。

本題如果x7不選，令x8=0，也可將全部子句消去，從而完成解的驗(yàn)證。

3 結(jié)論

本文介紹的子句消去法可以保證快速計(jì)算出SAT問題的一組滿足解，而不是全部解。當(dāng)然全解也可用子句消去法求出，只是還要引入新的概念。

SAT問題長(zhǎng)期未能找到確定的解題方法，是未能找到其特殊的結(jié)構(gòu)規(guī)律造成的。子句消去法找到了CNF的結(jié)構(gòu)特點(diǎn)，遵循首先確定變量唯一解，其次在變量普遍有2個(gè)可選解的情況下，確定出后續(xù)變量解，從而完全以確定的方式實(shí)現(xiàn)了CNF=1滿足解的計(jì)算。

SAT問題是NP-complete類問題，按照學(xué)術(shù)界的觀點(diǎn)，找到了SAT問題的多項(xiàng)式時(shí)間復(fù)雜度算法，就等于證明了NP=P。

本文的主題是介紹計(jì)算求出SAT滿足解的方法，它適應(yīng)任何SAT問題求解。關(guān)于子句消去法是否是O(nk+1)多項(xiàng)式時(shí)間復(fù)雜度算法，請(qǐng)參考文獻(xiàn)[6]，本文不予討論。

[1]P versus NP problem. https://en.wikipedia.org/wiki/P_versus_ NP_problem [OL].

[2]Cook S A. The complexity of theorem-proving procedures[C]// ACM Symposium on Theory of Computing. ACM, 1971:151-158.

[3]Stephen Cook. https://en.wikipedia.org/wiki/Stephen_Cook [OL].

[4]Boolean satisfiability problem. https://en.wikipedia.org/wiki/ Boolean_satisfability_problem [OL].

[5]姜詠江. 自己設(shè)計(jì)制作CPU與單片機(jī)[M]. 北京: 人民郵電出版社, 2014: 237-243.

[6]姜詠江. 論子句消去算法的多項(xiàng)式時(shí)間復(fù)雜度. http://blog. sciencenet.cn/blog-340399-1011907.html [EB/OL].

姜詠江（1945-），通訊作者，男，北京人，退休教師，中國(guó)計(jì)算機(jī)學(xué)會(huì)、中國(guó)電子學(xué)會(huì)高級(jí)會(huì)員。研究方向：數(shù)學(xué)、計(jì)算機(jī)科學(xué)。

Email: accsys@126.com

陳躍（1977-），男，北京人，西安交通大學(xué)博士，中國(guó)計(jì)算機(jī)學(xué)會(huì)會(huì)員。主要研究方向：大數(shù)據(jù)與機(jī)器學(xué)習(xí)、分布式計(jì)算。

Email: scottchen@163.com

A Fast Solution for SAT Problem based on Clause Elimination Method

JIANG Yong-jiang1, CHEN Yue2

(1. University of International Business and Economics, Chaoyang, Beijing,100013, China; 2. Xi’an Jiaotong University, Xi’an, Shanxi,710000, China)

Boolean satisfaction problem (SAT) is one of the fundamental problems that was proven to be NP-complete, which involves obtaining fast solution for various fields including integrated circuit design and optimization, biological gene, artificial intelligence and Internet. By using the concepts including Fix-bit number, Clause-block and Relate-section, a clause elimination method is discovered using the determination rule that aims at rapidly obtaining satisfied solution for SAT. A new way is found out for the solution of pure discrete variables.

SAT problem; Fix-bit Number; Clause Elimination Method; Clause-block; Relate-section; Polynomial Time Complexity

TP301.6；O158

A

2095-8412 (2016) 06-1255-05

10.14103/j.issn.2095-8412.2016.06.055