基于CDCL的SAT問題求解算法研究.pdf

1、人工智能領(lǐng)域中，研究命題邏輯公式的可滿足性(SAT)問題具有十分重要的作用。隨著科學(xué)、技術(shù)、社會(huì)等領(lǐng)域的發(fā)展，需要解決的SAT問題的規(guī)模變得越來越大，而傳統(tǒng)單一的算法無法適應(yīng)這些大規(guī)模的SAT問題。因此一些針對(duì)大規(guī)模的SAT問題的求解器應(yīng)運(yùn)而生，如Chaff、zChaff、 Minisat、Lingeling等諸多著名求解器。這些求解器都并非由單一的算法構(gòu)建，而是在傳統(tǒng)的DPLL等算法的基礎(chǔ)上構(gòu)建的一套系統(tǒng)，如CDCL求解器，其包含多個(gè)

2、決策過程，在算法過程中不斷的改進(jìn)學(xué)習(xí)和調(diào)整，以更為高效的解大規(guī)模的SAT問題。這些求解器主要分為如下幾個(gè)部分，分別是變量決策、沖突分析、子句學(xué)習(xí)和回溯機(jī)制。而其中的變量決策過程在整個(gè)算法構(gòu)架中占有十分重要的地位，一個(gè)好的變量決策策略可以減少?zèng)_突的產(chǎn)生，大量節(jié)省求解時(shí)間，因此研究變量決策過程的策略具有較為重要的意義。本文主要結(jié)合CDCL求解器構(gòu)架，做了如下幾個(gè)方面的研究工作:
　　1、本文提出一種啟發(fā)式策略，根據(jù)所給子句、文字?jǐn)?shù)量和