pkg
pkg copied to clipboard
pkg - roughly half of generated SAT rules are duplicates when doing pkg upgrade
Hi,
The following patch sorts the SAT rules and eliminate duplicates before passing onto the SAT solver.
--HPS
Hello @hselasky , has this patch been PR/merge'd?
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
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?