可滿足性問(wèn)題的充分必要條件

1、中苗科技200712可滿足性問(wèn)題的充分必要條件郭成(淮爭(zhēng)工孕Itlt理科學(xué)從.江蘇連云港222005)M鼻：可溝足鼻問(wèn)題是計(jì)算機(jī)和人工智能領(lǐng)城內(nèi)的一個(gè)*要的冋豪.是杲一個(gè)祓證明是NPC的問(wèn)是.*丈主矣杞子句皋邊行分給出轉(zhuǎn)定義、角草集定義，轉(zhuǎn)同構(gòu)定義.畀且證胡轉(zhuǎn)同構(gòu)不凍變子句集的可満足性.論丈證明了可満足子句舉的三個(gè)尢矣*件.并且it些尢要條件才以用于判斷可溝足問(wèn)懇的完仝搜索和不完金搜索算決.關(guān)子句集；賦值；樓；兩草集；*)#；轉(zhuǎn)同構(gòu)Sufficientandnecessaryczditk心forSAT.GUOCheng(MathematicsandPhysicsDepartmentHuaiHa

2、iInWMecftechnology,JiangSu,LianYunGang222005)Abstract:SatisfiabilityproblemsbbrevuttedtoSTicaveryimportantproblemincomputerscienceandartificialintelligenceandisfirstlyprovediobtaNPCproblemInthispaper,thesetsofclausesareresearched,givingthedeGnitionsofflipping,simplesetsofclausesandflippingisomorphis

3、m.Moreover,Iprovethatflippingdoesn9taffectthesatisfiabilityofasetofclausesandthreesufficientandnecessaryconditionsareproved.Intheendofthispaper,itissimplydiscussedthattheseconditionscanbeutilizedincompletealgorithmandincompletealgorithmofSAT.Keywords:setsofclausesiassignment,modelssimplesetsiflippin

4、glflippingisomorphism1引畝可滿足性問(wèn)題(satisfiabilityproblem,簡(jiǎn)稱SAT)是指合取范式的可滿足性問(wèn)題.簡(jiǎn)單可以敘述為，對(duì)于個(gè)合適公式.通常我們假定已經(jīng)轉(zhuǎn)化為CNF的形式.即一個(gè)合取范式.那么是否有一個(gè)算法能在多項(xiàng)式的時(shí)間內(nèi)找到該公式的一個(gè)賦值，使的其真值為真嗎？邏輯公式的可滿足性判定是計(jì)算機(jī)和人工智能領(lǐng)域內(nèi)的一個(gè)重要的問(wèn)題，解決SAT問(wèn)題對(duì)解決數(shù)學(xué)、計(jì)算機(jī)科學(xué).電子工程技術(shù)中的些實(shí)際問(wèn)題都有非常柬要的意義對(duì)于可滿足性SAT問(wèn)題.己經(jīng)被證明是一個(gè)NPC問(wèn)題，并且是第一個(gè)被證明是NPC問(wèn)題，詳見(jiàn)文獻(xiàn)命題原子。表朋命題的符號(hào)，用小寫(xiě)字母表示。文字。甜題原子

5、和命題原子的否定統(tǒng)稱為文字.命聽(tīng)原子稱為正文字.命題原子的否定稱為負(fù)文字。例如P為命題原子.同時(shí)也是一個(gè)止文字.-P為命題原子P的否定，同時(shí)也是一個(gè)負(fù)文字。子句有限個(gè)文字的析取.例如，子句。子句集有限個(gè)子句構(gòu)成的集合.命題原子集。一個(gè)子句集中的所有的原子的集合.賦值命毬原子集到集合P的映射，T表示真值為真.F茨示真值為假?？蓾M足模。對(duì)于一個(gè)子句集S.如果存在一個(gè)賦值中使得S中的每個(gè)子句在該賦值下的真值為真，那么稱S是可滿足的.并且稱賦值中為S的一個(gè)模.例如：子句集S=p,V-V2VV祁22祁”-7rp小F、PVp2Vpj命題原子集合*P|，PPJ賦值中I:Vi(Pi)=7,Vl(p2)=7，V

6、i(P)=賦值幻:V1(A)-7.V|(P2)-Ftvl(p3)=7其中在賦值中2下，S中的每個(gè)子句真值為真，所以幻是S的一個(gè)模。顯然，如果一個(gè)子句集S的命題原子集A中的原子個(gè)數(shù)為n,那么S的不同賦值的數(shù)目為2J判斷S是否可満足，可以通過(guò)鯊證2個(gè)賦值中.哪個(gè)是其模.這樣最壞的情況是要驗(yàn)證2次顯然這樣的算法量壞復(fù)雜度為2J比如，不可滿足子句集便需要全部驗(yàn)證完畢才能給出結(jié)論.到目前為止.判定SAT問(wèn)題算法最壞的情況都是指數(shù)的，不過(guò)算法平均意義上是多項(xiàng)式的，見(jiàn)文獻(xiàn)叫對(duì)于2-SAT問(wèn)JS有線性的時(shí)間復(fù)雜度的算法，對(duì)于Horn子句集，己經(jīng)有線性的時(shí)間復(fù)雜度的算法，見(jiàn)文獻(xiàn)2可満足子旬集的件2.1關(guān)轉(zhuǎn)同構(gòu)收

7、稿日期：2007-11-15修回日期：2007-12-04墓金項(xiàng)目：淮海工學(xué)院校內(nèi)基金(項(xiàng)目號(hào):I200532)作看簡(jiǎn)介：郭成(1972-),男.漢族.河北懷安.碩士研究生.應(yīng)用數(shù)學(xué)。定義1翻轉(zhuǎn)P如果s中有子句包含有文字P,則把P改寫(xiě)為如果S中有子句包含rp.則把改寫(xiě)成P,稱翻轉(zhuǎn)P。若詡轉(zhuǎn)I中的每個(gè)原子，稱翻轉(zhuǎn)1例1.S=p,V-ip,Vp,-ip,Vp,V-p,p,Vp,Vp,1=PPjo若翻轉(zhuǎn)P,則可以由s得到一個(gè)新的子句集s：s=(-p*-papP,Vpf,-,p(Vp：VpJ.若翻轉(zhuǎn)I,則可以由s得到一個(gè)新的子句集s“，并且s=(PfVp2-IP,V-ip2Vp,p,v-in.,Vp,

8、o定理1若S為個(gè)子句IA,翻轉(zhuǎn)T,得到-個(gè)新的子句集S,則S町滿足當(dāng)冃.僅當(dāng)S可滿足。證明：必要性證明，即S可滿足，證明S可滿足。因?yàn)镾可滿足，令W為S的一個(gè)模。由中構(gòu)造S的一個(gè)賦值2:弋pwAV(p)=7.如果pe/,v(p)=F:中(P)=F.如果pe/,v(P)=7:V(P)=V(P)f如果卜面證明中為s的模。令c是s中的任意-個(gè)子句，則S中的一定存在子句C,翻轉(zhuǎn)I時(shí)，由C得到。2為5的模.C在V下的真值為真.則C中有文字L,L在w下真值為真。如果L為正文字P,則V(P)=7如果則中P在C中.翻轉(zhuǎn)I.P被SS轉(zhuǎn)，rtic得到c；所以c中有負(fù)文字所以c在中下的真值為真。如果PW則w(p)7

9、(p27。P在C中.翻轉(zhuǎn)I,P沒(méi)有被翻轉(zhuǎn).由C得到C；所以C中有正文字P.所以C在中下的真值為真。如果L為負(fù)文字卡，則W(P2F,如果pwl.則V(P)=7e-P在C中，翻轉(zhuǎn)1.P被朋轉(zhuǎn)，由C得到C；所以C*有止文字P,所以C在W卜的真值為真。如果P電I則V(P)=M/(P)-A。在C中.翻轉(zhuǎn)I.P沒(méi)佇被翻轉(zhuǎn).由c得到C；所以C中有負(fù)文字F,所以C在/下的真值為真。由上可知.對(duì)FS中的任氫個(gè)子句C在w卜賓值為真。所以“為S的一個(gè)模。充分性證明.即S可滿足.證明S可滿足。s可滿足.令中為s的一個(gè)模。由中構(gòu)造S的一個(gè)賦值中:PP如果,V(p)-F:W(P)=F,如果pw/,V(p)=7:V(P)=

10、V(p).如果poF面證明w為S的模。令(:是s中的任意一個(gè)子句.亂轉(zhuǎn)I,由c得到s中的了句c：0為S的一個(gè)模.c在中F的真值為真.則c中有文字L,L在/下的真值為真。如果L為正艾字F.則w27.如境Pf則wWfP在c中.轉(zhuǎn)I.P被18轉(zhuǎn).由C甬到0斫以C中有負(fù)文字4所以下的真值為如果pJ,則WS2中(刃二7。P在C中，翻轉(zhuǎn)1,P沒(méi)有被詡轉(zhuǎn).由c得到c.所以c中冇正文字p,所以crr：w卜的真值為真。如果L為負(fù)文則v(p)=F.如果,則V(P)=7。在C中，翻轉(zhuǎn)I,P被翻轉(zhuǎn)，由C得到C；所以C中有止文字P,所以C在w卜的真值為真。如果pel則v(P)-v(P)=oPACK翻轉(zhuǎn)Ip沒(méi)有被翻轉(zhuǎn).由

11、C得到C：所以C中有負(fù)文字rp.所以C在中卜的真值為真。由卜-可知.對(duì)于s中的任意-個(gè)子hjc在中卜真值為真.所以中為S的一個(gè)模。證明完畢。曲定理1可知，翻轉(zhuǎn)不會(huì)彩響一個(gè)了句集的可滿足性。并且如果子句集S翻轉(zhuǎn)I得到子句集S；則子句集S也町以翻轉(zhuǎn)I得到子句集S。由此給出如下定義：定義2如果f句集S通過(guò)翻轉(zhuǎn)1得到子句集S；則稱這兩個(gè)子句集是翻轉(zhuǎn)同構(gòu)的。2.2簡(jiǎn)單集定義3簡(jiǎn)單集正簡(jiǎn)單集如果S中的每個(gè)子句都至少包含冇個(gè)正文字.則稱S為正簡(jiǎn)單集。例如PZ祁二VPv-Plvp：vrPp(vp?V為一八正簡(jiǎn)單集。負(fù)簡(jiǎn)單集如果S中的每個(gè)f句都至少包含有一個(gè)負(fù)文字，則稱S為負(fù)簡(jiǎn)單集。例如，為一個(gè)負(fù)簡(jiǎn)單集；止簡(jiǎn)單

12、集和負(fù)簡(jiǎn)單集統(tǒng)稱為簡(jiǎn)單集中科技200712定理2S如果為一個(gè)簡(jiǎn)單集，則S為可滿足的.證明：如果S為一個(gè)正簡(jiǎn)單集，則給出S的賦值v：v(p)=75，由于S中的每一個(gè)子句都有正文字，所以每個(gè)子句在賦值w下的真值為真，即賦值w為S的一個(gè)模，S可滿足.如果S為一個(gè)負(fù)簡(jiǎn)單集，則給出S的賦值v：v(P)=FgA,由于S中的每一個(gè)子句都有負(fù)文字，所以每個(gè)子句在賦值w下的真值為真，即賦值w為S的一個(gè)模，S可滿足.2.3三個(gè)充豪條件定理3S是可滿足的充要條件是S翻轉(zhuǎn)同構(gòu)一個(gè)負(fù)簡(jiǎn)單集.證明：充分性的證明.若SIB轉(zhuǎn)同構(gòu)一個(gè)負(fù)簡(jiǎn)唯集，由定理2,負(fù)簡(jiǎn)單集可滿足，由定理1可知，S可滿足.必要性的證明.由于S可滿足，則存

13、在使得S可滿足的一個(gè)模中.令/=plw(p)=7,pw/,翻轉(zhuǎn)I，則得到一個(gè)子句集S；下面證明S為一個(gè)負(fù)簡(jiǎn)單集.對(duì)于S中的任意一個(gè)子句C；由于S是翻轉(zhuǎn)1御到，故一定存在S中的子句C,翻轉(zhuǎn)I,由C得到C.V是s的一個(gè)模，所以C在W下的真值為真，所以C中有文字L,在中下L的真值為真.a)L是一個(gè)正文字P,w(p)=7,則p“，所以P被翻轉(zhuǎn)，因此C中有負(fù)文字B)L是一個(gè)負(fù)文字，叭則p軽/,所以沒(méi)有IH轉(zhuǎn)P,因此C中有負(fù)文字卩。所以中的任意一個(gè)子句都有一個(gè)負(fù)文字，故咼一個(gè)負(fù)簡(jiǎn)單集。定理4S是可滿足的充要條件是S翻轉(zhuǎn)同構(gòu)一個(gè)正簡(jiǎn)單集.證明：(1)充分性的證明.若SIB轉(zhuǎn)同構(gòu)一個(gè)負(fù)簡(jiǎn)單集，由定理2,負(fù)簡(jiǎn)單

14、集可滿足，由定理1可知，S可滿足.(2)必要性的證明.由干S可滿足，則存在使得S可滿足的一個(gè)模*令/plW(P)F,peQ8翻轉(zhuǎn)I,則得到一個(gè)子句集S；下面證明S為一個(gè)正簡(jiǎn)單集.對(duì)于S中的任意一個(gè)子句C,由于S超19轉(zhuǎn)得到，故一定存在S中的子句C,翻轉(zhuǎn)I,由C得到CV是S的一個(gè)模，所以C在W下的真值為真，所以C中有文字L,在中下L的真值為真.C)L是一個(gè)正文字P理(P”匚則P“，所以P沒(méi)有被翻轉(zhuǎn)，蟲(chóng)此C中有正文孑PG).是一個(gè)魚(yú)文字幾中(刃=尸，則P,所以P被製轉(zhuǎn)，因此C*肴正文字P所以s中的任意一個(gè)子句c都有一個(gè)正文字，故s是一個(gè)正簡(jiǎn)單集.由定理3和定理4可以得到：定理5S是可滿足的充要條件

15、是S8轉(zhuǎn)同構(gòu)一個(gè)簡(jiǎn)單集.3剜初轉(zhuǎn)不改變子句集合的可滿足性，可滿足子句集翻轉(zhuǎn)同構(gòu)簡(jiǎn)單集.利用本文給出的充娶條件，可以判斷一個(gè)子句集是否為可滿足的，并且可以用來(lái)給出對(duì)子句集的模的不完全技索算法，也可以給出完全搜第算法，本文只是證明三個(gè)充要條件，由于篇幅，算法具體問(wèn)題不進(jìn)行詳細(xì)具體討論.希文敵：L1JSACookThecoaplexityoftheorerprovingprocedure(JACMS/BposiusonTheoryofcomputing,1971(3):151-158S.Ben-Davis.B.Chor,0.Goldre)chfHLuby.OnthetheoryofaveragecasecoplexityJJof*CoaputerandSystemsSciences,1992(44):193-219B.AspvalltM.F.Plass.R.E.TarianALinear-tinealgorithafortestingthetruthofcertainquantifiedBooleanforulas(刀IPL.】9798(3):121-123W.F.Dowling,J.H.