def unit_propagate(clauses, cascade=True):
	"""Divide a collection of clauses into a set of satisfied literals and a
	new collection of clauses with satisfied literals removed.

	Args:
		clauses (:obj:`iter` of :obj:`iter` of :obj:`int`): A collection of clauses.
		cascade (:obj:`bool`, optional): Whether to recursively apply ``unit_propagate``.
			Defaults to `True`.

	Returns:
		:obj:`tuple` - The first element is a :obj:`set` of :obj:`int` containing
			satisfied literals. The second element is a collection of clauses with
			all satisfied literals removed.
	"""

	cnf_1, cnf_n = set(), set()
	cnf_other = list()

	for clause in clauses:
		if len(clause) == 1:
			cnf_1.add(list(clause)[0])
		else:
			cnf_other.append(clause)

	if not cnf_1:
		return cnf_1, cnf_other

	for clause in cnf_other:
		clause = set(clause)
		for literal in list(clause):
			# Remove clauses containing True literals
			if literal in cnf_1:
				break
			# Remove false literals from clauses
			if -literal in cnf_1:
				clause.remove(literal)
		else:
			cnf_n.add(frozenset(clause))

	if cascade:
		cnf_1_next, cnf_n = unit_propagate(cnf_n)
		cnf_1.update(cnf_1_next)

	return cnf_1, cnf_n