code: def minisat22_satisfiable(expr, all_models=False, minimal=False):
      if not isinstance(expr, EncodedCNF):
          exprs = EncodedCNF()
          exprs.add_prop(expr)
          expr = exprs
  
      from pysat.solvers import Minisat22
  
      # 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
  
      r = Minisat22(expr.data)
  
      if minimal:
          r.set_phases([-(i + 1) for i in range(r.nof_vars())])
  
      if not r.solve():
          return False
  
      if not all_models:
          return {
              expr.symbols[abs(lit) - 1]: lit > 0
              for lit in r.get_model()
          }
  
      else:
          # Make solutions SymPy compatible by creating a generator
          def _gen(results):
              satisfiable = False
              while results.solve():
                  sol = results.get_model()
                  yield {
                      expr.symbols[abs(lit) - 1]: lit > 0 for lit in sol
                  }
                  if minimal:
                      results.add_clause([-i for i in sol if i > 0])
                  else:
                      results.add_clause([-i for i in sol])
                  satisfiable = True
              if not satisfiable:
                  yield False
              raise StopIteration
  
          return _gen(r)
  
label_desc: Use image node_id 1 for calling a global function with example usage: minisat22_satisfiable(expr, all_models, minimal) and returns: False, False, unknown, _gen, unknown