def satisfiable(expr, algorithm='dpll2', all_models=False):
 expr = to_cnf(expr)
 if (algorithm == 'dpll'):
  from sympy.logic.algorithms.dpll import dpll_satisfiable
  return dpll_satisfiable(expr)
 elif (algorithm == 'dpll2'):
  from sympy.logic.algorithms.dpll2 import dpll_satisfiable
  return dpll_satisfiable(expr, all_models)
 raise NotImplementedError

def satisfiable ( expr , algorithm = 'dpll2' , all_models = False ) : expr = to_cnf ( expr ) if ( algorithm == 'dpll' ) : from sympy . logic . algorithms . dpll import dpll_satisfiable return dpll_satisfiable ( expr ) elif ( algorithm == 'dpll2' ) : from sympy . logic . algorithms . dpll2 import dpll_satisfiable return dpll_satisfiable ( expr , all_models ) raise NotImplementedError
check satisfiability of a propositional sentence .