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

On 23/11/2016 16:27, Ed Schouten wrote:
> 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?

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