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

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.

• @Nathaniel Thanks for your reminder and help.
– Jxb
Nov 8, 2022 at 2:39

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.