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

Output: unsatisfiable formula.


  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?

  • $\begingroup$ 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.] $\endgroup$
    – D.W.
    Commented Aug 11, 2017 at 16:07

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


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.