Counting Satisfying Assignments in a Special SAT Formula

We are given a Boolean SAT problem in Conjunctive Normal Form (CNF) with a special structure. In this problem, we have variables (x_1,x_2,\dots,x_n) where each (x_i \in {\mathrm{True},\mathrm{False}}) (we consider 1 as True and 0 as False). The CNF formula is expressed as: [ (l_{1,1}\lor l_{1,2}\lor \cdots \lor l_{1,q_1}) \land (l_{2,1}\lor l_{2,2}\lor \cdots \lor l_{2,q_2}) \land \cdots \land (l_{m,1}\lor l_{m,2}\lor \cdots \lor l_{m,q_m}) ] Each clause ((l_{i,1}\lor l_{i,2}\lor \cdots \lor l_{i,q_i})) is a disjunction of literals. A literal is either a variable (x_j) or its negation (\lnot x_j). It is guaranteed that within a clause no variable appears more than once (i.e. there do not exist indices (j < k) such that the same variable appears in both (l_{i,j}) and (l_{i,k})).

A certain researcher claims that any SAT instance can be reduced to a special case in which every clause satisfies two extra properties:

• For any \(1 \le i \le n\), both \(x_i\) and \(\lnot x_i\) do not appear simultaneously in any clause.
• For any \(1 \le i < j < k \le n\), if a clause contains \(x_i\) (or \(\lnot x_i\)) and \(x_k\) (or \(\lnot x_k\)), then it must also contain \(x_j\) (or \(\lnot x_j\)).

Because of the second property, every clause that contains at least two literals involves a set of variables with consecutive indices; that is, if a clause contains variables with smallest index (l) and largest index (r), then it contains all variables (x_l,x_{l+1},\dots,x_r) (each possibly negated).

For a literal, note that a positive literal (x_i) is satisfied if (x_i) is True, while a negative literal (\lnot x_i) is satisfied if (x_i) is False. A clause is satisfied if at least one of its literals is satisfied. Equivalently, each clause has exactly one forbidden assignment for the variables that appear in it: for a positive literal (x_i) the literal fails when (x_i) is False, and for a negative literal (\lnot x_i) it fails when (x_i) is True.

Given a special SAT formula, count the number of distinct truth assignments (x_1,x_2,\dots,x_n) that satisfy the whole formula. Since the answer can be huge, output it modulo (10^9+7).

Input Format: The input begins with two integers (n) and (m) denoting the number of variables and the number of clauses respectively. Then follow (m) lines. Each clause is given in one line starting with an integer (q) (the number of literals in the clause) followed by (q) space‐separated integers. For a literal represented by a positive integer (i), it stands for (x_i); a negative integer (-i) stands for (\lnot x_i).

Output Format: Output a single integer, the number of satisfying assignments modulo (10^9+7).

inputFormat

The first line contains two integers \(n\) and \(m\) separated by a space, representing the number of variables and clauses respectively.

Each of the following \(m\) lines describes a clause. Each line begins with an integer \(q\) (the number of literals in that clause), followed by \(q\) space-separated integers. A positive integer \(i\) represents literal \(x_i\), while a negative integer \(-i\) represents literal \(\lnot x_i\).

Constraints: It is guaranteed that in each clause, no variable appears more than once, and if a clause contains literals corresponding to variables with minimum index \(l\) and maximum index \(r\), then it contains all variables \(x_l,x_{l+1},\dots,x_r\) (with their respective signs).

outputFormat

Output a single integer: the total number of satisfying assignments modulo \(10^9+7\).

sample

3 2
2 1 2
2 -2 3

4