<SYSTEM_TASK:>
Solve the following problem using Python, implementing the functions described below, one line at a time
<END_TASK>
<USER_TASK:>
Description:
 def _backtrack(ex):
 """ If this function is satisfiable, return a satisfying input upoint. Otherwise, return None. """

    if ex is Zero:
        return None
    elif ex is One:
        return dict()
    else:
        v = ex.top
        points = {v: 0}, {v: 1}
        for point in points:
            soln = _backtrack(ex.restrict(point))
            if soln is not None:
                soln.update(point)
                return soln
        return None