POJ 3295 - Tautology

http://poj.org/problem?id=3295

概要

変数 p, q, r, s, t を含む論理式が与えられ，それがトートロジーかどうか答える．

制約

解法

変数が最大でも5種類しかないので，全通り試してすべて真になったらトートロジーと判定する． パースも簡単．

 1 #include <iostream>
 2 #include <vector>
 3 #include <cctype>
 4 #include <cassert>
 5 using namespace std;
 6 
 7 struct formula
 8 {
 9   char var;
10   char op;
11   const formula *lhs, *rhs;
12   formula(char v) : var(v), op(0), lhs(0), rhs(0) {}
13   formula(char o, const formula *l, const formula *r = 0)
14     : var(0), op(o), lhs(l), rhs(r) {}
15   ~formula() { delete lhs;  delete rhs; }
16   bool eval(bool bs[5]) const
17   {
18     if (var) {
19       return bs[var-'p'];
20     } else {
21       switch (op) {
22         case 'K': return lhs->eval(bs) && rhs->eval(bs);
23         case 'A': return lhs->eval(bs) || rhs->eval(bs);
24         case 'N': return !lhs->eval(bs);
25         case 'C': return !lhs->eval(bs) || rhs->eval(bs);
26         case 'E': return lhs->eval(bs) == rhs->eval(bs);
27         default: throw "unknown operator";
28       }
29     }
30   }
31 };
32 
33 typedef string::const_iterator Iterator;
34 const formula *parse(Iterator& it, const Iterator& last)
35 {
36   assert(it != last);
37   if (islower(*it)) {
38     const char v = *it;
39     ++it;
40     return new formula(v);
41   } else if (*it == 'N') {
42     ++it;
43     return new formula('N', parse(it, last));
44   } else {
45     const char op = *it;
46     ++it;
47     const formula *l = parse(it, last);
48     const formula *r = parse(it, last);
49     return new formula(op, l, r);
50   }
51 }
52 
53 bool tautology(const formula *f)
54 {
55   for (int s = 0; s < (1<<5); s++) {
56     bool bs[5];
57     for (int i = 0; i < 5; i++) {
58       bs[i] = (s & (1<<i)) != 0;
59     }
60     if (!f->eval(bs)) {
61       return false;
62     }
63   }
64   return true;
65 }
66 
67 int main()
68 {
69   string s;
70   while (cin >> s && s != "0") {
71     Iterator it = s.begin();
72     const Iterator last = s.end();
73     const formula *f = parse(it, last);
74     cout << (tautology(f) ? "tautology" : "not") << endl;
75     delete f;
76   }
77 }
poj/3295.cc