Whats the role of pricipal disjunctive normal form from discrete maths?

I think the main use of it is to make it easier for a computer to prove it. Automated Theorem Proving, it's called. Basically, throwing it in that form means you can verify various theorems by a computer.