離散數學 消解算法判斷合取范式的可滿足性

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加入S2
		for (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，清空S2
		for (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;
}