Question about a proof of the existence of unsatisfiable linear k-CNFs for any k

Question

Today I am reading paper Unsatisfiable Linear k-CNFs Exist, for every k by Dominik Scheder, 2007. But I have some problem to understand the proof of Theorem $3.2$.

I don't know how to understand the underlined part:

1. How do we create variable-disjoint copies of $F$?
2. Why is the number $2^m$?

Theorem 3.2. For any $k\in\Bbb N_0$, there are unsatisfiable linear $k$-CNFs.

Proof. We prove this by induction on $k$. For $k=0$, the formula $F=\{\{\}\}$ containing only the empty clause is linear and unsatisfiable. For the induction step, let $F=\{C_1,\cdots, C_2\}$ be an unsatisfiable linear $k$-CNF. We will construct an unsatisfiable linear $(k+1)$-CNF formula $F'$. Created $m$ new variables $x_x, \cdots, x_m$. For a clause $D=\{u1, \cdots, u_m\}$ with $u_i\in\{x_i, \bar x_i\}$, define $$F\otimes D := \{C_i\cup\{u_i\}\mid i=1,\cdots, m\}\ .$$ $F'$ is a linear $(k+1)$-CNF formula, and every assignment satisfying $F\otimes D$ satisfies $D$. Create $2^m$ variable-disjoint copies $F_1, \cdots, F_{2^m}$ of $F$, i.e., $\text{vbl}(F_i)\cap\text{vbl}(F_j)=\emptyset$ for $i\not=j$. By choosing $2^m$ different sign patterns, we create $2^m$ distinct $m$-clauses $D_1, \cdots, D_{2^m}$ over the variables $x_i$. The formula $\{D_1, \cdots, D_{2^m}\}$ is unsatisfiable. Hence, $$ F' := \bigcup_{i=1}^{2^m}F_i\otimes D_i$$ is unsatisfiable, as well. Clearly, $F'$ is a linear $(k+1)$-CNF. $\Box$

Here is the image of the quotation above in the original paper.

Answer 1

Suppose $\text{vbl}(F)=\{y_1,\cdots, y_v\}$, i.e., $F$ is a CNF over variables in $\text{vbl}(F)$.

Let $\{y_{i,j}\mid 1\le i\le 2^m, 1\le j\le v\}$ be a set of distinct $2^mv$ variables.
For each $i=1,\cdots, 2^m$, let $F_i$ be $F$ with every appearance of $y_j$ replaced with $y_{i,j}$ and every appearance of $\bar y_j$ replaced by $\bar y_{i,j}$. Then $F_i$ is a copy of $F$ over variables in $\text{vbl}(F_i)=\{y_{i,j}\mid 1\le j\le v\}$.

---

The number of all $m$-clauses $c$ such that $\text{vbl}(c)=\{x_1,\cdots, x_m\}$ is $2^m$. They are, for example if $m=3$, $\{x_1,x_2,x_3\}$,$\{x_1,x_2,\bar x_3\}$, $\{x_1,\bar x_2,x_3\}$, $\{x_1,\bar x_2,\bar x_3\}$, $\{\bar x_1,x_2,x_3\}$, $\{\bar x_1,x_2,\bar x_3\}$, $\{\bar x_1,\bar x_2,x_3\}$, $\{\bar x_1,\bar x_2,\bar x_3\}$. List these $2^m$ clauses as $D_1, \cdots, D_{2^m}$.

What is important is that the formula $\{D_1, \cdots, D_{2^m}\}$ is unsatisfiable. For example, given an assignment $u_1\mapsto1$, $u_2\mapsto0$, $u_3\mapsto0$, the clause $\{\bar u_1,u_2,u_3\}$ is not satisfied.