Jump to content
 







Main menu
   


Navigation  



Main page
Contents
Current events
Random article
About Wikipedia
Contact us
Donate
 




Contribute  



Help
Learn to edit
Community portal
Recent changes
Upload file
 








Search  

































Create account

Log in
 









Create account
 Log in
 




Pages for logged out editors learn more  



Contributions
Talk
 



















Contents

   



(Top)
 


1 Definition  





2 Conversion to CNF  



2.1  Basic algorithm  



2.1.1  Conversion by syntactic means  





2.1.2  Conversion by semantic means  







2.2  Other approaches  







3 Maximum number of disjunctions  





4 Computational complexity  





5 First-order logic  



5.1  Converting from first-order logic  







6 See also  



6.1  Notes  







7 References  





8 External links  














Conjunctive normal form






Català
Čeština
Deutsch
Español
فارسی
Français

Հայերեն
Italiano
עברית
Magyar
Nederlands

Polski
Português
Русский
Српски / srpski
Srpskohrvatski / српскохрватски
Українська


 

Edit links
 









Article
Talk
 

















Read
Edit
View history
 








Tools
   


Actions  



Read
Edit
View history
 




General  



What links here
Related changes
Upload file
Special pages
Permanent link
Page information
Cite this page
Get shortened URL
Download QR code
Wikidata item
 




Print/export  



Download as PDF
Printable version
 
















Appearance
   

 






From Wikipedia, the free encyclopedia
 


InBoolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunctionofliterals; otherwise put, it is a product of sumsoran AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

In automated theorem proving, the notion "clausal normal form" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.

Definition[edit]

A logical formula is considered to be in CNF if it is a conjunction of one or more disjunctions of one or more literals. As in disjunctive normal form (DNF), the only propositional operators in CNF are or (), and (), and not (). The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

The following is a context-free grammar for CNF:

  1. CNF → (Disjunction) CNF
  2. CNF → (Disjunction)
  3. DisjunctionLiteral Disjunction
  4. DisjunctionLiteral
  5. LiteralVariable
  6. LiteralVariable

Where Variable is any variable.

All of the following formulas in the variables , and are in conjunctive normal form:

The following formulas are not in conjunctive normal form:

Conversion to CNF[edit]

Inclassical logic each propositional formula can be converted to an equivalent formula that is in CNF.[1] This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.

Basic algorithm[edit]

The algorithm to compute a CNF-equivalent of a given propositional formula builds upon indisjunctive normal form (DNF): step 1.[2]
Then is converted to by swapping ANDs with ORs and vice versa while negating all the literals. Remove all .[1]

Conversion by syntactic means[edit]

Convert to CNF the propositional formula .

Step 1: Convert its negation to disjunctive normal form.[2]

,[a]

where each is a conjunction of literals .[b]

Step 2: Negate . Then shift inwards by applying the (generalized) De Morgan's equivalences until no longer possible. where

Step 3: Remove all double negations.

Example

Convert to CNF the propositional formula .[c]

The (full) DNF equivalent of its negation is[2]

Conversion by semantic means[edit]

A CNF equivalent of a formula can be derived from its truth table. Again, consider the formula .[c]

The corresponding truth tableis

T T T F T F F T F
T T F F T F T T F
T F T T F T F T T
T F F T F F T F T
F T T T F T F T T
F T F T F F T F T
F F T T F T F T F
F F F T F T T T F

A CNF equivalent of is

Each disjunction reflects an assignment of variables for which evaluates to F(alse).
If in such an assignment a variable

Other approaches[edit]

Since all propositional formulas can be converted into an equivalent formula in conjunctive normal form, proofs are often based on the assumption that all formulae are CNF. However, in some cases this conversion to CNF can lead to an exponential explosion of the formula. For example, translating the non-CNF formula

into CNF produces a formula with clauses:

Each clause contains either or for each .

There exist transformations into CNF that avoid an exponential increase in size by preserving satisfiability rather than equivalence.[3][4] These transformations are guaranteed to only linearly increase the size of the formula, but introduce new variables. For example, the above formula can be transformed into CNF by adding variables as follows:

Aninterpretation satisfies this formula only if at least one of the new variables is true. If this variable is , then both and are true as well. This means that every model that satisfies this formula also satisfies the original one. On the other hand, only some of the models of the original formula satisfy this one: since the are not mentioned in the original formula, their values are irrelevant to satisfaction of it, which is not the case in the last formula. This means that the original formula and the result of the translation are equisatisfiable but not equivalent.

An alternative translation, the Tseitin transformation, includes also the clauses . With these clauses, the formula implies ; this formula is often regarded to "define" to be a name for .

Maximum number of disjunctions[edit]

Consider a propositional formula with variables, .

There are possible literals: .

has non-empty subsets.[d]

This is the maximum number of disjunctions a CNF can have.[e]

All truth-functional combinations can be expressed with disjunctions, one for each row of the truth table.
In the example below they are underlined.

Example

Consider a formula with two variables and .

The longest possible CNF has disjunctions:[e]

This formula is a contradiction.

Computational complexity[edit]

An important set of problems in computational complexity involves finding assignments to the variables of a boolean formula expressed in conjunctive normal form, such that the formula is true. The k-SAT problem is the problem of finding a satisfying assignment to a boolean formula expressed in CNF in which each disjunction contains at most k variables. 3-SATisNP-complete (like any other k-SAT problem with k>2) while 2-SAT is known to have solutions in polynomial time. As a consequence,[f] the task of converting a formula into a DNF, preserving satisfiability, is NP-hard; dually, converting into CNF, preserving validity, is also NP-hard; hence equivalence-preserving conversion into DNF or CNF is again NP-hard.

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.

A formula in CNF can be converted into an equisatisfiable formula in "kCNF" (for k≥3) by replacing each conjunct with more than k variables by two conjuncts and with Z a new variable, and repeating as often as necessary.

First-order logic[edit]

In first order logic, conjunctive normal form can be taken further to yield the clausal normal form of a logical formula, which can be then used to perform first-order resolution. In resolution-based automated theorem-proving, a CNF formula

,[g] is commonly represented as a set of sets
.

See below for an example.

Converting from first-order logic[edit]

To convert first-order logic to CNF:[5]

  1. Convert to negation normal form.
    1. Eliminate implications and equivalences: repeatedly replace with ; replace with . Eventually, this will eliminate all occurrences of and .
    2. Move NOTs inwards by repeatedly applying De Morgan's law. Specifically, replace with ; replace with ; and replace with ; replace with ; with . After that, a may occur only immediately before a predicate symbol.
  2. Standardize variables
    1. For sentences like which use the same variable name twice, change the name of one of the variables. This avoids confusion later when dropping quantifiers. For example, is renamed to .
  3. Skolemize the statement
    1. Move quantifiers outwards: repeatedly replace with ; replace with ; replace with ; replace with . These replacements preserve equivalence, since the previous variable standardization step ensured that doesn't occur in . After these replacements, a quantifier may occur only in the initial prefix of the formula, but never inside a , , or .
    2. Repeatedly replace with , where is a new -ary function symbol, a so-called "Skolem function". This is the only step that preserves only satisfiability rather than equivalence. It eliminates all existential quantifiers.
  4. Drop all universal quantifiers.
  5. Distribute ORs inwards over ANDs: repeatedly replace with .

Example

As an example, the formula saying "Anyone who loves all animals, is in turn loved by someone" is converted into CNF (and subsequently into clause form in the last line) as follows (highlighting replacement rule redexesin):

by 1.1
by 1.1
by 1.2
by 1.2
by 1.2
by 2
by 3.1
by 3.1
by 3.2
by 4
by 5
(clause representation)

Informally, the Skolem function can be thought of as yielding the person by whom is loved, while yields the animal (if any) that doesn't love. The 3rd last line from below then reads as " doesn't love the animal , or else is loved by ".

The 2nd last line from above, , is the CNF.

See also[edit]

Notes[edit]

  1. ^ maximum number of conjunctions for
  • ^ maximum number of literals for
  • ^ a b = ((NOT (pANDq)) IFF ((NOTr) NAND (pXORq)))
  • ^
  • ^ a b It is assumed that repetitions and variations (like ) based on the commutativity and associativityof and do not occur.
  • ^ since one way to check a CNF for satisfiability is to convert it into a DNF, the satisfiability of which can be checked in linear time
  • ^ maximum number of disjunctions
    maximum number of literals
  • References[edit]

  • ^ Tseitin 1968.
  • ^ Jackson & Sheridan 2004.
  • ^ Russel & Norvig 2010, pp. 345–347, 9.5.1 Conjunctive normal form for first-order logic.
    • Andrews, Peter B. (2013). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. ISBN 9401599343.
  • Howson, Colin (11 October 2005) [1997]. Logic with trees: an introduction to symbolic logic. Routledge. ISBN 978-1-134-78550-6.
  • Jackson, Paul; Sheridan, Daniel (10 May 2004). "Clause Form Conversions for Boolean Circuits" (PDF). In Hoos, Holger H.; Mitchell, David G. (eds.). Theory and Applications of Satisfiability Testing,. 7th International Conference on Theory and Applications of Satisfiability Testing, SAT. Revised Selected Papers. Lecture Notes in Computer Science. Vol. 3542. Vancouver, BC, Canada: Springer 2005. pp. 183–198. doi:10.1007/11527695_15. ISBN 978-3-540-31580-3.
  • Kleine Büning, Hans; Lettmann, Theodor (28 August 1999). Propositional Logic: Deduction and Algorithms. Cambridge University Press. ISBN 978-0-521-63017-7.
  • Russel, Stuart; Norvig, Peter, eds. (2010) [1995]. Artificial Intelligence : A Modern Approach (PDF) (3rd ed.). Upper Saddle River, NJ: Prentice Hall. ISBN 978-0-13-604259-4. Archived (PDF) from the original on 31 August 2017.
  • Tseitin, Grigori S. (1968). "On the Complexity of Derivation in Propositional Calculus" (PDF). In Slisenko, A.O. (ed.). Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian). Steklov Mathematical Institute. pp. 115–125.
  • Whitesitt, J. Eldon (24 May 2012) [1961]. Boolean Algebra and Its Applications. Courier Corporation. ISBN 978-0-486-15816-7.
  • External links[edit]


    Retrieved from "https://en.wikipedia.org/w/index.php?title=Conjunctive_normal_form&oldid=1228380816"

    Categories: 
    Normal forms (logic)
    Knowledge compilation
    Hidden categories: 
    Articles with short description
    Short description is different from Wikidata
    Pages that use a deprecated format of the math tags
     



    This page was last edited on 10 June 2024, at 22:52 (UTC).

    Text is available under the Creative Commons Attribution-ShareAlike License 4.0; additional terms may apply. By using this site, you agree to the Terms of Use and Privacy Policy. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc., a non-profit organization.



    Privacy policy

    About Wikipedia

    Disclaimers

    Contact Wikipedia

    Code of Conduct

    Developers

    Statistics

    Cookie statement

    Mobile view



    Wikimedia Foundation
    Powered by MediaWiki