摘要：用正則樹表示的XML數據中對XPath的決策問題,是大數據查詢中常見的方法之一,本文提出了一套實用的、有效的數學模型來解決XPath表達式中的可滿足性問題。并通過對一些決策問題,例如帶或者不帶類型約束的XPath的空、包含、重疊和覆蓋問題的實驗對于算法進行了證實,實驗證明該系統能夠有效的被使用于對操作XPath表達式和XML類型注釋的程序語言的靜態分析器中。