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.

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

1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.