Parallel disk-based computation for large, monolithic binary decision diagrams