public function propagateLiteral($decidedLiteral, $level, $decisions)
    {
        // we invert the decided literal here, example:
        // A was decided => (-A|B) now requires B to be true, so we look for
        // rules which are fulfilled by -A, rather than A.
        $literal = -$decidedLiteral;

        if (!isset($this->watchChains[$literal])) {
            return null;
        }

        $chain = $this->watchChains[$literal];

        $chain->rewind();
        while ($chain->valid()) {
            $node = $chain->current();
            $otherWatch = $node->getOtherWatch($literal);

            if (!$node->getRule()->isDisabled() && !$decisions->satisfy($otherWatch)) {
                $ruleLiterals = $node->getRule()->getLiterals();

                $alternativeLiterals = array_filter($ruleLiterals, function ($ruleLiteral) use ($literal, $otherWatch, $decisions) {
                    return $literal !== $ruleLiteral &&
                        $otherWatch !== $ruleLiteral &&
                        !$decisions->conflict($ruleLiteral);
                });

                if ($alternativeLiterals) {
                    reset($alternativeLiterals);
                    $this->moveWatch($literal, current($alternativeLiterals), $node);
                    continue;
                }

                if ($decisions->conflict($otherWatch)) {
                    return $node->getRule();
                }

                $decisions->decide($otherWatch, $level, $node->getRule());
            }

            $chain->next();
        }

        return null;
    }