def propagate(self, assumptions=[], phase_saving=0):
        """
            The method takes a list of assumption literals and does unit
            propagation of each of these literals consecutively. A Boolean
            status is returned followed by a list of assigned (assumed and also
            propagated) literals. The status is ``True`` if no conflict arised
            during propagation. Otherwise, the status is ``False``.
            Additionally, a user may specify an optional argument
            ``phase_saving`` (``0`` by default) to enable MiniSat-like phase
            saving.

            **Note** that only MiniSat-like solvers support this functionality
            (e.g. :class:`Lingeling` does not support it).

            :param assumptions: a list of assumption literals.
            :param phase_saving: enable phase saving (can be ``0``, ``1``, and
                ``2``).

            :type assumptions: iterable(int)
            :type phase_saving: int

            :rtype: tuple(bool, list(int)).

            Usage example:

            .. code-block:: python

                >>> from pysat.solvers import Glucose3
                >>> from pysat.card import *
                >>>
                >>> cnf = CardEnc.atmost(lits=range(1, 6), bound=1, encoding=EncType.pairwise)
                >>> g = Glucose3(bootstrap_with=cnf.clauses)
                >>>
                >>> g.propagate(assumptions=[1])
                (True, [1, -2, -3, -4, -5])
                >>>
                >>> g.add_clause([2])
                >>> g.propagate(assumptions=[1])
                (False, [])
                >>>
                >>> g.delete()
        """

        if self.solver:
            return self.solver.propagate(assumptions, phase_saving)