2
$\begingroup$

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)$

$\endgroup$
3
$\begingroup$

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.

$\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.