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

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?

• I doubt it is NP-hard, since it is in P/poly. So, I suggest you look for a polynomial-time algorithm for the problem before trying to prove NP-hardness. Of course, the answer might be that it is neither in FP nor NP-hard. [Possibly related, but probably not that helpful: cstheory.stackexchange.com/q/8117/5038, cs.stackexchange.com/q/79628/755.] – D.W. Aug 11 '17 at 16:07

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))$
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.