题目描述

题目译自 PA 2016 Runda 5 CNF-SAT

又一届「$P=NP$ 平等游行」即将来临。今年，$P=NP$ 运动的非正式领袖 Bajtazar 决定在游行中彻底让众多反对者闭嘴，宣布证明这一著名等式的证据。

Bajtazar 的证明基于展示一个多项式时间算法来解决众所周知的 NP 困难问题 CNF-SAT。在这个问题中，给定 $n$ 个逻辑变量 $x_{1}, \ldots, x_{n}$ 以及一个以所谓合取范式（CNF）表示的逻辑公式。这样的公式形式为：

$$(l_{1,1} \vee \ldots \vee l_{1, q_{1}}) \wedge (l_{2,1} \vee \ldots \vee l_{2, q_{2}}) \wedge \ldots \wedge (l_{m,1} \vee \ldots \vee l_{m, q_{m}}), $$

其中每个表达式 $(l_{i,1} \vee \ldots \vee l_{i, q_{i}})$ 称为一个子句，每个 $l_{i,j}$ 是一个文字，即某个变量或某个变量的否定，来自给定的 $x_{1}, \ldots, x_{n}$。我们假设任何有效的子句中不包含两个相同的文字。例如，对于 $n=m=3$，一个合取范式的公式示例为 $(x_{1} \vee \neg x_{3}) \wedge (x_{2}) \wedge (\neg x_{3} \vee \neg x_{1} \vee x_{2})$。

CNF-SAT 问题在于判定是否存在一个变量 $x_{1}, \ldots, x_{n}$ 的赋值，使得给定的公式为真（即其逻辑值为真）。

遗憾的是，Bajtazar 的证明还差一步。他声称已经将一般的 CNF-SAT 问题归约到了一个特殊情况，其中给定公式的每个子句 $C$ 都是连贯的，即满足以下性质：

• 对于任意 $i$，$x_{i}$ 和 $\neg x_{i}$ 不能同时作为子句 $C$ 的文字出现。
• 如果存在 $i, j, k$ 使得 $i < j < k$，且变量 $x_{i}$（或其否定）以及 $x_{k}$（或 $\neg x_{k}$）出现在子句 $C$ 中，则 $x_{j}$ 或 $\neg x_{j}$ 也必须出现在子句 $C$ 中。
  例如，对于 $n=3$，子句 $(x_{2})$ 和 $(\neg x_{3} \vee \neg x_{1} \vee x_{2})$ 是连贯的，而子句 $(x_{2} \vee \neg x_{2})$ 和 $(x_{1} \vee \neg x_{3})$ 则不是。

请帮助 Bajtazar 找到一个有效的算法，解决上述 CNF-SAT 问题的特殊情况。为了进一步让他惊讶，编写一个程序，计算满足由连贯子句组成的给定 CNF-SAT 公式的变量 $x_{1}, \ldots, x_{n}$ 赋值的数量。

输入格式

输入数据的第一行包含一个整数 $n$ $(1 \leq n \leq 1000000)$，表示变量数量。

第二行包含一个在变量 $x_{1}, \ldots, x_{n}$ 上的 CNF-SAT 公式，由纯连贯子句组成。公式的格式如下（另见下方示例）。

• 每个子句以左括号 ( 开始，以右括号 ) 结束。
• 文字 $x_{i}$（对于 $1 \leq i \leq n$）表示为 x i，文字 $\neg x_{i}$ 表示为 ~x i，例如 x 2 或 ~x 15。
• 同一子句内的相邻文字由符号 v（表示逻辑或）分隔，符号两侧各有一个空格。
• 相邻子句由符号 ^（表示逻辑与）分隔，符号两侧各有一个空格。

公式中所有子句的文字总数不超过 $1000000$。

输出格式

输出一个整数，表示满足输入公式的变量 $x_{1}, \ldots, x_{n}$ 赋值的数量，对 $10^{9}+7$ 取模。

3
(x2) ^ (x3 v ~x2) ^ (x2 v x1 v ~x3)

2

给定的公式仅在两种赋值下为真：$(0,1,1)$ 和 $(1,1,1)$。