[UVA] 11357 - Ensuring Truth
|
In this problem we will consider Boolean formulas written according to the following BNF grammar:
<formula> ::= <clause> | <formula> "|" <clause><clause> ::= "(" <conjunction-of-literals> ")"<conjunction-of-literals> ::= <literal> | <conjunction-of-literals> "&" <literal><literal> ::= <variable> | "~" <variable><variable> ::= "a" | "b" | "c" | ... | "z"
Each formula can contain up to 26 different Boolean variables, which are denoted by lowercase English letters. We use the ampersand sign ("&") to denote conjunction, vertical bar ("|") for disjunction, and tilde ("~") for inversion. The truth tables of these operators are shown below for your reference.
|
|
|
A formula is called satisfiable if it is possible to assign values to its variables in such a way as to make the formula evaluate to true.
Input
The first line of the input file contains an integer T (1 ≤ T ≤ 5000). Each of the next T lines contains a Boolean formula. You can assume that the formulas will strictly follow the grammar specified above, and will not be longer than 250 characters.
Output
For each formula, you should determine whether it is satisfiable, and output a line "YES" if yes, it is, and "NO" otherwise.
|
Sample Input |
Output for Sample Input |
2(a&b&c)|(a&b)|(a)(x&~x) |
YESNO
|
ProblemSetter: Ivan Krasilnikov
乍看之下以為是 NPC 問題。其實不是的。
由於 BNF 語法出來只會有 (&&&&) | (&&&&&) | ...
並不會存在 not exist (&&&&(&&&|&&&))。
因此只要考慮其中一個存在 (&&&&&) = true 就大功告成了。
char s[1005];
int main() {
int testcase;
scanf("%d", &testcase);
while(testcase--) {
scanf("%s", s);
int i, j, yes = 0;
for(i = 0; s[i]; i++) {
if(s[i] == '(') {
int cnt[26] = {};
while(s[i] != ')') {
if(s[i] >= 'a' && s[i] <= 'z') {
if(i >= 0 && s[i-1] == '~')
cnt[s[i]-'a'] |= 2;
else
cnt[s[i]-'a'] |= 1;
}
i++;
}
for(j = 0; j < 26; j++)
if(cnt[j] == 3)
break;
if(j == 26)
yes = 1;
}
}
puts(yes ? "YES" : "NO");
}
return 0;
}