def dpll_satisfiable(expr, all_models=False):
 clauses = conjuncts(to_cnf(expr))
 if (False in clauses):
  if all_models:
   return (f for f in [False])
  return False
 symbols = sorted(_find_predicates(expr), key=default_sort_key)
 symbols_int_repr = range(1, (len(symbols) + 1))
 clauses_int_repr = to_int_repr(clauses, symbols)
 solver = SATSolver(clauses_int_repr, symbols_int_repr, set(), symbols)
 models = solver._find_model()
 if all_models:
  return _all_models(models)
 try:
  return next(models)
 except StopIteration:
  return False

def dpll_satisfiable ( expr , all_models = False ) : clauses = conjuncts ( to_cnf ( expr ) ) if ( False in clauses ) : if all_models : return ( f for f in [ False ] ) return False symbols = sorted ( _find_predicates ( expr ) , key = default_sort_key ) symbols_int_repr = range ( 1 , ( len ( symbols ) + 1 ) ) clauses_int_repr = to_int_repr ( clauses , symbols ) solver = SATSolver ( clauses_int_repr , symbols_int_repr , set ( ) , symbols ) models = solver . _find_model ( ) if all_models : return _all_models ( models ) try : return next ( models ) except StopIteration : return False
check satisfiability of a propositional sentence .