結(jié)合AIG和兩變量觀測(cè)策略的SAT滿(mǎn)足性算法

摘要： 現(xiàn)今,布爾可滿(mǎn)足性(SAT)解算器已在工業(yè)電路驗(yàn)證過(guò)程中得到了廣泛的應(yīng)用。大多數(shù)SAT解算器是基于DPLL算法來(lái)構(gòu)造的,需要電路輸入形式是合取范式(CNF)的形式。CNF形式的構(gòu)建會(huì)使電路表示正交化,但通常會(huì)產(chǎn)生更多的額外變量,同時(shí)也會(huì)破壞電路的原始結(jié)構(gòu)信息,在使用DPLL算法搜索整個(gè)變量空間的時(shí)候需要大量的時(shí)間消耗。本文提出了一些方法來(lái)解決這些問(wèn)題。首先使用與/非門(mén)(AIG)來(lái)簡(jiǎn)化待驗(yàn)證電路,然后在基于CNF的兩變量觀測(cè)策略上,結(jié)合合取范式CNF和析取范式DNF的圖特性來(lái)改善DPLL搜索過(guò)程,加速布爾約束推導(dǎo)(BCP)的進(jìn)行。針對(duì)ISCAS85電路的驗(yàn)證結(jié)果驗(yàn)證了本算法的有效性。 （共5頁(yè)）