I want to know in general how can I convert $4-SAT$ to 3-SAT.

And I have a specific case that if you can help me optimize it to 3-SAT it will be greate.

I want to do this so I be able to use sat solvers programs.

$(C \lor A \lor D) \land (C \lor B \lor D) \land (\lnot C \lor A \lor \lnot D) \land (\lnot C \lor B \lor \lnot D) \land (C \lor \lnot A \lor \lnot B \lor \lnot D) \land (\lnot C \lor \lnot A \lor \lnot B \lor D)$


1 Answer 1


Every clause is of the form $(x_1 \vee x_2 \vee x_3 \vee x_4)$, where $x_i$, $i \in [4]$ is a literal. Replace every such clause with two clauses $(x_1 \vee x_2 \vee z) \wedge (\neg z \vee x_3 \vee x_4)$, where $z$ is a fresh variable. You can then verify that if some setting of $x_i$'s satisfies the original clause, you can find a setting of $z$ such that the two clauses are satisfied.

However, note that if you want to use a SAT solver, none of this is needed. A standard SAT solver can handle clauses of any length, and different clauses can be of different length.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .