def _unit_prop(self):
        result = len(self._unit_prop_queue) > 0
        while self._unit_prop_queue:
            next_lit = self._unit_prop_queue.pop()
            if -next_lit in self.var_settings:
                self.is_unsatisfied = True
                self._unit_prop_queue = []
                return False
            else:
                self._assign_literal(next_lit)

        return result
Perform unit propagation on the current theory.
dataset/ETHPy150Open sympy/sympy/sympy/logic/algorithms/dpll2.py/SATSolver._unit_prop