A Hall-type theorem with algorithmic consequences in planar graphs