AOJ 1078 - SAT-EN-3

http://judge.u-aizu.ac.jp/onlinejudge/description.jsp?id=1078

解法

加法標準形で与えられているため，どれか1つの節が充足可能であればよい．

1つの節に含まれるのは3つのリテラルかリテラルの否定なので，やるだけ．

 1 #include <iostream>
 2 #include <vector>
 3 #include <algorithm>
 4 using namespace std;
 5 
 6 vector<string> split(const string& s, char d)
 7 {
 8   vector<string> r;
 9   for (string::const_iterator it = s.begin();;) {
10     string::const_iterator jt = find(it, s.end(), d);
11     if (jt == s.end()) {
12       r.push_back(string(it, s.end()));
13       return r;
14     } else {
15       r.push_back(string(it, jt));
16       it = jt+1;
17     }
18   }
19 }
20 int main()
21 {
22   string line;
23   while (cin >> line && line != "#") {
24     vector<string> clauses = split(line, '|');
25     for (vector<string>::const_iterator it = clauses.begin(); it != clauses.end(); ++it) {
26       vector<string> lits = split(it->substr(1, it->size()-2), '&');
27       vector<int> v(100, 0);
28       for (vector<string>::const_iterator jt = lits.begin(); jt != lits.end(); ++jt) {
29         if ((*jt)[0] == '~') {
30           v[(*jt)[1]-'A'] |= 1<<1;
31         } else {
32           v[(*jt)[0]-'A'] |= 1<<0;
33         }
34       }
35       if (find(v.begin(), v.end(), 3) == v.end()) {
36         cout << "yes" << endl;
37         goto NEXT;
38       }
39     }
40     cout << "no" << endl;
41 NEXT:
42     ;
43   }
44   return 0;
45 }