Polarity driven rephasing 20260617

[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".

[shnarazk]

~/.cargo/bin/splr (0.19.0-rc7) @ 2026-07-14T08:06:06

#	target CNF solved by splr	time (s)	ret
1	0a8a4c28d27228e954354ea0a6e7f16c-sum_of_three_cubes_		124
2	1a936d41e3439d602c3ddcf96458a38c-arles_thres10_p10_r	0.27	20
3	2b4467a5ac4ac41b36d4c3432b07f767-oddball_69_5_tto_zp	2016.18	10
4	3a1f1b4b9a521737cc760017fe9d8b43-MVRoundRobin_n16_d1		124
5	4ba2c1aa580b6497df6baf5e7e2c87be-at-least-two-vmpc_2	314.09	10
6	5aed29ce52192a55ffbd2a6f340017e7-oisc-subrv-and-nest		124
7	6cb995b1c550beb579c53e27f6ca881a-RoundRobin_n16_d13.		124
8	7a044c997ede14d00002f1db39d45170-sum_of_3_cubes_37_b	1331.38	10
9	8a05f9b6bf49285e40d0a197967ea5d3-arles_thres10_p10_r	0.71	20
10	9a839badecb20dcf505ec79eedd3753a-anbul-dated-5-15-u.	170.23	20
11	a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r	0.11	20
12	b1c8eaa002ac2fa1c8bfd1002738e78e-cliquecolouring_n15		124
13	c0bd86bd7ca2c65e44311de374168150-goldcrest-and-14.cn	3578.96	20
14	d0298807e51730261ef65db827dcd70f-Break_triple_16_70.	375.44	10
15	e2d2b011b0805782df6adba648db92e8-59-129706.cnf	4172.84	10
16	f0bafebdcce23ccfbaf6c27a7522069b-div-mitern172.cnf	757.74	20

"splr" , med: 375.44, max: 4172.84,total except 5 timeouts:12717.95