Review for NeurIPS paper: Efficient Exact Verification of Binarized Neural Networks

The paper was assessed as a high quality work by most of the reviewers, contributing fast methods for robustness verification of binary neural networks and training robust binary networks. The points of strong criticism were positioning of the contribution wrt to the constraint programming methods. Since one of the main claimed contributions is the speed-up, it was questioned whether such a speed-up can be obtained by just existing methods / solvers. In particular, L168: "We present the first extension to handle the reified cardinality constraints" was criticized. The arguments of the discussion clarified that in modern pseudo-Boolean solvers the same (resp. Cardinality constraints and more generally linear inequality constraints can be handled natively.