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 }

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)

(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

## 3 comments:

Thank you.

Very helpful thank you. I implemented the algorithm in C. Used it in a project: propositional theorem proving.

Thanks!Your method is so elegant.

Post a Comment