Talk:Conjunctive normal form

Not a method

Bah. Conjunctive normal form is not a method. There is a method to construct a conjunctive normal form of a logical function, but the CNF, the result of this method is not the method. A method is not the same as the result of this. Be exact, please :-)) (a mathematician). Gubbubu 20:44, 28 May 2005 (UTC)

4-SAT

If 4-SAT is defined like 3-SAT (all clauses have at most 4 literals), the problem is NP-complete, like any other k-SAT problem with k>2. The recent edit stating that 4-SAT is linear is incorrect unless a different definition of 4-SAT is considered. Source? - Liberatore(T) 15:25, 16 December 2005 (UTC)

Inquiry

Regarding the following line:

Transformations of formulae in CNF form preserving satisfiability (rather than equivalence) and introducing new variables exist. These transformations are interesting because they are guaranteed not to produce an exponential blow-up.

I am curious as to the source of this statement. I am particularly interested in reading what these transformations are specifically. --Stux 06:48, 2 January 2006 (UTC)

See for example

Daniel Sheridan. The Optimality of a Fast CNF Conversion and its Use with SAT.SAT 2004

These transformations are based on creating new variables that represent the truth value of a subformula (should the fact that new variables are necessary be mentioned in the article?). For example, $(a\wedge b)\vee c$ can be transformed into $(new\vee c)\wedge (\neg new\vee a)\wedge (\neg new\vee b)$, where $new$ is a new variable. - Liberatore(T) 13:50, 2 January 2006 (UTC)