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

[Ed Schouten]

2016-11-24 13:13 GMT+01:00 Vsevolod Stakhov <vsevolod at highsecure.ru>:
> 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.

Exactly. This is why I've stated: it affects performance linearly.
Referring to Wikipedia's pseudo-code of the algorithm: the number of
calls to unit-propagate() and pure-literal-assign() drops linearly,
but the recursion will stay the same.

-- 
Ed Schouten <ed at nuxi.nl>
Nuxi, 's-Hertogenbosch, the Netherlands
KvK-nr.: 62051717