pub fn models_of(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<u64>Expand description
The satisfying assignments of a CNF, each packed into the low num_vars bits of a u64. Brute force
over 2^{num_vars} — small n only (the census / symmetry-measurement regime).