Re: Optimising generated rules for SAT solving (5/12 are duplicates)

From: Ed Schouten <ed_at_nuxi.nl>
Date: Wed, 23 Nov 2016 17:27:42 +0100
Hi Hans,

2016-11-23 15:27 GMT+01:00 Hans Petter Selasky <hps_at_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_at_nuxi.nl>
Nuxi, 's-Hertogenbosch, the Netherlands
KvK-nr.: 62051717
Received on Wed Nov 23 2016 - 15:28:14 UTC

This archive was generated by hypermail 2.4.0 : Wed May 19 2021 - 11:41:08 UTC