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

On 11/24/16 13:13, Vsevolod Stakhov wrote:
> 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.

Hi,

I added some code to measure the time for SAT solving. During my test 
run I'm seeing values in the range 8-10ms for both versions, so I 
consider that neglible. However, the unpatched version wants to 
reinstall 185 packages while the non-patched version wants to reinstall 
1 package. That has a huge time influential. I'm not that familar with 
PKG that I can draw any conclusions from this.

# Test1:
echo "n" | /xxx/pkg/src/pkg-static upgrade --no-repo-update > b.txt

# Test2:
echo "n" | env PKG_NO_SORT=YES /xxx/pkg/src/pkg-static upgrade 
--no-repo-update > a.txt

Please find the material attached including a debug version patch you 
can play with.

--HPS