Boolean Function Manipulation on Massively Parallel Computers