SMT求解器增強(qiáng)技術(shù)的研究.pdf

1、在計(jì)算機(jī)集成電路不斷飛速發(fā)展的信息時(shí)代，無論計(jì)算機(jī)的硬件還是軟件設(shè)計(jì)的復(fù)雜度都在不斷提高，也對(duì)開發(fā)設(shè)計(jì)提出了新的挑戰(zhàn)，尤其是在保證新產(chǎn)品的安全性、可靠性和正確性方面。為了解決該難題，將計(jì)算機(jī)輔助設(shè)計(jì)概念引入測(cè)試、驗(yàn)證等領(lǐng)域逐漸形成了新的技術(shù)發(fā)展趨勢(shì)。而可滿足性問題，包括SAT和SMT兩方面已經(jīng)成為最近10年中的研究熱點(diǎn)。與其相關(guān)的技術(shù)都在不斷發(fā)展中得到了性能的提高和功能的完善。在發(fā)展的同時(shí)SMT求解器可在許多新的領(lǐng)域得到了應(yīng)用，優(yōu)化問題

2、則是其中的重要的領(lǐng)域。因此，本文就可滿足性求解技術(shù)的增強(qiáng)以及該種技術(shù)與優(yōu)化問題如何結(jié)合等問題做了如下研究：
　　 1．研究已有的沖突分析算法，設(shè)計(jì)新的沖突分析和學(xué)習(xí)算法。該種算法旨在使用盡量少的沖突節(jié)點(diǎn)，產(chǎn)生出更為有效且更加簡(jiǎn)潔的沖突分析子句。求解器可以根據(jù)這些包含更多信息的沖突分析子句在后續(xù)搜索中更加有效地避免沖突，以便更快的得到計(jì)算結(jié)果。
　　 2．研究相關(guān)的預(yù)處理算法，并對(duì)其有所改進(jìn)。新設(shè)計(jì)預(yù)處理算法主要是為了在正

3、式開始求解過程之前，對(duì)已有的CNF進(jìn)行化簡(jiǎn)。由于現(xiàn)在流行的可滿足性求解器的設(shè)計(jì)特點(diǎn)，其效率的高低對(duì)各個(gè)變量之間的邏輯關(guān)系的表達(dá)方式有著很強(qiáng)的依賴性，例如在CNF的子句中有大量的斷言了句并且每個(gè)子句中所包含的文字盡量少會(huì)對(duì)快速解決問題有很大幫助。這也是本文所設(shè)計(jì)算法的出發(fā)點(diǎn)。
　　 3．研究設(shè)計(jì)了一種將SMT求解應(yīng)用于最憂化問題的方法，使得原有的SMT求解器可以解決一定形式的最優(yōu)化問題，并對(duì)其進(jìn)行計(jì)算。該方法是使用數(shù)學(xué)中有關(guān)多元函