Towards Optimal Branching of Linear and Semidefinite Relaxations for Neural Network Robustness Certification