# Breaking down CNF clauses

I have an assignment where i have to encode certain problem to conjunctive normal form so i can solve it by using SAT solver. I have been able to encode my problem correctly but the solver is quite slow and most likely the cause for this is the length of some clauses which i have.

So my question is:

How can one break down long clauses into smaller ones and therefore speed up the SAT solver, lets say i have following clause:

$(x_1 \vee x_2 \vee x_3 \vee ... \vee x_n)$ where n can potentially be large number.

Is there any way to split this into smaller clauses which would be logically equivalent?

• Every CNF is equivalent to a 3CNF, in which every clause contains at most 3 literals. You can see the reduction in any NP-completeness proof of 3SAT. I'm not sure that will speed up to SAT solver, though. – Yuval Filmus Feb 2 '17 at 20:03

$$( x_1 \vee x_2 \vee \dots \vee x_n)$$
$$(x_1 \vee x_2 \vee y_1) \wedge (\neg y_1 \vee x_3 \vee y_2) \wedge \dots \wedge (\neg y_{n-4} \vee x_{n-2} \vee y_{n-3}) \wedge (\neg y_{n-3} \vee x_{n-1} \vee x_n)$$
where $\{y_i\}_{i \in \mathbb{N}}$ are fresh variables.