13
$\begingroup$

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?

$\endgroup$
27
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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