Talk:Conjunctive normal form
From Wikipedia, the free encyclopedia
Contents |
[edit] 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)
[edit] 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)
[edit] 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,
can be transformed into 
, where new is a new variable. - Liberatore(T) 13:50, 2 January 2006 (UTC)
[edit] incomplete definition?
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)
- 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)
