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?