code: def _backtrack(ex):
      
      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
docs: If this function is satisfiable, return a satisfying input upoint.
      Otherwise, return None.