The ordered binary decision diagram (OBDD) is a data structure used for representing Boolean functions, which are often utilized for formal circuit verification. The author analyzes what he calls the shared parity OBDD. He presents an involved algorithm to minimize the number of nodes in a parity OBDD in polynomial time. Moreover, he proves that the problems of satisfiability, synthesis, equivalence, replacement by constants, and replacement by functions for such OBDDs can also be solved in polynomial time.