Bool Expression is widely used in search engine, automatic thoery proving and database query evaluation etc. In these situations, you need to convert the bool expression into some normal form so that two expression can be compared to test equality, can be implemented using existing operators or can be used to optimize the query evaluation. CNF is such kind of normal form.

In Conjunctive Normal Form(CNF), every sentence is expressed as a conjunction of clauses (where a clause is a disjunction of literals)

The conversion algorithm is simple and straight forward[1]:
1. Drive In Negation (Move Negation Inwards)
- Double-Negation Elimination
- De Morgan
2. Distributed ORs over ANDs
3. Clause Collection
- Remove always true clauses

The implementation:
1. Define a BoolExpr class to represent bool expression. Composite pattern is used since bool expression is a tree like data structure.
2. Use recursive method: DriveInNegation() to implement step 1 in conversion algorithm.
3. Recursive method ToCNF()is used to implement step 2 in conversion algorithm. It first convert each children into CNF, then recognize several cases and deal each case individually:
- if root op is AND, it’s done.
- if root op is OR, both left and right op are OR, it’s done.
- if root op is OR, left is AND but right is OR, it is converted using the rule: (A ∧ B) ∨ C ∨ D <=> (A ∨ C ∨ D) ∧ (B ∨ C ∨ D)
- if root op is OR, left is OR but right is AND, it’s similar to upper case
- if root op is OR, both left and righ op are AND, it’s converted using the rule: (A ∧ B) ∨ (C ∧ D) <=> (A ∨ C) ∧ (B ∨ C) ∧ (A ∨ D) ∧ (B ∨ D)
4. RemoveDeadClause() is used to implement step 3 in the algorithm. It uses a static map to detect paried literals(for example: Q/Q)

conversion logic code
 1 public BoolExpr ToCNF()
 2 {
 3     if (IsLeaf())
 4     // A
 5     {
 6         return new BoolExpr(this);
 7     }
 8
 9     if (_op == BOP.NOT)
10     {
11         if (_left.IsLeaf())
12         // ┐A
13         {
14             return new BoolExpr(this);
15         }
16         else
17         // ┐(…)
18         {
19             BoolExpr expr = _left.DriveInNegation();
20             return expr.ToCNF();
21         }
22     }
23
24     // convert children first
25     BoolExpr cnfLeft = null, cnfRight = null;
26     if (_left  != null) { cnfLeft  = _left.ToCNF(); }
27     if (_right != null) { cnfRight = _right.ToCNF(); }
28
29     if (_op == BOP.AND)
30     //   *
31     // ?   ?
32     { return new BoolExpr(_op, cnfLeft, cnfRight); }
33
34     if (_op == BOP.OR)
35     {
36         if (( cnfLeft == null || cnfLeft.IsAtomic() || cnfLeft.Op == BOP.OR)
37             && (cnfRight == null || cnfRight.IsAtomic() || cnfRight.Op == BOP.OR))
38         //   +
39         // +   +
40         {
41             return new BoolExpr(BOP.OR, cnfLeft, cnfRight);
42         }
43         else if ((cnfLeft != null && cnfLeft.Op == BOP.AND)
44                 && (cnfRight == null || cnfRight.IsAtomic() || cnfRight.Op == BOP.OR))
45         //   +
46         // *   +
47         {
48             BoolExpr newLeft = new BoolExpr(BOP.OR, cnfLeft.Left, cnfRight);
49             BoolExpr newRight = new BoolExpr(BOP.OR, cnfLeft.Right, cnfRight);
50
51             return new BoolExpr(BOP.AND, newLeft.ToCNF(), newRight.ToCNF());
52         }
53         else if ((cnfRight != null && cnfRight.Op == BOP.AND)
54                 && (cnfLeft == null || cnfLeft.IsAtomic() || cnfLeft.Op == BOP.OR))
55         //   +
56         // +   *
57         {
58             BoolExpr newLeft = new BoolExpr(BOP.OR, cnfLeft, cnfRight.Right);
59             BoolExpr newRight = new BoolExpr(BOP.OR, cnfLeft, cnfRight.Left);
60
61             return new BoolExpr(BOP.AND, newLeft.ToCNF(), newRight.ToCNF());
62         }
63         else if ((cnfLeft != null && cnfLeft.Op == BOP.AND)
64                 && (cnfRight != null && cnfRight.Op == BOP.AND))
65         //   +
66         // *   *
67         {
68             BoolExpr newLeft = new BoolExpr(BOP.AND,
69                 new BoolExpr(BOP.OR, cnfLeft.Left, cnfRight.Left),
70                 new BoolExpr(BOP.OR, cnfLeft.Right, cnfRight.Left));
71
72             BoolExpr newRight = new BoolExpr(BOP.AND,
73                 new BoolExpr(BOP.OR, cnfLeft.Left, cnfRight.Right),
74                 new BoolExpr(BOP.OR, cnfLeft.Right, cnfRight.Right));
75
76             return new BoolExpr(BOP.AND, newLeft.ToCNF(), newRight.ToCNF());
77         }
78     }
79
80     // error status, should NOT reach here
81     System.Console.Out.WriteLine("Error Status");
82     return null;
83 }

console test output
(A ∧ B) ∨ (C ∧ D) => (A ∨ C) ∧ (B ∨ C) ∧ (A ∨ D) ∧ (B ∨ D)
(A ∧ B) ∨ C ∨ D => (A ∨ C ∨ D) ∧ (B ∨ C ∨ D)
¬((A ∧ B) ∨ C ∨ D) => (¬A ∨ ¬B) ∧ ¬C ∧ ¬D
¬¬¬¬¬¬A => A
¬¬¬¬¬A => ¬A
(P ∧ Q) ∨ (¬P ∧ R) ∨ (¬Q ∧ ¬R) => (P ∨ R ∨ ¬Q) ∧ (Q ∨ ¬P ∨ ¬R)

TODO:
1. Eliminate true clauses
2. Reorder literals

source code

Update@5/14/2009
- Always True Clauses are removed in the final result

[Reference]
[1] Artificial Intelligence, a modern approach [2E]
[2] code for algorithms in [1]
[3] course lecture on cnf conversion
[4] cnf conversion in scheme

 

One Response to convert Arbitrary Bool Expression into Conjunctive Normal Form

  1. Anonymous says:

    Thank you.

Leave a Reply

Your email address will not be published. Required fields are marked *

* Copy This Password *

* Type Or Paste Password Here *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

Set your Twitter account name in your settings to use the TwitterBar Section.