1795. Which Switches Have No Say In It

There are n switches and k rules. Each rule names two conditions and demands that at least one of them holds. The condition written i is "switch i is ON" and the condition written -i is "switch i is OFF". A rule may name the same switch twice, so 3 3 demands that switch 3 is ON and 2 -2 demands nothing at all.

A SETTING assigns ON or OFF to every switch. Call switch i STUCK if every setting that satisfies all k rules gives i the same value. Print how many switches are stuck, or No if no setting satisfies all the rules.

Problem 1725 asks only whether a setting exists. Problem 1726 prints the lexicographically smallest one. This asks which switches have no choice at all, which is a question about every setting at once rather than about one of them.

## What most people try first

Solving once and reporting the switches that came out ON. That describes one setting. With no rules at all, the smallest setting is everything OFF and nothing is stuck.

The second attempt is "switch i is stuck when some rule mentions i twice with the same sign", which catches 3 3 and misses everything else. In the rules -1 2, -2 1, 1 1 no rule pins switch 2 directly, and switch 2 is still stuck ON, because switch 1 is pinned ON and the first rule carries it across.

The third is to solve, then flip switch i, then check the rules again. Flipping one switch usually breaks a rule that could have been repaired by flipping another, so that reports far too many switches as stuck. The rules -1 2, -2 1 have exactly two settings, both OFF and both ON; flipping switch 1 alone breaks a rule, and neither switch is stuck.

## The implication graph, and what reachability means in it

Build a node for every condition, 2n of them. A rule a b says that if a fails then b must hold, and if b fails then a must hold, so draw an arc from NOT a to b and an arc from NOT b to a. A setting satisfies all the rules exactly when the set of true conditions is closed under these arcs.

> Switch i is stuck ON exactly when the node "i is OFF" reaches the node > "i is ON". Switch i is stuck OFF exactly when "i is ON" reaches "i is > OFF".

One direction is immediate. If "i is OFF" reaches "i is ON" then any setting with i OFF makes that first condition true, so by following the arcs it makes "i is ON" true as well, and a setting cannot have i both ways. So no satisfying setting has i OFF.

The other direction is the real claim: with no such path, some satisfying setting really does have i OFF. Adding the rule -i -i draws the single new arc from "i is ON" to "i is OFF". The enlarged formula can only fail if some switch j has both of its conditions in one strongly connected component, which needs a cycle through the new arc, so a path j is ON -> ... -> i is ON and a path i is OFF -> ... -> j is OFF. The implication graph is skew symmetric: an arc from p to q always comes with an arc from NOT q to NOT p, so a path j is ON -> ... -> i is ON mirrors into a path i is OFF -> ... -> j is OFF, and together with the other half these give a path from "i is OFF" to "i is ON", which we assumed does not exist.

A switch cannot be stuck both ways while the formula is satisfiable, so the two tests never both fire and a single count is enough.

``` n = 3, rules: 1 1 -> arcs (1 OFF) -> (1 ON) twice -1 2 -> arcs (1 ON) -> (2 ON), (2 OFF) -> (1 OFF) 3 -3 -> arcs (3 OFF) -> (3 OFF), (3 ON) -> (3 ON)

switch 1: (1 OFF) -> (1 ON) stuck ON switch 2: (2 OFF) -> (1 OFF) -> (1 ON) -> (2 ON) stuck ON switch 3: no path either way free answer: 2 ```

## The boundary that breaks a careless implementation

Check satisfiability FIRST. In an unsatisfiable formula both tests fire for some switch and the count is meaningless, so the answer is No and nothing else.

A rule naming the same switch with opposite signs, like 2 -2, is satisfied by both values and must not be dropped, because it still contributes two arcs and those arcs are real: 2 OFF -> 2 OFF and 2 ON -> 2 ON, both harmless but present. A rule naming it twice with the same sign pins it.

Build every traversal with an explicit stack. At n = 300 the graph has 600 nodes and a chain of implications can run through all of them, which is fine for a stack and not for Python's 1000-frame recursion limit once the search is nested inside another.

## Cost

Satisfiability is one pass of a strongly-connected-component search, O(n + k). The stuck test is a traversal from each of the 2n nodes, O(n * k). At n = 300 and k = 2000 that is 600 traversals over 4000 arcs, about 2.4 * 10^6 steps.

## Overflow

Every number printed is a count of switches, at most 300.

Constraints - `1 ≤ n ≤ 300` - `0 ≤ k ≤ 2000` - `1 ≤ abs(a) ≤ n` and `1 ≤ abs(b) ≤ n`, and neither `a` nor `b` is 0 - a rule may name the same switch twice, with the same sign or with opposite signs - the same rule may be listed more than once - with `k = 0` every setting satisfies every rule, so no switch is stuck