Function random_ksat 

pub fn random_ksat(
    k: usize,
    vars: usize,
    num_clauses: usize,
    seed: u64,
) -> DimacsCnf

A random k-SAT instance: num_clauses clauses of k distinct variables with random signs, over vars variables, from a seeded SplitMix64 stream (reproducible — no wall-clock). Generalizes random_3sat. The satisfiability threshold climbs with k roughly as α_k ≈ 2ᵏ ln 2 (≈ 4.27 for k=3, ≈ 9.93 for k=4, ≈ 21.1 for k=5). Requires k ≤ vars.