code: def dpll_satisfiable(expr, all_models=False, use_lra_theory=False):
      """
      Check satisfiability of a propositional sentence.
      It returns a model rather than True when it succeeds.
      Returns a generator of all models if all_models is True.
  
      Examples
      ========
  
      >>> from sympy.abc import A, B
      >>> from sympy.logic.algorithms.dpll2 import dpll_satisfiable
      >>> dpll_satisfiable(A & ~B)
      {A: True, B: False}
      >>> dpll_satisfiable(A & ~A)
      False
  
      """
      if not isinstance(expr, EncodedCNF):
          exprs = EncodedCNF()
          exprs.add_prop(expr)
          expr = exprs
  
      # Return UNSAT when False (encoded as 0) is present in the CNF
      if {0} in expr.data:
          if all_models:
              return (f for f in [False])
          return False
  
      if use_lra_theory:
          lra, immediate_conflicts = LRASolver.from_encoded_cnf(expr)
      else:
          lra = None
          immediate_conflicts = []
      solver = SATSolver(
          expr.data + immediate_conflicts,
          expr.variables,
          set(),
          expr.symbols,
          lra_theory=lra,
      )
      models = solver._find_model()
  
      if all_models:
          return _all_models(models)
  
      try:
          return next(models)
      except StopIteration:
          return False
  
imports: from collections import defaultdict
  from heapq import heappush, heappop
  from sympy.core.sorting import ordered
  from sympy.assumptions.cnf import EncodedCNF
  from sympy.logic.algorithms.lra_theory import LRASolver
label_desc: Use image node_id 1 for calling a global function with example usage: dpll_satisfiable(expr, all_models, use_lra_theory) and returns: False, _all_models, next, unknown, False