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
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
It is an especially important approach when dealing with incompatibilities that has more than two terms. Which is rare in our use case.
But I agree that The data structures behind unit propagation, are going to be some of the next performance improvements.
Actual implementation may be more relevant than the theoretical descriptions I have read.
Last updated: Oct 21 2021 at 20:21 UTC