code: def pycosat_satisfiable(expr, all_models=False):
      import pycosat
  
      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 not all_models:
          r = pycosat.solve(expr.data)
          result = r != "UNSAT"
          if not result:
              return result
          return {expr.symbols[abs(lit) - 1]: lit > 0 for lit in r}
      else:
          r = pycosat.itersolve(expr.data)
          result = r != "UNSAT"
          if not result:
              return result
  
          # Make solutions SymPy compatible by creating a generator
          def _gen(results):
              satisfiable = False
              try:
                  while True:
                      sol = next(results)
                      yield {
                          expr.symbols[abs(lit) - 1]: lit > 0
                          for lit in sol
                      }
                      satisfiable = True
              except StopIteration:
                  if not satisfiable:
                      yield False
  
          return _gen(r)
  
label_desc: Use image node_id 1 for calling a global function with example usage: pycosat_satisfiable(expr, all_models) and returns: False, unknown, _gen, unknown, result, result