Description

消解算法

Input

合式公式 A 的合取范式

Output

當(dāng) A 是可滿足時(shí)，回答“YES ”；否則回答“NO”。

輸入公式的符號(hào)說(shuō)明：
! 非，相當(dāng)于書(shū)面符號(hào)中的 “ ? ”
& 與，相當(dāng)于書(shū)面符號(hào)中的 “ ∧ ”
| 或，相當(dāng)于書(shū)面符號(hào)中的 “ ∨ ”
( 前括號(hào)
) 后括號(hào)

Code

#include <cstdio> #include <cstring> #define N 1010 int s[N][30]; //每行存儲(chǔ)一個(gè)簡(jiǎn)單析取式，第二維下標(biāo)0~25代表命題變項(xiàng)a~z //取值 0: 該變項(xiàng)沒(méi)有出現(xiàn)，1: 該變項(xiàng)出現(xiàn)，2: 該變項(xiàng)出現(xiàn)且為否定 int sum0, sum1, sum2; //實(shí)現(xiàn)對(duì)S1，S2，S3三個(gè)集合的指向 void store(char str[]) //將輸入字符串存到s數(shù)組，標(biāo)記到S2 {memset(s, 0, sizeof(s));sum0 = sum1 = -1; sum2 = 0;int len = strlen(str);int i = 0; while (i <= len){if (str[i] >= 'a' && str[i] <= 'z') s[sum2][str[i] - 'a'] = 1;else if (str[i] == '&') sum2++;else if (str[i] == '!') s[sum2][str[++i] - 'a'] = 2;i++;} } bool same(int a[], int b[]) //判斷兩簡(jiǎn)單析取式是否相同 {for (int i = 0; i < 26; i++)if (a[i] != b[i]) return false;return true; } bool check(int c[]) //檢查S1，S2，S3中是否有重復(fù) {for (int i = 0; i <= sum2; i++)if (same(s[i], c)) return false;return true; } bool res(int a[], int b[]) //消解函數(shù)，若得到空子句，返回false，否則返回true {int single = 0; //不能消解的變項(xiàng)個(gè)數(shù)int couple = 0; //可消解的變項(xiàng)個(gè)數(shù)for (int i = 0; i < 26; i++){if (!a[i] && !b[i]) continue;if ((a[i] == 1 && b[i] == 2) || (a[i] == 2 && b[i] == 1)) couple++;else single++;}if (couple != 1) return true; //不能消解或有多對(duì)可以消解if (!single) return false; //只有一對(duì)可消解且沒(méi)有不能消解的變項(xiàng)，得到空子句int c[30]; //消解結(jié)果for (int i = 0; i < 26; i++){if ((!a[i] && !b[i]) || (a[i] + b[i] == 3)) c[i] = 0;else if (a[i] == 1 || b[i] == 1) c[i] = 1;else c[i] = 2;}if (check(c)) //檢查c在S0，S1，S2中是否出現(xiàn)過(guò){sum2++; //將c加入S2for (int i = 0; i < 26; i++) s[sum2][i] = c[i];}return true; } int main() {char str[N];scanf("%s", str);store(str);do{sum0 = sum1; sum1 = sum2; //將S1并到S0中，令S1等于S2，清空S2for (int i = 0; i <= sum0; i++)for (int j = sum0 + 1; j <= sum1; j++)if (!res(s[i], s[j])){printf("NO\n");return 0;}for (int i = sum0 + 1; i <= sum1; i++)for (int j = i + 1; j <= sum1; j++)if (!res(s[i], s[j])){printf("NO\n");return 0;}} while (sum2 > sum1); //若S2為空，結(jié)束printf("YES\n");return 0; }

轉(zhuǎn)載于:https://www.cnblogs.com/dadamrx/p/7294648.html

總結(jié)

以上是生活随笔為你收集整理的离散数学 消解算法判断合取范式的可满足性的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。