可滿足性問(wèn)題的預(yù)處理策略研究與分析.pdf

1、可滿足性問(wèn)題（即SAT問(wèn)題）是第一個(gè)被證明的經(jīng)典NP問(wèn)題。人們一直致力于如何在有限的時(shí)間求解可滿足性問(wèn)題。隨著現(xiàn)實(shí)世界中可滿足性問(wèn)題的規(guī)模逐漸增長(zhǎng)，預(yù)處理技術(shù)已經(jīng)逐漸受到重視。由于其良好的簡(jiǎn)化效果，變量消除算法已經(jīng)應(yīng)用于多種預(yù)處理器中。作為一種輕量級(jí)預(yù)處理技術(shù)，變量消除算法的簡(jiǎn)化效果與其消除過(guò)程中的約束條件有著直接聯(lián)系。
　　為了進(jìn)一步提高和優(yōu)化變量消除算法的預(yù)處理性能，本文對(duì)比研究了在不同的約束條件下變量消除算法的簡(jiǎn)化性能以及簡(jiǎn)

2、化后的CNF實(shí)例的求解效果，同時(shí)設(shè)計(jì)了一種基于子句文字長(zhǎng)度動(dòng)態(tài)約束的變量消除算法。與分解前的子句文字長(zhǎng)度相比，只有當(dāng)分解后的子句集合的文字長(zhǎng)度減少時(shí)，該算法完成變量消除替換過(guò)程。為了減少變量消除算法中無(wú)價(jià)值計(jì)算，該算法引入了動(dòng)態(tài)約束機(jī)制，大大縮短了預(yù)處理時(shí)間，進(jìn)一步提高簡(jiǎn)化性能。本文在該算法的基礎(chǔ)上，基于MiniSat的開(kāi)源代碼實(shí)現(xiàn)了一個(gè)可滿足性問(wèn)題的預(yù)處理器 MiniSat BFS。除了通過(guò)常規(guī)的性能指標(biāo)來(lái)對(duì)比分析兩種不同約束條件下變