Date: Wed, 23 Nov 2016 17:27:42 +0100 From: Ed Schouten <ed@nuxi.nl> To: 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: <CABh_MKm7LAtQzp9KEBpaRZWQQHnsUtNFiKVSVF70-wj4GmytuA@mail.gmail.com> In-Reply-To: <cbc964a7-5f90-6ea1-630d-414de68867b1@selasky.org> 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>
next in thread | previous in thread | raw e-mail | index | archive | help
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? 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 -- Ed Schouten <ed@nuxi.nl> Nuxi, 's-Hertogenbosch, the Netherlands KvK-nr.: 62051717
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?CABh_MKm7LAtQzp9KEBpaRZWQQHnsUtNFiKVSVF70-wj4GmytuA>