Date: Thu, 24 Nov 2016 12:13:39 +0000 From: Vsevolod Stakhov <vsevolod@highsecure.ru> To: Ed Schouten <ed@nuxi.nl>, Hans Petter Selasky <hps@selasky.org> Cc: Baptiste Daroussin <bapt@freebsd.org>, Slawa Olhovchenkov <slw@zxy.spb.ru>, ports@freebsd.org, FreeBSD Current <freebsd-current@freebsd.org> Subject: Re: Optimising generated rules for SAT solving (5/12 are duplicates) Message-ID: <d786cde5-89af-cb14-c42e-cc649cb32bdb@highsecure.ru> In-Reply-To: <CABh_MKm7LAtQzp9KEBpaRZWQQHnsUtNFiKVSVF70-wj4GmytuA@mail.gmail.com> References: <20150414200459.GE39658@ivaldir.etoilebsd.net> <20150421103454.GR1394@zxy.spb.ru> <5593D0AE.2010205@selasky.org> <416359ce-1dcd-1160-5c56-f120a0f6358f@selasky.org> <20160627115533.gqvdsmtzwnvrrfuo@ivaldir.etoilebsd.net> <0671148b-d7cd-f8ad-906d-a0baa1b98cf5@selasky.org> <cbc964a7-5f90-6ea1-630d-414de68867b1@selasky.org> <CABh_MKm7LAtQzp9KEBpaRZWQQHnsUtNFiKVSVF70-wj4GmytuA@mail.gmail.com>
next in thread | previous in thread | raw e-mail | index | archive | help
On 23/11/2016 16:27, Ed Schouten wrote: > Hi Hans, > > 2016-11-23 15:27 GMT+01:00 Hans Petter Selasky <hps@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. Is there any real improvement of SAT solver speed with this patch? From my experiences, SAT solving is negligible in terms of CPU time comparing to other tasks performed by pkg. > By the way, why attach a zip file with a diff? GitHub's pull requests > are awesome! :-) > > [1] Davis-Putnam-Logemann-Loveland algorithm: > https://en.wikipedia.org/wiki/DPLL_algorithm > -- Vsevolod Stakhov
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?d786cde5-89af-cb14-c42e-cc649cb32bdb>