def unit_clause_assign(clause, model):
P, value = None, None<EOL>for literal in disjuncts(clause):<EOL><INDENT>sym, positive = inspect_literal(literal)<EOL>if sym in model:<EOL><INDENT>if model[sym] == positive:<EOL><INDENT>return None, None  <EOL><DEDENT><DEDENT>elif P:<EOL><INDENT>return None, None      <EOL><DEDENT>else:<EOL><INDENT>P, value = sym, positive<EOL><DEDENT><DEDENT>return P, value<EOL>
Return a single variable/value pair that makes clause true in
    the model, if possible.
    >>> unit_clause_assign(A|B|C, {A:True})
    (None, None)
    >>> unit_clause_assign(B|~C, {A:True})
    (None, None)
    >>> unit_clause_assign(~A|~B, {A:True})
    (B, False)