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)

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 .