pkg icon indicating copy to clipboard operation
pkg copied to clipboard

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

Open hselasky opened this issue 9 years ago • 3 comments

Hi,

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

pkg_rule_optimise.diff.zip

--HPS

hselasky avatar Nov 23 '16 14:11 hselasky

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

tigergao99 avatar Nov 23 '20 18:11 tigergao99

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

igalic avatar Nov 23 '20 18:11 igalic

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?

vstakhov avatar Nov 23 '20 20:11 vstakhov