unicode_fol_kit.find_model

unicode_fol_kit.find_model(formulas, max_size=4, max_candidates=1048576)

Return a finite Structure satisfying every formula, or None.

Searches domains of size 1 .. max_size in turn, enumerating every interpretation of the theory’s signature and returning the first structure in which all formulas hold. A domain size whose interpretation space exceeds max_candidates is skipped (so a return of None is bounded, not a proof of unsatisfiability).

Parameters:

• max_size (int)

• max_candidates (int)

Return type:

Structure | None