I'm currently learning about conjunctive normal form in a course on logic for Computer Science. I was reading the Wikipedia entry on the subject and encountered this:
Typical problems in this case involve formulas in "3CNF": conjunctive normal form with no more than three variables per conjunct. Examples of such formulas encountered in practice can be very large, for example with 100,000 variables and 1,000,000 conjuncts.
There is no source for this, and I'm curious as to the "practice" that's being referred to here. What kind of problems lead to these large sets of conjuncts; and can anyone point me to some examples?