code: def dpll_satisfiable(expr):
      """
      Check satisfiability of a propositional sentence.
      It returns a model rather than True when it succeeds
  
      >>> from sympy.abc import A, B
      >>> from sympy.logic.algorithms.dpll import dpll_satisfiable
      >>> dpll_satisfiable(A & ~B)
      {A: True, B: False}
      >>> dpll_satisfiable(A & ~A)
      False
  
      """
      if not isinstance(expr, CNF):
          clauses = conjuncts(to_cnf(expr))
      else:
          clauses = expr.clauses
      if False in clauses:
          return False
      symbols = sorted(_find_predicates(expr), key=default_sort_key)
      symbols_int_repr = set(range(1, len(symbols) + 1))
      clauses_int_repr = to_int_repr(clauses, symbols)
      result = dpll_int_repr(clauses_int_repr, symbols_int_repr, {})
      if not result:
          return result
      output = {}
      for key in result:
          output.update({symbols[key - 1]: result[key]})
      return output
  
file_path: sympy/sympy/logic/algorithms/dpll.py
imports: from sympy.core.sorting import default_sort_key
  from sympy.logic.boolalg import Or, Not, conjuncts, disjuncts, to_cnf, to_int_repr, _find_predicates
  from sympy.assumptions.cnf import CNF
  from sympy.logic.inference import pl_true, literal_symbol
label_desc: Use image node_id 1 for calling a global function with example usage: dpll_satisfiable(expr) and returns: output, False, result