This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects:

Mathematics Low‑priority This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles Low This article has been rated as Low-priority on the project's priority scale.

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)Reply[reply]

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)Reply[reply]

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)Reply[reply]

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, ${\displaystyle (a\wedge b)\vee c}$ can be transformed into ${\displaystyle (new\vee c)\wedge (\neg new\vee a)\wedge (\neg new\vee b)}$, where ${\displaystyle new}$ is a new variable. - Liberatore(T) 13:50, 2 January 2006 (UTC)Reply[reply]

I have been studying boolean algebra in my class "Fundamentals of Logic Design", and we are taught that CNF is more than just product of sums. We are taught that every sum (clause) must contain every literal. *This* is what makes the form useful for comparing functions and performing automatic analysis. Please comment, i'm interested to know how this is formally defined and used. Fresheneesz 21:05, 6 February 2006 (UTC)Reply[reply]

A formula in CNF is a conjunction of clauses. There is in general no obligation for a clause to contain all variables, which is a special case. Can you provide a source for the statement that every clause must contain all variables? Clearly, in some cases this is necessary, but is not part of the definition of CNF. - Liberatore(T) 21:21, 6 February 2006 (UTC)Reply[reply]

In circuit design it seems common to use a different definition than the one used in logic: Canonical_form_(Boolean_algebra). I'm no expert though. However, somebody should mention this fact on this page. --Blaisorblade (talk) 20:23, 29 January 2011 (UTC)Reply[reply]

I'm not quite sure, but in my Logic class I've been told that ${\displaystyle A\wedge B}$ is actually in DNF, and not CNF, because it is a single literal (i.e. equivalent to ${\displaystyle (A\wedge B)\vee (True\wedge True)}$). Can someone provide a counterexample if this is false or change the page if not? Poromenos (talk) 11:36, 13 February 2008 (UTC)Reply[reply]

${\displaystyle A\wedge B}$ is, in the definitions I am used to, both in CNF and DNF. It is in CNF because it is the conjunction of two disjunctions of literals (the disjunctions being 'A' and 'B'). It is in DNF because it is the disjunction of a conjunction of literals (there is only one disjunct, and it is ${\displaystyle A\land B}$).

An illuminating question to ask in your logic class would be - if ${\displaystyle A\land B}$ is not in CNF, then what is its conjunctive normal form? — Carl (CBM · talk) 12:53, 13 February 2008 (UTC)Reply[reply]

I have also reverted the change from -(A v B) to -(A & B); IMO, since A v B is more obvious to be in CNF than A&B (even if the second still is), then it's clear that the negation (rather than the binary connective) is the problem there. I have also added an explanation for A&B to be in CNF since this might not be obvious at first sight. Tizio 12:58, 14 February 2008 (UTC)Reply[reply]

Shouldn't it be "distribute ORs over ANDs"? Where i am interpreting "distribute ANDs over ORs" to mean the act of converting things like "A AND (B OR C)" into things like "(A AND B) OR (A AND C)". Bayle Shanks (talk) 10:23, 24 January 2010 (UTC)Reply[reply]

It appears that a step is missing. While converting, the second step should be to move ¬ inward. —Preceding unsigned comment added by Loki411 (talk • contribs) 07:31, 10 November 2010 (UTC)Reply[reply]

I don't believe this should be merged. Olleicua (talk) 16:48, 29 September 2011 (UTC)Reply[reply]

I think it can be merged, over various internet sources both are treated same.. AshutoshJuve (talk) 17:01, 6 December 2011 (UTC)Reply[reply]

Conjunctive normal form and clausal normal form are indeed the same thing. See, for example, Melvin Fitting, First order logic and automated theorem proving, second edition, page 28. Thus I vote to merge 82.24.239.152 (talk) 19:56, 28 December 2012 (UTC)Reply[reply]

Regarding the word "redices" -- is that a word? --LilHelpa (talk) 13:47, 16 May 2017 (UTC)Reply[reply]

The method of converting a formula into a CNF is not introduced. Wxhtxdy (talk) 16:05, 9 March 2019 (UTC)Reply[reply]

Shouldn't the complexity of converting a formula into CNF, preserving validity, be coNP-hard? Because the validity problem for a DNF is coNP-hard and it can be decided by converting the DNF into CNF (the validity of a CNF can be decided in linear time)? 94.103.211.82 (talk) 18:07, 19 January 2024 (UTC)Reply[reply]