I was instead thinking of making it <code>__semantic_tableaux</code> and add a model or return_model parameter to satisfiable function. <code>satisfiable(expr, algorithm="dpll2", model=True)</code> The end-user is very less likely to know what this function does and how it can be used. Its major use to evaluate unsatisfiability (and validity), so integrating it with the corresponding function would probably be a good idea.