pkg - roughly half of generated SAT rules are duplicates when doing pkg upgrade

[hselasky]

Hi,

The following patch sorts the SAT rules and eliminate duplicates before passing onto the SAT solver.

pkg_rule_optimise.diff.zip

--HPS

[tigergao99]

Hello @hselasky , has this patch been PR/merge'd?

[igalic]

i imagine if this had been submitted as pull-request, it would have been easier.

i can try that tonight…, depending on how much conflicts there are, given that this patch is from four years ago

[vstakhov]

Yes, exactly! I've just noticed this patch that might have attracted my attention being submitted as a PR.

The problem is that identical rules are not a problem for PicoSAT or any other advanced SAT solver - they use conflicts driven solving algorithm that efficiently either include all duplicates in a conflicts chain or totally exclude non-conflicting clauses. Are there any performance improvements in SAT process after this change?