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?
The reason why the SAT solver is slow is unlikely to be the size of the clauses, but rather the hardness of the problem itself.

In any case, any instance of CNF-SAT can notoriously be transformed into an equisatisfiable formula with at most three literals per clause by replacing each clause in the form:

$$
( x_1 \vee x_2 \vee \dots \vee x_n)
$$

with:

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