2016-11-24 13:13 GMT+01:00 Vsevolod Stakhov <vsevo...@highsecure.ru>: > On 23/11/2016 16:27, Ed Schouten wrote: >> Hi Hans, >> >> 2016-11-23 15:27 GMT+01:00 Hans Petter Selasky <h...@selasky.org>: >>> I've made a patch to hopefully optimise SAT solving in our pkg utility. >> >> Nice! Do you by any chance have any numbers that show the performance >> improvements made by this change? Assuming that the SAT solver of >> pkg(1) uses an algorithm similar to DPLL[1], a change like this would >> affect performance linearly. My guess is therefore that the running >> time is reduced by approximately 5/12. Is this correct? > > There won't be any improvement if you just remove duplicates from SAT > formula. This situation is handled by picosat internally and even for > naive DPLL there is no significant influence of duplicate KNF clauses: > once you've assumed all vars in some clause, you automatically resolve > all duplicates.
Exactly. This is why I've stated: it affects performance linearly. Referring to Wikipedia's pseudo-code of the algorithm: the number of calls to unit-propagate() and pure-literal-assign() drops linearly, but the recursion will stay the same. -- Ed Schouten <e...@nuxi.nl> Nuxi, 's-Hertogenbosch, the Netherlands KvK-nr.: 62051717 _______________________________________________ freebsd-current@freebsd.org mailing list https://lists.freebsd.org/mailman/listinfo/freebsd-current To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"