基于知識編譯的QBF求解器的研究.pdf

1、智能規(guī)劃是人工智能研究領(lǐng)域的一個重要分支,已在許多領(lǐng)域得以廣泛應(yīng)用。求解智能規(guī)劃問題的一個重要方法即把智能規(guī)劃問題轉(zhuǎn)化為命題邏輯公式求解。動作和世界狀態(tài)確定的規(guī)劃問題可以轉(zhuǎn)化成經(jīng)典命題邏輯問題(SAT)求解；動作確定,初始狀態(tài)不確定的一致性規(guī)劃可以在有效時間內(nèi)轉(zhuǎn)化成量化布爾公式(Quantified Boolean Formulae,簡稱QBF)問題求解。QBF是SAT的泛化,它可以對狀態(tài)空間較大的一致性規(guī)劃問題求解。QBF問題作為標(biāo)準(zhǔn)

2、的PSPACE完備問題在人工智能領(lǐng)域的重要性日益增長。非單調(diào)性推理,并行一致性推理等許多人工智能領(lǐng)域問題也可以在多項式時間內(nèi)轉(zhuǎn)換成QBF問題,并且實驗數(shù)據(jù)表明基于轉(zhuǎn)換的方法比基于域依賴的方法有效。
　　 知識編譯是近年來出現(xiàn)的一個新的研究方向,它用于處理一般命題邏輯推理的計算復(fù)雜性。根據(jù)這種方法,推理過程被分為兩個階段:離線編譯階段和在線查詢階段。離線階段,命題理論被編譯成某種易處理的目標(biāo)語言；在線階段編譯目標(biāo)被用于有效應(yīng)答指數(shù)

3、級數(shù)量的查詢。知識編譯的主要動機(jī)是將主要花銷放在離線階段,用無數(shù)次的有效在線查詢抵消,并生成一個快捷的在線推理系統(tǒng)。知識編譯是應(yīng)用于命題邏輯SAT上的,并在SAT上取得了很好的效果,QBF是SAT的泛化,知識編譯同樣可以應(yīng)用于QBF。
　　 本文討論了EPCCL、D-FNNF、FNNF、D-OFNNF、OFNNF這五種命題語言的基本性質(zhì),完備性,易處理性,以及它們的簡潔性。根據(jù)OFNNF的性質(zhì),我們提出一種新的模型計數(shù)方法-表推