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

From: Ed Schouten <>
Date: Thu, 24 Nov 2016 15:15:07 +0100
2016-11-24 13:13 GMT+01:00 Vsevolod Stakhov <>:
> On 23/11/2016 16:27, Ed Schouten wrote:
>> Hi Hans,
>> 2016-11-23 15:27 GMT+01:00 Hans Petter Selasky <>:
>>> 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 <>
Nuxi, 's-Hertogenbosch, the Netherlands
KvK-nr.: 62051717
Received on Thu Nov 24 2016 - 13:15:39 UTC

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