Can you help me find some examples of 3co-SAT for 4 variables?

Question

I've been studying the examples of 3co-SAT recently.

It's easy to find an example of one variable.

$(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$

Examples of 2 variables are as follows.

$(x_1\lor x_2\lor x_2)\land (x_1\lor \overline{x_2}\lor \overline{x_2})\land (\overline{x_1}\lor x_2 \lor x_2) \land (\overline{x_1}\lor \overline{x_2}\lor \overline{x_2})$

Examples of 3 variables are as follows.

$(x_1\lor x_2\lor x_3)\land (x_1\lor x_2\lor \overline{x_3})\land (x_1\lor \overline{x_2} \lor x_3) \land (x_1\lor \overline{x_2}\lor \overline{x_3}) \\ \land (\overline{x_1}\lor x_2 \lor x_3)\land (\overline{x_1} \lor x_2 \lor \overline{x_3}) \land (\overline{x_1} \lor \overline{x_2} \lor x_3) \land (\overline{x_1} \lor \overline{x_2} \lor \overline{x_3})$

But I can't find examples of four variables. Can you help me find some examples of 3co-SAT for 4 variables?

Answer 1

CNF is only used to describe problem formally, but it's kind of hard for human to understand it. Entailment is such tool that used to write "readable" formula. You can use propositional rules to give a contradiction.

Here is how i work it out:

First, given an unsatisfied clause using Entailment:

$A\wedge B\rightarrow C\wedge D, \neg(C\wedge D)\rightarrow (A\wedge B),\neg(C\wedge D)$

This breaks the Transpostion, it's certainly unsatifiable.

Secondly, rewrite it to CNF. For short, I use comma instead of a lot of $\wedge$s.

$$ (\neg A\vee \neg B) \vee (C\wedge D), (C\wedge D)\vee (A \wedge B),\neg C\vee \neg D $$

Use rules to simplify that, we get

$$ \neg A\vee \neg B\vee C,\neg A\vee \neg B\vee D, C\vee A,C\vee B, D\vee A, D\vee B, \neg C\vee \neg D $$

The variables in clause are less than 3. If you want a strict 3-CNF, you can simply repeat some literal in that clause.

May this help you.