def find_unit_clause(clauses, model):
    for clause in clauses:
        num_not_in_model = 0
        for literal in disjuncts(clause):
            sym = literal_symbol(literal)
            if sym not in model:
                num_not_in_model += 1
                P, value = sym, not (literal.func is Not)
        if num_not_in_model == 1:
            return P, value
    return None, None
A unit clause has only 1 variable that is not bound in the model.
dataset/ETHPy150Open sympy/sympy/sympy/logic/algorithms/dpll.py/find_unit_clause