I'm trying to wrap my head around an NP-completeness proof which seem to revolve around SAT/3CNF-SAT.

Maybe it's the late hour but I'm afraid I can't think of a 3CNF formula that cannot be satisfied (I'm probably missing something obvious).

Can you give me an example for such formula?


2 Answers 2


Technically, you can write $x\wedge \neg x$ in 3-CNF as $(x\vee x\vee x)\wedge (\neg x\vee \neg x\vee \neg x)$, but you probably want a "real" example.

In that case, a 3CNF formula needs at least 3 variables. Since each clause rules out exactly one assignment, that means you need at least $2^3=8$ clauses in order to have a non-satisfiable formula. Indeed, the simplest one is:

$$(x\vee y\vee z)\wedge (x\vee y\vee \neg z)\wedge (x\vee \neg y\vee z)\wedge(x\vee \neg y\vee \neg z)\wedge(\neg x\vee y\vee z)\wedge(\neg x\vee y\vee \neg z)\wedge(\neg x\vee \neg y\vee z)\wedge(\neg x\vee \neg y\vee \neg z)$$ It is not hard to see that this formula is unsatsifiable.

  • $\begingroup$ perhaps I'm being rather naive here, but why can't you perform a series of comparisons to determine if there are $2^v$ sets of non-equivalent expressions? - $v$ is the number of unique variables. If I have counted correctly, there are only $\frac{n(n-1)}{2}$ comparisons to be made $\endgroup$ Jul 8, 2019 at 16:19
  • $\begingroup$ @BenCrossley - not sure what you mean. Can you give an example? $\endgroup$
    – Shaull
    Jul 8, 2019 at 17:31

If you want more complex examples of such formulas, have a look some benchmark problems of SATLIB. ToughSAT is also a nice tool for creating 3-SAT instances; it's easy to build both satisfiable and unsatisfiable instances.


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.