unicode_fol_kit.is_satisfiable_finite¶ unicode_fol_kit.is_satisfiable_finite(formula, max_size=4, max_candidates=1048576)[source]¶ True iff formula has a finite model of size ≤ max_size (bounded). Parameters: formula (Node) max_size (int) max_candidates (int) Return type: bool