Look into two-watched-literal scheme

[mpizenberg]

It was mentioned in a comment on reddit so may be worth exploring.

[mpizenberg]

Explanation from reddit:

The two watched literal scheme is used while unit propagation. You can propagate if only one literal is left in a nogood and when every literal in a nogood is in the assignment you have a conflict. In all other cases nothing happens. Since you only care about going from two unset literals to one you have only to watch two literals.

http://haz-tech.blogspot.com/2010/08/whos-watching-watch-literals.html?m=1 http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf

[Eh2406]

This is closely tied to #19. #19 points out that we can reduce the number of incompatibilities we need to check by preemptively combining ones that have the same semantic meaning. This one points out that we can reduce the number of incompatibilities we need to check by paying attention to their size.

An incompatibility that refers only to one package, I have been referring to as unitary. They all say "there is a fundamental problem with this package" (except for NotRoot). They are always relevant, no matter what decisions we have made. Equivalently, they are always either "almost satisfied" or "contradicted". It only takes checking one Term intersection to determine if any of them are relevant. (We can do this by storing a special term for checking, or by actually combining them into one incompatibility. Depending on how aggressive we want to be with #19.) These incompatibilities tend to be rare when resolution is on the path to success, and extremely common when resolution is a having trouble. Aggressively combining these is the biggest fix for #135

An incompatibility that has two terms can also be handled specially. By storing these in a trie, it should be very efficient to identify "dependence merge" cases for #19. And possibly reduce the number of terms that need to be intersected to identify almost satisfied terms.

Incompatibilities that have more terms, are extremely rare in our data sets. However when they occur they require a lot of intersections to determine if they are relevant. A two-watched-literal scheme reduces the cost to basically the same as the two terms case. Instead of storing a vector of incompatibilities each one of which needs to have all of its terms checked, we can store a vector of (P1, P2, incompatibility). Where P1 and P2 pointed to two terms that are not Satisfied. We only need to reevaluate if one of those terms is Satisfied. (This is because we only take action when an incompatibility goes from 2 unsatisfied terms to 1, or from 1 to 0.) If on closer evaluation there is some different set of terms that mean that no action is needed we change P1 or P2 so that they are both not Satisfied. The fun part about this scheme is that we do not need to take any action when backtracking, as neither term can become satisfied by backtracking.