26622번 - CNF-SAT 다국어

Zbliża się kolejna Parada Równości P = NP. W tym roku nieformalny lider ruchu P = NP, Bajtazar, postanowił ostatecznie uciszyć swoich licznych przeciwników, ogłaszając na Paradzie dowód słynnej równości.

Dowód Bajtazara polega na pokazaniu algorytmu rozwiązującego znany NP-trudny problem CNF-SAT w czasie wielomianowym. W tym problemie dane jest n zmiennych logicznych x₁, . . . , x_n i formuła logiczna w tak zwanej koniunkcyjnej postaci normalnej. Taka formuła jest postaci

(l_1,1 ∨ . . . ∨ l_1,q1) ∧ (l_2,1 ∨ . . . ∨ l_2,q2) ∧ . . . ∧ (l_m,1 ∨ . . . ∨ l_m,qm),

dzie każde z wyrażeń (l_i,1 ∨ . . . ∨ l_1,qi) nazywamy klauzulą, a każde spośród wyrażeń l_i,j jest literałem, czyli pewną zmienną lub zaprzeczeniem pewnej zmiennej spośród danych x₁, . . . , x_n. Przyjmujemy, że żadna poprawna klauzula nie zawiera dwóch identycznych literałów. Dla n = m = 3, przykładową formułą w koniunkcyjnej postaci normalnej może być (x₁ ∨ ¬x₃) ∧ (x₂) ∧ (¬x₃ ∨ ¬x₁ ∨ x₂).

Problem CNF-SAT polega na rozstrzygnięciu, czy istnieje pewne wartościowanie zmiennych x₁, . . . , x_n, dla którego dana formuła jest spełniona (to znaczy, jej wartością logiczną jest prawda).

Niestety, do dokończenia dowodu Bajtazarowi brakuje jednego kroku. Twierdzi on, że udało mu się sprowadzić^∗ ogólny problem CNF-SAT do jego szczególnego przypadku, gdzie każda klauzula C danej formuły jest spójna, czyli ma następujące własności:

• Dla dowolnego i, x_i i ¬x_i nie mogą być jednocześnie literałami C.
• Jeśli i, j, k są takie, że i < j < k i zarówno zmienna xi (lub jej zaprzeczenie) jak i x_k (lub ¬x_k) występują w klauzuli C, to x_j albo ¬x_j także występuje w C.

Przykładowo, dla n = 3 klauzule (x₂) i (¬x₃ ∨ ¬x₁ ∨ x₂) są spójne, a klauzule (x₂ ∨ ¬x₂) i (x₁ ∨ ¬x₃) – nie.

Pomóż Bajtazarowi znaleźć efektywny algorytm rozwiązujący powyższy szczególny przypadek problemu CNF-SAT. Aby jeszcze bardziej go zadziwić, napisz program znajdujący liczbę wartościowań zmiennych x₁, . . . , x_n spełniających daną formułę CNF-SAT, składającą się z samych spójnych klauzul.

W pierwszym wierszu wejścia znajduje się liczba całkowita n (1 ≤ n ≤ 1 000 000) oznaczająca liczbę zmiennych. W drugim wierszu wejścia mamy daną formułę CNF-SAT na zmiennych x₁, . . . , x_n, składającą się z samych spójnych klauzul. Formuła dana jest w następującym formacie (patrz także przykład poniżej).

• Każda klauzula zaczyna się nawiasem otwierającym (, a kończy nawiasem zamykającym ).
• Literał x_i (dla 1 ≤ i ≤ n) reprezentowany jest jako xi, a literał ¬x_i jako xi, np. x2 lub x15.
• Sąsiednie literały w obrębie jednej klauzuli oddzielone są znakiem v (oznaczającym logiczne lub) otoczonym z obu stron pojedynczymi spacjami.
• Sąsiednie klauzule oddzielone są znakiem ^ (oznaczającym logiczne i) otoczonym z obu stron pojedynczymi spacjami.

Sumaryczna liczba literałów we wszystkich klauzulach danej formuły nie przekroczy 1 000 000.

^∗Bajtazar zapomniał wspomnieć, czy jego redukcja działała w czasie wielomianowym...

Na wyjście należy wypisać liczbę wartościowań zmiennych x₁, . . . , x_n spełniających daną na wejściu formułę, modulo 10⁹ + 7.

Wyjaśnienie do przykładu: Dana formuła jest spełniona tylko dla dwóch wartościowań: (0, 1, 1) i (1, 1, 1).