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
87
88
#include <cstdlib>
#include <cstring>
#include <cmath>
#include <iostream>
#include <algorithm>
#include <string>
#include <vector>
#include <sstream>
#include <iterator>

using namespace std;
typedef long long int lint;
#define span(x) x.begin(), x.end()

const lint mod = 1000000007;
int n;

int main()
{
	ios_base::sync_with_stdio(false);
	cin >> n;
	cin.ignore();
	
	string in;
	getline(cin, in);
	for(auto& c : in)
		if(c == 'x') c = '0';
		else if(c == '~') c = '-';
		else if(c == '(' || c == ')' || c == 'v') c = ' ';
	
	istringstream iss(in);
	vector<string> tokens;
	string token;
	while(getline(iss, token, '^'))
		tokens.emplace_back(move(token));
	
	vector<vector<int>> expressions;
	for(const auto &t : tokens)
	{
		vector<int> expr;
		istringstream tiss(t);
		copy(istream_iterator<int>(tiss), istream_iterator<int>(), back_inserter(expr));
		sort(span(expr), [](int x, int y) { return abs(x) < abs(y); });
        expressions.emplace_back(move(expr));
	}
	
	if(expressions.size() == 1)
	{
		lint result = expressions[0].size();
		for(int i = 1; i < n; ++i)
			result = (2*result)%mod;
		printf("%lld", result);
		return 0;
	}
	
	int result = 0;
	for(int c = 0, cEnd = 1<<(n); c < cEnd; ++c)
	{
		bool areExprsSat = true;
		for(const auto &expr : expressions)
		{
			bool isExprSat = false;
			for(int i = 1; i <= n; ++i)
			{
				int v = c & (1<<(i-1));
				auto it = lower_bound(span(expr), i, [](int x, int y) { return abs(x) < abs(y); });
				if(it != expr.end() && abs(*it) == i && *it == (v == 0 ? -i : i))
				{
					isExprSat = true;
					break;
				}
			}
			if(!isExprSat)
			{
				areExprsSat = false;
				break;
			}
		}
		if(areExprsSat)
		{
			++result;
		}
	}
	
	printf("%d", result);
	
    return 0;
}