基于集合理論的SAT算法的設(shè)計(jì)與實(shí)現(xiàn).pdf

1、SAT是理論計(jì)算機(jī)科學(xué)中的一個(gè)經(jīng)典問(wèn)題，也是被發(fā)現(xiàn)的第一個(gè)NP完全問(wèn)題。SAT問(wèn)題是對(duì)于給定的一個(gè)布爾邏輯表達(dá)式在SAT問(wèn)題可滿(mǎn)足的情況下給出一組解，使得該布爾邏輯表達(dá)式為“真”；在給定問(wèn)題不可滿(mǎn)足的情況下給出證明。比較著名的高效SAT求解算法有MiNiSat、zchaff Grasp等。SAT求解算法廣泛應(yīng)用于實(shí)際生活中的各種領(lǐng)域，如電路設(shè)計(jì)的形式化驗(yàn)證、人工智能、資源調(diào)度等。雖然SAT求解算法的研究已經(jīng)相當(dāng)成熟，但它仍然是實(shí)際應(yīng)用領(lǐng)

2、域中必須打破的一個(gè)瓶頸。例如在電路設(shè)計(jì)的形式化驗(yàn)證中，將電路中的變量轉(zhuǎn)化為布爾邏輯的合取范式形式(Conjunctive Normal Form簡(jiǎn)稱(chēng)CNF)，再應(yīng)用SAT求解來(lái)檢測(cè)電路故障，傳統(tǒng)算法往往要占用很長(zhǎng)時(shí)間和大量的內(nèi)存，而最后往往還不能得到滿(mǎn)意的結(jié)果。所以到目前為止，眾多國(guó)內(nèi)外學(xué)者層出不窮的推出新型算法來(lái)提高計(jì)算效率，以便高效地應(yīng)用于各行各業(yè)。 雖然命題邏輯的理論研究已經(jīng)相當(dāng)成熟，但是在SAT問(wèn)題及其算法被越來(lái)越多地應(yīng)

3、用到現(xiàn)實(shí)世界的生產(chǎn)和生活中的今天，探尋命題邏輯可滿(mǎn)足性判定的高效算法仍然是一個(gè)令人興奮的方向。SAT問(wèn)題的解決方法一般分為兩類(lèi)：完備算法和不完備算法，它們的典型代表是Davis-Putnam提出的基于回溯搜索的DPLL算法和本地啟發(fā)式搜索。當(dāng)今流行的SAT算法主要是完備算法或在DPLL算法基礎(chǔ)上的改進(jìn)和衍生。 本文在對(duì)現(xiàn)有的SAT問(wèn)題相關(guān)理論的研究以及算法分析的基礎(chǔ)上，基于DPLL算法結(jié)合集合理論提出了一種新型的SAT算法。具有