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
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
#include <cstdio>
#include <vector>
#include <cstdlib>
#include <algorithm>

#define debug 0
#define MODULO 1000000007

using namespace std;

long long int powers_of_2[1000010];
long long int com_table[1000010][2];

vector<vector<vector<bool> > > klauzule(1000010, vector<vector<bool> >(0)); // dla klauzule[i] trzy,a wszystkie klauzule kończące się  literałem i
// od tyłu i, i-1, i-2, ... w formacie: czy_wlasciwa (true) czy zanegowana (false)

int n;

void compute_powers_2() {
    powers_of_2[0] = 1;
    for(int i = 1; i < 1000005; ++i) {
        powers_of_2[i] = (powers_of_2[i-1] * 2) % MODULO;
    }
}

int char_array_to_int(char array[]) {
    int i;
    sscanf(array, "%d", &i);
    return i;
}


void compute_combinations() {
   com_table[0][0] = 1;
   int zanegowane_i = 0;
   int niezanegowane_i = 0;
   int wykladnik = 0;
   bool przekroczony_zakres_klauzul = false;
   int iterator_klauzuli = 1;
   int pozytywne_literaly = 0;
   int negatywne_literaly = 0;

   for(int i = 1; i <=n+1; ++i) {
       zanegowane_i = 0;
       niezanegowane_i = 0;
      for(int j = 0; j<klauzule[i].size(); ++j) {
        if(klauzule[i][j][0]) {
            ++niezanegowane_i;
        } else {
            ++zanegowane_i;
        }
      }
      // jeśli brak klauzul wymagających zanegowanego i to niezanegowane spełnia jak dotąd wszystkie klauzule
      if (zanegowane_i == 0) {
        com_table[i][0] = (com_table[i-1][0] + com_table[i-1][1]) % MODULO;
      } else {
        // ech, trzeba przetwarzać
        wykladnik = 0;
        przekroczony_zakres_klauzul = false;
        iterator_klauzuli = 1;

        while(!przekroczony_zakres_klauzul) {
            // sprawdź, czy nadal możesz znaleźć przodka spełniającego wszystkie klauzule 
            pozytywne_literaly = 0;
            negatywne_literaly = 0;
            for(int j = 0; j < klauzule[i].size(); ++j) {
                if(klauzule[i][j][0] == true) continue; // pozytywne nas teraz nie obchodza, bo je spelniamy
                if(klauzule[i][j].size() <= iterator_klauzuli) {
                    przekroczony_zakres_klauzul = true;
                    break;
                } else if (klauzule[i][j][iterator_klauzuli]) {
                    ++pozytywne_literaly;
                } else {
                    ++negatywne_literaly;
                }
            }
            if (przekroczony_zakres_klauzul) break;
            // jest szansa na znalezienie:
            if (pozytywne_literaly > 0 && negatywne_literaly == 0) {
                if (debug) printf("Znaleziono literał co spełnia wszystkie klauzule: x%d\n", i-iterator_klauzuli);
                // BINGO!
                // biore maxa, chociaz nie zadziala, ale nie chce mi sie juz tego rozpisywac
                com_table[i][0] = max(com_table[i][0], com_table[i-iterator_klauzuli][0] * powers_of_2[wykladnik] %
                MODULO);
            } else if (pozytywne_literaly == 0 && negatywne_literaly > 0) {
                if (debug) printf("Znaleziono literał co spełnia wszystkie klauzule: x%d\n", i-iterator_klauzuli);
                // znowu BINGO!
                com_table[i][0] = max(com_table[i][0], com_table[i-iterator_klauzuli][1] * powers_of_2[wykladnik] %
                MODULO);
            }
            // zwieksz wykladnik gdyby sie pożniej trafił spełniacz:
            if (com_table[i-iterator_klauzuli][0] && com_table[i-iterator_klauzuli][1])
                wykladnik += 1;
            iterator_klauzuli += 1;
        }
      }
      // i odwrotnie
      if (niezanegowane_i == 0) {
        com_table[i][1] = (com_table[i-1][0] + com_table[i-1][1]) % MODULO;
      } else {
        // ech, trzeba przetwarzać
        wykladnik = 0;
        przekroczony_zakres_klauzul = false;
        iterator_klauzuli = 1;
        
        while(!przekroczony_zakres_klauzul) {
            // sprawdź, czy nadal możesz znaleźć przodka spełniającego wszystkie klauzule 
            pozytywne_literaly = 0;
            negatywne_literaly = 0;
            for(int j = 0; j < klauzule[i].size(); ++j) {
                if(klauzule[i][j][0] == false) continue; // negatywne nas teraz nie obchodza, bo je spelniamy
                if(klauzule[i][j].size() <= iterator_klauzuli) {
                    przekroczony_zakres_klauzul = true;
                    break;
                } else if (klauzule[i][j][iterator_klauzuli]) {
                    ++pozytywne_literaly;
                } else {
                    ++negatywne_literaly;
                }
            }
            if (przekroczony_zakres_klauzul) break;
            // jest szansa na znalezienie:
            if (pozytywne_literaly > 0 && negatywne_literaly == 0) {
                if (debug) printf("Znaleziono literał co spełnia wszystkie klauzule: x%d\n", i-iterator_klauzuli);
                // BINGO!
                com_table[i][1] = max(com_table[i][1], com_table[i-iterator_klauzuli][0] * powers_of_2[wykladnik] %
                MODULO);
            } else if (pozytywne_literaly == 0 && negatywne_literaly > 0) {
                if (debug) printf("Znaleziono literał co spełnia wszystkie klauzule: x%d\n", i-iterator_klauzuli);
                // znowu BINGO!
                com_table[i][1] = max(com_table[i][1], com_table[i-iterator_klauzuli][1] * powers_of_2[wykladnik] %
                MODULO);
            }
            // zwieksz wykladnik gdyby sie poźniej trafił spełniacz:
            if (com_table[i-iterator_klauzuli][0] && com_table[i-iterator_klauzuli][1])
                wykladnik += 1;
            iterator_klauzuli += 1;
        }
      }
   }
}


void parse_input() {
    scanf("%d\n", &n);


    char x;
    int node;

    bool is_in_clause = false;
    bool is_in_literal = false;
    int literal_number_i = 0;

    char number_array[10];

    vector<int> clause_literals; // nieuporządkowane literały w formacie +i lub -i

    while(x = getchar()) {
        if (debug > 1) printf("Pobrałem znak: %c\n", x);
        if (x == '\n' || x == '\0') {
            return;
        } else {
            if (x == '(') {
                is_in_clause = true;
                clause_literals.clear();
            } else if (x == ')') {
                is_in_clause = false;
                if (is_in_literal) {
                    number_array[literal_number_i++] = '\0';
                    int literal = char_array_to_int(number_array);
                    is_in_literal = false;
                    clause_literals.push_back(literal);
                }
                if (debug>1) printf("Wczytałem literał: %d\n", clause_literals[clause_literals.size()-1]);
                // move clause to vector klauzule
                int clause_min = abs(clause_literals[0]);
                int clause_max = abs(clause_literals[0]);
                // find clause range
                for(int i = 1; i < clause_literals.size(); i++) {
                    if (clause_min > abs(clause_literals[i])) {
                        clause_min = abs(clause_literals[i]);
                    }
                    if (clause_max < abs(clause_literals[i])) {
                        clause_max = abs(clause_literals[i]);
                    }
                }

                if (debug>1) printf("Wyznaczyłem mina: %d i maksa %d\n", clause_min, clause_max);
                vector<bool> klauzula(clause_max - clause_min + 1);
                for(int i = 0; i < clause_literals.size(); ++i) {
                    klauzula[(clause_max - clause_min) - (abs(clause_literals[i]) - clause_min)] = clause_literals[i] > 0;
                }
                if (debug>1) printf("Dodaje wyznaczony wektor na koniec\n");
                klauzule[clause_max].push_back(klauzula);
            } else if (x == ' ') {
                if (is_in_literal) {
                    number_array[literal_number_i++] = '\0';
                    int literal = char_array_to_int(number_array);
                    is_in_literal = false;
                    clause_literals.push_back(literal);
                }
            } else if (x == 'x') {
                if (!is_in_literal) {
                    is_in_literal = true;
                    literal_number_i = 0;
                }
            } else if (x == '^' || x == 'v') {
            } else if (x == '~') {
                is_in_literal = true;
                literal_number_i = 0;
                number_array[literal_number_i++] = '-';
            } else if (x >= '0' && x <= '9') {
                if (is_in_literal) {
                    number_array[literal_number_i++] = x;
                } else {
                    if (debug) printf("OMG! Wczytano liczbe a nie parsuje liczby!!!\n");
                }
            }
        }
    }
}


void print_test_input() {
    for(int i = 1; i <= n; ++i) {
        printf("Klauzule konczace sie w %d:\n", i);
        for(int j = 0; j < klauzule[i].size(); ++j) {
            printf("\tKlauzula %d: ", j);
            for (int k = 0; k < klauzule[i][j].size(); ++k) {
                printf(klauzule[i][j][k] ? "x%d " : "-x%d ", i - k);
            }
            printf("\n");
        }
    }
    return;
}

void print_combinations_table() {
    //print headers
    for (int i = 0; i <= n+1; i++) {
        printf("%d ", i);
    }
    printf("\n");

    for (int i = 0; i <= n+1; i++) {
        printf("%d ", com_table[i][0]);
    }
    printf("\n");

    for (int i = 0; i <= n+1; i++) {
        printf("%d ", com_table[i][1]);
    }
    printf("\n");
}

int main() {
    if (debug>1) printf("Bede czytal\n");
    parse_input();
    
    if (debug) printf("Wczytano input\n");
    if (debug) print_test_input();

    compute_powers_2();

    compute_combinations();
    if (debug) print_combinations_table();

    printf("%lld\n", com_table[n+1][0]);
    return EXIT_SUCCESS;
}