命題邏輯中隨機(jī)3-SAT問題算法研究.pdf

1、命題邏輯公式的可滿足性問題(SAT)是計算機(jī)科學(xué)和人工智能中一個重要問題。它是第一個被證明了的NP完全問題，由Stephen Cook于1971年提出。SAT問題在人工智能、軟件工程、VLSI集成電路設(shè)計等領(lǐng)域具有廣泛的應(yīng)用。3-SAT問題是每個子句的文字個數(shù)固定為3的SAT問題。作為SAT問題的子問題之一，3-SAT問題也是NP完全問題。3-SAT問題有來自工業(yè)問題轉(zhuǎn)化的實際問題，也有機(jī)器自動生成的。來自工業(yè)問題轉(zhuǎn)化的3-SAT問題在

2、數(shù)目和結(jié)構(gòu)上都有很大的限制，根本不能滿足各類SAT算法的測試需求，所以目前大部分的3-SAT問題來自機(jī)器自動生成，這類問題又稱為隨機(jī)3-SAT問題。當(dāng)變元的數(shù)目達(dá)到1000乃至1兆的規(guī)模時，3-SAT問題的求解變得異常困難，所以對大規(guī)模隨機(jī)3-SAT的求解是一個比較有前景的研究領(lǐng)域。
　　自從20世紀(jì)80年代隨機(jī)3-SAT問題被提出以來，很多學(xué)者在這方面做了大量的工作，提出了各種各樣的算法。當(dāng)前較為高效的算法有Sparrow201

3、1算法、ProbSAT算法、CCMC算法等。然而這些算法，在求解較大規(guī)模的隨機(jī)3-SAT問題上的效率仍不夠理想。
　　本文在綜合分析以往SAT問題算法的基礎(chǔ)上，在提高隨機(jī)3-SAT問題的求解效率方面主要做了如下工作:
　　1、基于SAT問題的自身結(jié)構(gòu)，研究各個文字在子句集中出現(xiàn)的頻率，挖掘出文字與子句集可滿足性判定的關(guān)系。給出文字的關(guān)鍵度和關(guān)鍵文字的概念，利用關(guān)鍵文字規(guī)則和DPLL規(guī)則設(shè)計出了對子句集初始真值指派的優(yōu)化策略。