Maths / Logic and Modelling – CNF


This is going to be the first post I’m going to write that is valid for BOTH year 1 and year 2. Just in case you get confused as to who should be reading it 😉

CNF is short for Conjunctive Normal Form. A formula is in CNF if it is True (T) or False ( _|_ ) or a conjunction of disjunctions:

conofdis

Such as:

  • T or _|_
  • (q \/ p) /\ p
  • (q \/ p) /\ (r \/ q)

Rewrite Rules

In order to convert a formula to CNF, one much rewrite the formulas sub-formulas. For example, using these rewrite rules:

  • A <-> B       =       (¬A \/ B) /\ (¬B \/ A)
  • A –> B        =       ¬A \/ B
  • ¬(A \/ B)      =       ¬A /\ ¬B
  • ¬(A /\ B)      =       ¬A \/ ¬B
  • ¬¬A             =        A
  • (A /\ B) \/ C  =       (A \/ C) /\ (B \/ C)

Now, have you noticed? None of the rewrites contain either “<->” or “->”, this is because a CNF formula must contain NO “<->” or “->” 😉

 

Example

Lets now consider a quick example. Consider the following formula:

  • ((p –> q) –> r)

Now lets go through the steps to transform it:

  1. Using the priorities, the first part to rewrite is “p –> q” so we get:
    • p –> q  =   ¬p \/ q

      Now we have the formula (¬p \/ q) –> r

  2. Next we have to rewrite the whole of the formula using the implication rewrite rule so we get:
    • (¬p \/ q) –> r    =    ¬(¬p \/ q) \/ r

      now we have to simplify this:

    • ¬(¬p \/ q) \/ r    =    (¬¬p /\ ¬q) \/ r
  3. As you can  now see we have a double negation on ‘¬¬p’, so we use the rule above so that we have:
    • (¬¬p /\ ¬q) \/ r    =    (p /\ ¬q) \/ r
  4. Finally we use the expansion rule next:
    • (p /\ ¬q) \/ r    =    (p \/ r) /\ (¬q \/ r)

And there we go 😀 , the CNF form of the formula ((p –> q) –> r) is (p \/ r) /\ (¬q \/ r)

Clauses – Year 2 Only

As a quick note – and this is only for second years… When using the DPLL algorithm we a CNF’ed formula we need to use the clauses to check satisfiability. The clauses from the CNF formula above are:

  • (p \/ r)
  • (¬q \/ r)
Advertisements

About Badgerati
Computer Scientist, Games Developer, and DevOps Engineer. Fantasy and Sci-fi book lover, also founder of Cadaeic Studios.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: