Skip to main content

weighted_model_count_solve_counts

Function weighted_model_count_solve_counts 

Source
pub fn weighted_model_count_solve_counts(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> (usize, usize)
Expand description

(orbit_solves, total_models) — how many solve() calls the symmetry-accelerated weighted count makes (one per model-orbit) versus the number of models. Equal with no usable symmetry, smaller when symmetry fuses models into orbits.