pub fn min_res_width_clauses(
num_vars: usize,
clauses: &[Vec<Lit>],
convention: WidthConvention,
) -> Option<usize>Expand description
The minimum resolution-refutation width under a convention: the least w whose closure derives
the empty clause. None iff the formula is satisfiable (resolution is complete at w = num_vars).