Refine clause reduction and vivification

[shnarazk]

Changes in reduce (this branch vs. dev-0.19.0)

1. Retention criterion rebuilt around an adaptive "height" threshold

The old ladder of fixed thresholds pairing dynamically recomputed LBD with reference rate is gone. Each clause is now scored by its stored reference height plus stored LBD, and kept if that falls below a threshold derived from slow-moving averages of conflict and backjump levels — so the keep/drop boundary adapts to how deep the solver is currently working. A kept clause must also be well-anchored (low reference height) or recently referred to.

2. Recency anchor changed from restarts to a fixed conflict window

"Used since the last restart?" became "referred to within the last several hundred thousand conflicts?". The signature changed accordingly: reduce now takes the solver state instead of the last-restart timestamp.

3. Length-based protection deliberately removed

Clauses of three or fewer literals are no longer unconditionally kept; a comment notes that length without context makes results worse.

4. Cheaper bookkeeping and a different activity model

LBD is no longer recomputed per clause during reduction — the stored value is trusted, making the pass much lighter. The floating-point reference-rate EMA is replaced by a reference height in decision levels, and the tier statistics are now simple stored-LBD bands.

Changes in vivify (this branch vs. dev-0.19.0)

1. Rescheduling heuristic rewritten (the core change)

The old linear cooldown — anchored to the last reference, with a hard retirement after eight attempts — is replaced by an exponential backoff: the interval doubles with each attempt, scales with clause length, and is anchored to the last vivification. A learnt or previously vivified clause is only reconsidered if it has been referred to since its last vivification. The hard retirement age is gone; instead, a failed attempt ages a clause by two, a successful one by one, so unproductive clauses back off faster.

2. The length/LBD band filter was dropped

Clauses that were too short or had a high current LBD used to be skipped. Now every clause passing the scheduling check is attempted.

3. Clause bookkeeping simplified

The reference-rate EMA decay helper is gone; the loop stamps the vivification time and age directly on the clause. A shortened replacement clause inherits the original's reference height, vivification timestamp, and age.

4. Shrunken clauses get a refreshed LBD

A shortened clause's LBD is capped at the number of decisions used to derive it, so it immediately looks as good as it now is to the reduction machinery.

RephaseTarget::Polarity (new on this branch vs. dev-0.19.0)

1. New Var::polarity field

Each variable now carries a long-term phase bias (src/types/var.rs): an
exponential moving average updated on every backtrack, drifting toward +1.0 if
the variable keeps getting assigned true, toward -1.0 if false, and staying
near 0.0 if it flips around.

2. New rephase mode

Under Polarity (src/assign/propagate.rs), the saved phase is chosen
stochastically: the stronger a variable's accumulated bias, the more likely it
keeps its current assignment; weakly biased variables tend to get flipped. It
sits between Walk (always keep) and Inverted (always flip), concentrating
randomness on variables without a settled "personality".