Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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?
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.
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.
