Breaking down CNF clauses
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.