Stream: t-cargo/PubGrub

Topic: two-watched-literal


view this post on Zulip Matthieu Pizenberg (Jul 05 2021 at 00:17):

There was a reddit comment from I think (but not sure) Sven Thiele, which is now following the project and is a member of Potassco (the group at the origin of the algorithm used by pubgrub) suggestion to look into the "two-watched-literal" scheme: https://github.com/pubgrub-rs/pubgrub/issues/101

view this post on Zulip Matthieu Pizenberg (Jul 05 2021 at 00:19):

From very briefly looking into the first link, it seems to handle more efficiently unit propagation, which is where we spend most of our time. So it may be worth exploring, in addition to new API

view this post on Zulip Eh2406 (Jul 05 2021 at 00:43):

It is an especially important approach when dealing with incompatibilities that has more than two terms. Which is rare in our use case.

view this post on Zulip Eh2406 (Jul 05 2021 at 00:44):

But I agree that The data structures behind unit propagation, are going to be some of the next performance improvements.

view this post on Zulip Eh2406 (Jul 05 2021 at 00:58):

Actual implementation may be more relevant than the theoretical descriptions I have read.


Last updated: Oct 21 2021 at 20:21 UTC