Filter the clique branching set by recolouring and infra-chromatic bounds

[ciaranm]

Adds --filter none|recolour|infra-chromatic to the clique solver, bringing in
recolouring (Tomita's Re-NUMBER, so MCSa → MCSb) and the infra-chromatic bound
(San Segundo, Nikolaev and Batsyn), fused into a single pass.

What it does

After colouring, every vertex whose colour is at least k_min is one we would
otherwise have to branch on. Both tests hang off the same quantity,
C_k1 & N(v), which is why they are fused as in San Segundo et al's
FILTER_RECOL_INFRACHROM:

• no neighbour of v in some class → v belongs there (one-move recolouring);
• exactly one neighbour w → either w moves to another class and v takes
  its place (double-move recolouring), or no vertex of a third class is
  adjacent to both v and w, in which case ({v}, C_k1, C_k2) admits no
  triangle with one vertex in each, and contributes two rather than three to
  the bound.

Recolouring alone does not pay for itself, which is Prosser's finding too
("MCSb1 is always slower than MCSa1, i.e. the colour repair is too expensive").
It pays once the second half of what condition I buys is also cashed in.

Results

Fifteen DIMACS instances, best of three, against plain MCSa1:

	nodes	ms
MCSa1	15,290,657	34,558
--filter recolour	8,507,454 (1.80×)	45,723 (0.76×)
--filter infra-chromatic	4,521,825 (3.38×)	26,137 (1.32×)

MANN_a27 is the useful control: recolouring gives 4.2× fewer nodes and 1.61×
faster, and the infra-chromatic test then adds nothing at all — 9,084 nodes
either way. It is near-perfect, so the colouring bound is already tight and
there are no conflicting triples to find.

Implementation notes

Classes below k_min are held as intrusive singly linked lists over one int
array, so a recolouring is O(1) and nothing is allocated per node. Condition I
is a walk over the class that bails at the second neighbour of v rather than
a bitset intersection: Prosser's Proposition 1 means the first neighbour is
always there to be found, and on a dense graph the second arrives after a
couple of tests — so failure, the common case, is where it is cheapest. A
bitset intersection has no such asymmetry and pays for every word every time.

Two things here are easy to get wrong, and both were caught by differential
fuzzing rather than by reading:

• Filtering removes a vertex from the branching set, not the candidate set.
  All we have shown is that we need not branch on it here; a clique through
  some other branching vertex may still need it. It stays in p, and the
  position is marked by negating its entry in p_bounds.
• Nogoods must not be posted for filtered vertices during a restart. A
  filtered vertex has no completed subtree behind it; all we know is that the
  classes below k_min and the filtered vertices cannot beat the incumbent
  between them, which says nothing until the rest of the branching set has
  been dealt with.

Proof logging

Works with --prove. A filtered vertex is never individually justified — only
the combined statement holds, that the classes below k_min, enlarged by
recolouring, together with one singleton per conflict, have clique number
k_min - 1. That is exactly why the colours a conflict spends are marked
forbidden: the sum only works if the conflicts are over disjoint classes.

Proof::colour_bound therefore takes the conflicts as a second argument and is
handed the recoloured classes. An inconsistent triple becomes an at-most-two
over the union of the three classes, derived by summing the non-edges from v
to what it cannot see, the at-most-one over the independent set inside its
neighbourhood, and nbar - 1 copies of the plain two-class bound so that every
coefficient is nbar and the division is legal; the right-hand side lands one
short of 3 * nbar and the rounding does the rest. Since reverse polish
composes, this is a subexpression and the bound remains a single pol line.

Proofs come out smaller, since the stronger bound means fewer nodes to log:

	nodes	proof MB	check s		nodes	proof MB	check s
	MCSa1				infra-chromatic
brock200_2	3,757	3.2	0.6		2,083	2.4	0.4
p_hat300-2	4,072	6.4	0.9		2,005	4.1	0.6
keller4	13,542	15.7	1.4		7,623	11.5	1.0

Testing

• ~2,700 random graphs plus 240 large dense ones, differential against
  --filter none, checking both ω and that the reported clique really is one;
  decide mode across k = ω ± 2; restarts enabled.
• ~1,060 instances with --prove, all checked by VeriPB 3.0.2, exercising
  ~2,800 conflict triples, no failures.
• Mutation tested: incrementing the divisor, or dropping the nbar - 1
  padding, both get rejected by VeriPB — so the check is load-bearing.
• All 41 unit tests and run-tests.bash pass. Node counts are unchanged with
  --filter none, which takes the same path as before.

Unrelated issue found in passing

--decide k --prove emits a proof VeriPB rejects when the answer is true;
the unsatisfiable direction is fine. This reproduces on a clean checkout of
master with no filtering, so it predates this branch — but it is worth
knowing before trusting a satisfiable decision proof.

🤖 Generated with Claude Code

https://claude.ai/code/session_012qVra2UG1rKEur4wa7w67w