Composer API
Class

Composer\DependencyResolver\RuleWatchGraph

class RuleWatchGraph

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.

Methods

insert(RuleWatchNode $node)

Inserts a rule node into the appropriate chains within the graph

Rule|null propagateLiteral(int $decidedLiteral, int $level, Decisions $decisions)

Propagates a decision on a literal to all rules watching the literal

Details

at line 41
public insert(RuleWatchNode $node)

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.

Parameters

RuleWatchNode $node The rule node to be inserted into the graph

at line 79
public Rule|null propagateLiteral(int $decidedLiteral, int $level, Decisions $decisions)

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.

Parameters

int $decidedLiteral The literal which was decided (A in our example)
int $level The level at which the decision took place and at which all resulting decisions should be made.
Decisions $decisions Used to check previous decisions and to register decisions resulting from propagation

Return Value

Rule|null If a conflict is found the conflicting rule is returned