Function fractional_automorphism 

pub fn fractional_automorphism(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Vec<usize>

A fractional automorphism of a formula: a doubly-stochastic matrix B commuting with the variable co-occurrence matrix A (BA = AB) — the LP relaxation of an automorphism (a permutation matrix commuting with A). The canonical one is block-averaging over the coarsest equitable partition ([equitable_partition_of]): B[u][v] = 1/|cell(u)| if u,v share a cell, else 0. By Tinhofer’s theorem it commutes with A iff the partition is equitable, and it is non-trivial (not a permutation) exactly when the partition is non-discrete — i.e. exactly when the formula has non-trivial 1-WL symmetry.

Returns the partition cell[v]. Its non-discreteness certifies a fractional automorphism; the commutation BA = AB is checked exactly (over integers, by clearing the 1/|cell| denominators) by is_fractional_automorphism.