Description

消解算法

Input

合式公式 A 的合取范式

Output

當 A 是可滿足時，回答“YES ”；否則回答“NO”。

輸入公式的符號說明：
! 非，相當于書面符號中的 “ ? ”
& 與，相當于書面符號中的 “ ∧ ”
| 或，相當于書面符號中的 “ ∨ ”
( 前括號
) 后括號

Code

#include <cstdio> #include <cstring> #define N 1010 int s[N][30]; //每行存儲一個簡單析取式，第二維下標0~25代表命題變項a~z //取值 0: 該變項沒有出現，1: 該變項出現，2: 該變項出現且為否定 int sum0, sum1, sum2; //實現對S1，S2，S3三個集合的指向 void store(char str[]) //將輸入字符串存到s數組，標記到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[]) //判斷兩簡單析取式是否相同 {for (int i = 0; i < 26; i++)if (a[i] != b[i]) return false;return true; } bool check(int c[]) //檢查S1，S2，S3中是否有重復 {for (int i = 0; i <= sum2; i++)if (same(s[i], c)) return false;return true; } bool res(int a[], int b[]) //消解函數，若得到空子句，返回false，否則返回true {int single = 0; //不能消解的變項個數int couple = 0; //可消解的變項個數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; //不能消解或有多對可以消解if (!single) return false; //只有一對可消解且沒有不能消解的變項，得到空子句int c[30]; //消解結果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中是否出現過{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為空，結束printf("YES\n");return 0; }

轉載于:https://www.cnblogs.com/dadamrx/p/7294648.html

總結

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

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。