class RuleWatchGraph (View source)
The RuleWatchGraph efficiently propagates decisions to other rules
All rules generated for solving a SAT problem should be inserted into the graph. When a decision on a literal is made, the graph can be used to propagate the decision to all other rules involving the literal, leading to other trivial decisions resulting from unit clauses.
at line 41
Inserts a rule node into the appropriate chains within the graph
The node is prepended to the watch chains for each of the two literals it watches.
Assertions are skipped because they only depend on a single package and have no alternative literal that could be true, so there is no need to watch changes in any literals.
Propagates a decision on a literal to all rules watching the literal
If a decision, e.g. +A has been made, then all rules containing -A, e.g. (-A|+B|+C) now need to satisfy at least one of the other literals, so that the rule as a whole becomes true, since with +A applied the rule is now (false|+B|+C) so essentially (+B|+C).
This means that all rules watching the literal -A need to be updated to watch 2 other literals which can still be satisfied instead. So literals that conflict with previously made decisions are not an option.
Alternatively it can occur that a unit clause results: e.g. if in the above example the rule was (-A|+B), then A turning true means that B must now be decided true as well.