题目信息
输入
合式公式 A 的合取范式
输出
当 A 是可满足时,回答YES
;否则回答NO
。
输入公式的符号说明:
!
非,相当于书面符号中的 ¬
&
与,相当于书面符号中的 ∧
|
或,相当于书面符号中的 ∨
-
蕴含联结词,相当于书面符号中的 →
+
等价联结词,相当于书面符号中的 ↔
(
前括号
)
后括号
解答
#include <iostream>
#include <cstring>
using namespace std;
int s[500][30] = {
0};
//每行存储一个简单析取式,第二维下标0~25代表命题变项a~z
//取值 0: 该变项没有出现,1: 该变项出现,2: 该变项出现且为否定
int sum0 = -1, sum1 = -1, sum2 = 0; //实现对S1,S2,S3三个集合的指向
void store(char *str)
{
//将输入字符串存到s数组
int len = strlen(str);
for (int i = 0; i < len; i++)
{
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;
}
}
}
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中是否有重复,有重复返回false
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++)
{
//遍历26个字母
if (!a[i] && !b[i])
{
//如果是两个0表示都不存在这些字母,不考虑了
continue;
}
else 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))
{
//全为0或者是一正一负可消解掉
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加入S2
for (int i = 0; i < 26; i++)
{
s[sum2][i] = c[i];
}
}
return true;
}
int main()
{
//freopen("/Users/zhj/Downloads/test.txt", "r", stdin);
char str[1000];
cin >> str;
store(str);
do
{
sum0 = sum1;
sum1 = sum2; //将S1并到S0中,令S1等于S2
for (int i = 0; i <= sum0; i++)
{
for (int j = sum0 + 1; j <= sum1; j++)
{
if (!res(s[i], s[j]))
{
cout << "NO" << endl;
return 0;
}
}
}
for (int i = sum0 + 1; i < sum1; i++)
{
for (int j = i + 1; j <= sum1; j++)
{
if (!res(s[i], s[j]))
{
cout << "NO" << endl;
return 0;
}
}
}
} while (sum2 > sum1); //若S2为空,结束
cout << "YES" << endl;
return 0;
}