redundant clauses, impact performance?

[Bikes4Fun]

How impactful will multiple identical clauses be on performance? Eg, (-a -b) occurring 2, 3 or 4 times along with others. Given our data structure, it will be a decent sized project to weed out where duplicates will naturally occur. I'm trying to gauge where to best place efforts for final performance. A bit of extra encoding on my end + a few extra seconds or even minutes running the data would need to significantly boost performance at the solver level.

[DvonHolten]

duplicate clauses will be detected and removed in any decent solver during loading or preprocessing. It's cheap.
The question is: where do these duplicates come from?
If you really want to get rid of them, you can sort the cnf-file and remove duplicates - take care of the header, though.

btw: the solver will detect duplicates like ( -a -b) and ( -b -a ) as well

[arminbiere]

Yep, there are many pre- and inprocessing techniques which would find and remove duplicates, i.e., subsumption, vivification. Actually some of them even need to do that for correctness, such as removing duplicated binary clauses. So it is completely harmless to keep them in the input.

[Bikes4Fun]

Thank you :) I assumed they would be filtered out quickly but wanted to be sure so I can focus efforts elsewhere. Thank you again!