Is generating MIN-3-UNSAT $\mathsf{NP}$-hard?

Question

Input: amount of variables (with minimum of $10$ since otherwise problem is unsolvable).

Output: unsatisfiable formula.

Restrictions:

1. Every clause contains exactly 3 variables.
2. Every clause differs by at least one variable. For example, a pair of clauses $(x\lor y\lor z)\land(x\lor \overline y\lor\overline z)$ is forbidden.
3. Every variable must be involved.
4. Removing any clause makes the formula satisfiable.

No set of clauses is given as input. Is this problem in $\mathsf{FP}$ or is it $\mathsf{NP}$-hard?

Answer 1

The smallest formula with $n=10$ can be written as follows:

$(x_1\rightarrow(x_2\rightarrow x_3))\land(x_1\rightarrow(x_3\rightarrow x_4))\land(x_1\rightarrow(x_4\rightarrow\overline{x_2}))\land$ $(x_1\rightarrow(\overline{x_2}\rightarrow x_5))\land(x_1\rightarrow(x_5\rightarrow x_6))\land(x_1\rightarrow(x_6\rightarrow x_2))\land$ $(\overline{x_1}\rightarrow(x_2\rightarrow x_7))\land(\overline{x_1}\rightarrow(x_7\rightarrow x_8))\land(\overline{x_1}\rightarrow(x_8\rightarrow\overline{x_2}))\land$ $(\overline{x_1}\rightarrow(\overline{x_2}\rightarrow x_9))\land(\overline{x_1}\rightarrow(x_9\rightarrow x_{10}))\land(\overline{x_1}\rightarrow(x_{10}\rightarrow x_2))$

It satisfies all of the restrictions.

As you can see, it is just two unsatisfiable 2-SAT formulas one of which is implied by $x_1$ and another by $\overline{x_1}$. We can add arbitrary amount of vertices to any of these implication chains, so, generating such formula for any $n\ge10$ can be done in linear time.