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?

Many thanks.

  • 1
    $\begingroup$ This is not a complete answer, but rather a hint, so a comment it is. Many problems can be expressed as SAT fairly directly, but doing so often requires to create many variables. For example, for solving Sudoku you can create variables "square 1,1 has value 1", "square 1,1 has value 2", etc. This already immediately gives 729 variables for Sudoku, which is a 9x9 problem. A 50 by 50 Sudoku would already result in 125000 variables. This "booleanization" of your problem often explodes the number of variables. Then translating from this to 3SAT often explodes the number of clauses as well. $\endgroup$
    – orlp
    Mar 31 '20 at 22:05
  • $\begingroup$ Most studies on 3-CNF formulas focus mainly on random generated ones and hence not derived from real world problems. But note that any CNF formula can be translated to a 3-CNF formula while preserving the satisfiability. Hence any practical problem that can be reduced to SAT can be reduced to a 3-CNF formula as well. of course the size of the resulting 3-CNF formula get increased. $\endgroup$
    – RTK
    Apr 4 '20 at 15:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.