[發明專利]一種基于極小不協調集合的R縮減求解方法

無效

• 申請號: 200910243037.6
• 申請日: 2009-12-22
• 公開（公告）號: CN101719094A
• 公開（公告）日: 2010-06-02
• 發明（設計）人: 羅杰;李未;李賀;劉祥龍;蔣東辰
• 申請（專利權）人: 北京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京科迪生專利代理有限責任公司 11251
• 代理人: 李新華

1.一種基于極小不協調集合的R縮減求解方法，其特征在于步驟如下：

(1)獲取輸入的協調原子語句和原子語句的否定的集合，存于Δ中，獲取輸入的被修正語句集合，存于Γ中；

(2)將Γ中的所有公式轉換為否定范式(NNF)，然后再轉換為析取范式(DNF)，存入?！渲校?/p>

(3)求解出Δ∪Γ′的所有極小不協調集合，存于中；

(4)根據求解出Δ∪?！涞乃袠O小刪除集合，存于中；

(5)對于中的每一個極小刪除集合θ′，如果它對應的Γ中的語句集合是θ，并且那么Γ-θ就是Γ關于Δ的R縮減，并將其加入集合中。

2.根據權利要求1的基于極小不協調集合的R縮減求解方法，其特征在于：所述的步驟(3)進一步包括：

(3a)當Δ∪?！渲话诱Z句和原子語句的否定時：枚舉出Δ∪?！渌行稳鐊A，～A}的子集{A₁，～A₁}，...，{A_m，～A_m}，則

(3b)當Δ∪?！浒珹∧B時：記Ξ＝Δ∪?！?{A∧B}。遞歸的使用此方法求解Ξ∪{A，B}的所有極小不協調集合，存于中；遍歷中的所有元素，如果并且那么將Λ加入中；如果并且那么將(Λ-{A，B})∪{A∧B}加入中；

(3c)當Δ∪?！浒珹∨B時：記Ξ＝Δ∪?！?{A∨B}。遞歸的使用此方法求解Ξ∪{A}和Ξ∪{B}的所有極小不協調集合，分別存于和中；如果那么將Λ加入集合遍歷和中的所有元素，如果A∈Λ₁并且B∈Λ₂，那么(Λ₁-{A})∪(Λ₂-{B})∪{A∨B}加入集合遍歷中的所有元素，如果并且不存在使得那么將Λ加入中。

3.根據權利要求1的基于極小不協調集合的R縮減求解方法，其特征在于：所述的步驟(4)進一步包括：

(4a)若集合不是空集，則：

(i)選取集合中的第一個極小不協調子集Λ；

(ii)對于Λ中的任何一個語句A，

對遞歸的使用這一方法求出它的所有極小刪除集合

(iii)對任意的遍歷集合如果存在Φ′使得Φ′⊃{A}∪Φ,]]>那么就將Φ′從中刪除

如果不存在一個使得Φ′⋐{A}∪Φ,]]>那么

(4b)若集合是空集，則