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:
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:
- 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
- p –> q = ¬p \/ q
- 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
- (¬p \/ q) –> r = ¬(¬p \/ q) \/ r
- 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
- (¬¬p /\ ¬q) \/ r = (p /\ ¬q) \/ r
- Finally we use the expansion rule next:
- (p /\ ¬q) \/ r = (p \/ r) /\ (¬q \/ r)
And there we go :D , 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)
No comments:
Post a Comment