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
#include <cstdio>
#include <vector>
#include <algorithm>
using namespace std;

char *input;
size_t input_size;

int main()
{
    int n;
    scanf("%d\n", &n);
    getline(&input, &input_size, stdin);
    vector<pair<int,int> > klauzula;
    vector<pair<int,int> > zmienne[n+1];
    int nr_klauzuli = 0, liczba, znak;
    for (int i = 0; input[i] != 0; ++i) {
        ++nr_klauzuli;
        while (input[i] == '(' || input[i] == ' ' || input[i] == 'x' || input[i] == '^')
            ++i;
        while (input[i] != ')') {
            liczba = 0;
            znak = 1;
            if (input[i] == '~') {
                znak = -1;
                ++i;
            }
            while (input[i] == ' ' || input[i] == 'x')
                ++i;
            while ('0' <= input[i] && input[i] <= '9') {
                liczba = 10 * liczba + input[i] - '0';
                ++i;
            }

            //klauzula.push_back(make_pair(liczba, znak));
            //printf("klauzula(%d, %d)\n", liczba, znak);
            zmienne[liczba].push_back(make_pair(znak, nr_klauzuli));

            while (input[i] == ' ' || input[i] == 'x' || input[i] == 'v')
                ++i;
        }
        ++i; // przejście za znak ')'
    }
    int liczba_klauzul = nr_klauzuli, wynik = 0;
    int wartosc_kl[liczba_klauzul + 1];
    int wartosc_zm[n + 1];
    for (int i = 0; i <= n; ++i)
        wartosc_zm[i] = 1;
    while (true) {
        // sprawdzenie
        for (int i = 0; i <= liczba_klauzul; ++i)
            wartosc_kl[i] = -1;
        for (int i = 0; i <= n; ++i)
            for (int j = 0; j < zmienne[i].size(); ++j) {
//                printf("przed: wartosc_kl[%d] = %d\n", zmienne[i][j].second, wartosc_kl[zmienne[i][j].second]);
                wartosc_kl[zmienne[i][j].second] = max(wartosc_kl[zmienne[i][j].second], wartosc_zm[i]*zmienne[i][j].first);
//                printf("po: wartosc_kl[%d] = %d\n", zmienne[i][j].second, wartosc_kl[zmienne[i][j].second]);
            }
        int klauzul_spelnionych = 0;
        for (int i = 1; i <= liczba_klauzul; ++i)
            if (wartosc_kl[i] == 1) {
                ++klauzul_spelnionych;
//                printf("klauzula %d spelniona\n", i);
            }
        if (klauzul_spelnionych == liczba_klauzul)
            wynik = (wynik + 1) % 1000000007;

        // nastepna wartosc
        int pos = 1;
        while (pos <= n && wartosc_zm[pos] == -1) {
            wartosc_zm[pos] = 1;
            ++pos;
        }
        if (pos <= n)
            wartosc_zm[pos] = -1;
        else
            break;
    }
    printf("%d\n", wynik);
    return 0;
}