SMT全解求解器為許多研究領(lǐng)域提供輔助,但現(xiàn)有的SMT全解求解器在速度、內(nèi)存消耗或者支持的求解類型方面存在局限性。首先,提出了求解器的4種新的潛在應(yīng)用;其次,設(shè)計(jì)了一種基于二分查找(Binary Search,BS)的新型求解器,可以支持多種求解類型,同時(shí),結(jié)合上下文感知(Context Aware,CA)機(jī)制來(lái)提升求解器的速度,并通過(guò)暫�；謴�(fù)(Suspend Resume,SR)機(jī)制降低內(nèi)存消耗。初步試驗(yàn)表明,BS、BS+CA、BS+SR和所提方法分別能將傳統(tǒng)的阻塞子句方法(Blocking Clauses Method,BCM)的求解速度提高了4.6倍、13.4倍、7.3倍以及32.4倍;與BCM相比,提出的方案的內(nèi)存消耗降低至35.3%。此外,試驗(yàn)結(jié)果表明,可以通過(guò)并行化進(jìn)一步提升方案的性能。

【文章頁(yè)數(shù)】：7 頁(yè)

【部分圖文】：

圖1 一個(gè)例子闡述二分查找

提出的BS方法和上述方法一樣，通過(guò)求解φ產(chǎn)生與上述方法相同的第一個(gè)模型m0。隨后產(chǎn)生6個(gè)公式φ1～φ6對(duì)應(yīng)6個(gè)任務(wù)動(dòng)態(tài)劃分搜素空間，如圖1所示，如φ6=φ∧((x==50)∧(y==50)∧(z>50))。增量子句來(lái)描述子空間邊界，如x<50表示子空間：

圖2 式（3）的模型數(shù)量

圖3表明基于BS和BD+CA求解器隨著時(shí)間增加持續(xù)增加內(nèi)存開銷，BCM沒有明顯增加內(nèi)存開銷，這是由于BCM求解器會(huì)變得很慢導(dǎo)致的，如圖2所示。圖3式（3）的內(nèi)存消耗

圖3 式（3）的內(nèi)存消耗

圖2式（3）的模型數(shù)量表1和圖3表明，基于BS+CA的求解器比基于BS的求解器需要消耗更多的內(nèi)存（BS+CA的為4.4倍，BS的為2.2倍）。本文提出的求解器比基于BS+SR的求解器在給定相同內(nèi)存閾值的情況下暫�；謴�(fù)需要更多時(shí)間，前者41.4，后者8.5。導(dǎo)致這一結(jié)果是因?yàn)榛?...

圖4 并行化求解速度提升情況

圖4表明本文提出的求解器能夠通過(guò)并行處理進(jìn)行加速。兩個(gè)工作程序能夠?qū)⑵骄俣忍岣叩?.62倍，4個(gè)工作程序能夠?qū)⑵骄俣忍岣叩?.4倍。下一步可以考慮解決以下實(shí)現(xiàn)限制提升并發(fā)性。所有的工作程序從一個(gè)共享的任務(wù)隊(duì)列中獲取任務(wù)；所有的工作程序添加他們產(chǎn)生的任務(wù)到一個(gè)共享隊(duì)列；如果當(dāng)任....

本文編號(hào)：4025433