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
89
90
91
92
93
94
//Lukasz Janeczko Krakow
#include <iostream>
#include <vector>
#include <string>
#include <algorithm>
using namespace std;
int main()
{
    ios_base::sync_with_stdio(false);
    int n, s; char cha; string c;
    cin >> n;
    cin >> cha;
    getline(cin,c);
    c=cha+c;
    s=c.size();
    vector < vector <int> > Clauses;
    for(int i=0; i<s; )
        {
            int j=i+1; int val=0; bool sig=true; vector <int> W(1,0);
            if(true)
                {
                    if(c[j]=='~')
                        {
                            sig=false;
                            j++;
                        }
                    j++;
                    while('0'<=c[j] && c[j]<='9')
                        {
                            W[0]=10*W[0]+c[j]-'0';
                            j++;
                        }
                    if(!sig)
                        W[0]*=(-1);
                }

            while(c[j]!=')')
                {
                    j+=3;
                    val=0;
                    sig=true;
                    if(c[j]=='~')
                        {
                            sig=false;
                            j++;
                        }
                    j++;
                    while('0'<=c[j] && c[j]<='9')
                        {
                            val=10*val+c[j]-'0';
                            j++;
                        }
                    if(!sig)
                        val*=(-1);
                    W.push_back(val);
                }
            Clauses.push_back(W);
            i=j+4;
        }
    if(n>0)
        {
            /*for(int i=0; i<Clauses.size(); i++)
                {
                    for(int j=0; j<Clauses[i].size(); j++)
                        cout << Clauses[i][j] << " ";
                    cout <<endl;
                }*/
            long long ans=0, q=1000000007;
            for(int t=0; t<(1<<n); t++)
                {
                    vector <int> V(n,0); int k=t, i=0; bool good=true;
                    while(k>0)
                        {
                            V[i]=k%2;
                            k/=2;
                            i++;
                        }
                    for(int i=0; i<Clauses.size() && good; i++)
                        {
                            good=false;
                            for(int j=0; j<Clauses[i].size() && !good; j++)
                                if(Clauses[i][j]<0 && V[(-1)*Clauses[i][j]-1]==0)
                                    good=true;
                                else
                                if(Clauses[i][j]>0 && V[Clauses[i][j]-1]==1)
                                    good=true;
                        }
                    if(good)
                        ans++;
                }
            cout << ans%q <<endl;
        }
    return 0;
}