1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <vector>
#include <algorithm>
#include <cctype>
using namespace std;

char buffer[1000000 + 2];

int main() {
  int n;
  scanf("%d", &n);
  getchar();

  fgets(buffer, sizeof(buffer), stdin);
  char *ptr = strchr(buffer, '\n');
  if (ptr != NULL) {
    *ptr = '\0';
  }

  char c;
  int input_length = strlen(buffer);
  vector<vector<pair<int, int> > > clauses;
  for (int i = 0; i < input_length;) {
    // Should be '('.
    i++;

    // Read clause.
    vector<pair<int, int> > clause;
    while (1) {
      int idx, value = 1;

      c = buffer[i++];
      if (c == '~') {
        value = 0;
        i++;
      }

      idx = atoi(&buffer[i]);
      while (isdigit(buffer[i])) {
        i++;
      }

      clause.push_back(make_pair(idx, value));

      if (buffer[i] == ' ') {
        i += 3;
      } else {
        i += 4;
        break;
      }
    }

    /*printf("Clause:\n");
    for (auto it : clause) {
      printf("  (%d, %d)\n", it.first, it.second);
    }*/

    clauses.push_back(clause);
  }

  int result = 0;
  for (int i = 0; i < (1 << n); i++) {
    bool success = true;
    for (auto clause : clauses) {
      bool found = false;
      for (auto literal : clause) {
        if ((i & (1 << (literal.first - 1))) == (literal.second << (literal.first - 1))) {
          found = true;
          break;
        }
      }
      if (!found) {
        success = false;
        break;
      }
    }
    if (success) {
      result++;
    }
  }
  printf("%d\n", result);

  return 0;
}