code: def satask(
      proposition,
      assumptions=True,
      context=global_assumptions,
      use_known_facts=True,
      iterations=oo,
  ):
      """
      Function to evaluate the proposition with assumptions using SAT algorithm.
  
      This function extracts every fact relevant to the expressions composing
      proposition and assumptions. For example, if a predicate containing
      ``Abs(x)`` is proposed, then ``Q.zero(Abs(x)) | Q.positive(Abs(x))``
      will be found and passed to SAT solver because ``Q.nonnegative`` is
      registered as a fact for ``Abs``.
  
      Proposition is evaluated to ``True`` or ``False`` if the truth value can be
      determined. If not, ``None`` is returned.
  
      Parameters
      ==========
  
      proposition : Any boolean expression.
          Proposition which will be evaluated to boolean value.
  
      assumptions : Any boolean expression, optional.
          Local assumptions to evaluate the *proposition*.
  
      context : AssumptionsContext, optional.
          Default assumptions to evaluate the *proposition*. By default,
          this is ``sympy.assumptions.global_assumptions`` variable.
  
      use_known_facts : bool, optional.
          If ``True``, facts from ``sympy.assumptions.ask_generated``
          module are passed to SAT solver as well.
  
      iterations : int, optional.
          Number of times that relevant facts are recursively extracted.
          Default is infinite times until no new fact is found.
  
      Returns
      =======
  
      ``True``, ``False``, or ``None``
  
      Examples
      ========
  
      >>> from sympy import Abs, Q
      >>> from sympy.assumptions.satask import satask
      >>> from sympy.abc import x
      >>> satask(Q.zero(Abs(x)), Q.zero(x))
      True
  
      """
      props = CNF.from_prop(proposition)
      _props = CNF.from_prop(~proposition)
  
      assumptions = CNF.from_prop(assumptions)
  
      context_cnf = CNF()
      if context:
          context_cnf = context_cnf.extend(context)
  
      sat = get_all_relevant_facts(
          props,
          assumptions,
          context_cnf,
          use_known_facts=use_known_facts,
          iterations=iterations,
      )
      sat.add_from_cnf(assumptions)
      if context:
          sat.add_from_cnf(context_cnf)
  
      return check_satisfiability(props, _props, sat)
  
file_path: sympy/sympy/assumptions/satask.py
imports: from sympy.core.singleton import S
  from sympy.core.symbol import Symbol
  from sympy.core.kind import NumberKind, UndefinedKind
  from sympy.assumptions.ask_generated import get_all_known_matrix_facts, get_all_known_number_facts
  from sympy.assumptions.assume import global_assumptions, AppliedPredicate
  from sympy.assumptions.sathandlers import class_fact_registry
  from sympy.core import oo
  from sympy.logic.inference import satisfiable
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.matrices.kind import MatrixKind
label_desc: Use image node_id 1 for calling a global function with example usage: satask(proposition, assumptions, context, use_known_facts, iterations) and returns: check_satisfiability