本文選題：知識編譯 + 擴展規(guī)則�。� 參考：《軟件學(xué)報》2017年08期

【摘要】：超擴展規(guī)則是對擴展規(guī)則的擴充,基于超擴展規(guī)則能夠求得任意兩個非互補且不相互蘊含的子句所能擴展出極大項集的交集、差集和并集,并將所得結(jié)果以EPCCL(each pair of clauses contains complementary literals)理論的形式保存.基于超擴展規(guī)則的性質(zhì),提出一種EPCCL理論編譯算法:求交知識編譯算法IKCHER(intersection approach to knowledge compilation based on hyper extension rule).該算法適合難解類SAT問題的知識編譯,也是一種可并行的知識編譯算法.研究了如何實現(xiàn)多個EPCCL理論的求交操作,證明了EPCCL理論的求交過程是可并行執(zhí)行的,并設(shè)計了相應(yīng)的并行求交算法PIAE(parellel intersection of any number of EPCCL).通過對輸入EPCCL理論對應(yīng)普通子句集的利用,設(shè)計了一種高效的并行求交算法imp-PIAE(improvement of PIAE).基于上述算法,還設(shè)計了兩種并行知識編譯算法P-IKCHER(IKCHER with PIAE)和imp P-IKCHER(IKCHER with imp-PIAE),分別采用PIAE并行合并算法和imp-PUAE并行合并算法.最后,通過實驗驗證了,大部分情況下,IKCHER算法的編譯質(zhì)量是目前為止所有EPCCL理論編譯器中最優(yōu)的,P-IKCHER算法所使用的合并策略并沒有起到加速的效果,反而使得編譯效率和編譯質(zhì)量有所下降;imp P-IKCHER算法提高了IKCHER算法的編譯效率,CPU四核環(huán)境下最高可提高2倍.
[Abstract]:The hyper - extension rule is an extension of extended rule . Based on the hyper - extension rule , we can obtain the intersection , difference set and union of any two non - complementary and mutually exclusive clauses . Based on the properties of hyper - extension rules , an algorithm for compiling an EPC CL is proposed : IKCHER is applied to knowledge compilation based on hyper - extension rule . This algorithm is suitable for knowledge compilation of difficult - class SAT problems , and it is also a parallel knowledge compilation algorithm . It studies how to realize the intersection operation of multiple EPC CL theories . It is proved that the intersection process of EPC CL theory can be executed in parallel , and the corresponding PIAE ( parellel ) of any number of EPC CL is designed . In this paper , we design an efficient parallel intersection algorithm ( PIAE ) , which corresponds to the use of common clause set in the input EPC CL theory . 鍩轟簬涓婅堪綆楁硶,榪樿璁′簡涓ょ騫惰鐭ヨ瘑緙栬瘧綆楁硶P-IKCHER(IKCHER with PIAE)鍜宨mp P-IKCHER(IKCHER with imp-PIAE),鍒嗗埆閲囩敤PIAE騫惰鍚堝茍綆楁硶鍜宨mp-PUAE騫惰鍚堝茍綆楁硶.鏈，

本文編號：1986839