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

On 11/24/16 14:11, Vsevolod Stakhov wrote:
> On 24/11/2016 13:05, Hans Petter Selasky wrote:
>> 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
>>
>
> Then I don't understand how your patch should affect the solving
> procedure. If pkg tries to reinstall something without *reason* it is a
> good sign of bug in pkg itself and/or your database/repo and not in SAT
> solver.
>
> I'll try to review your issue but I'll likely need your local packages
> database for this test.
>

Hi,

Maybe it is a bug somewhere.

I noticed some rules repeating the same variable two times for example.

Send me the list of files you need off-list.

Thank you!

--HPS