.md .pdf

Contents

Simplification

We can write a program in Racket that will symbolically manipulate a Boolean expression. We will simplify an expression to CNF form.

Preliminaries

We need a few of the functions from our boolean evaluator to make the simplification program.

;Get the first operand of an expression
;input-contract: A valid expression
;output-contact: The first operand
(define (op1 exp)
  (second exp)
)
;Get the second operand of an expression
;input-contract: A valid expression
;output-contact: The second operand
(define (op2 exp)
  (third exp)
)

;Detect Expression Type
;Given an operator and list length
;creates a procedure to detect expressions of that format
;input-contract: (and (symbol? op) (integer? len))
;output-contract: (procedure? (isOperator op len))
(define (isOperator op len)
  (lambda (expr)
    (and
     (list? expr)
     (equal? (length expr) len)
     (equal? op (first expr))
    )
 )
)
;Define the formats we need
;Negation only takes 1 input
;Other Boolean Operators are 2 inputs and the operator
(define isNot? (isOperator '~ 2) )
(define isAnd? (isOperator '& 3) )
(define isOr?  (isOperator 'v 3) )
(define isImplies? (isOperator '-> 3))
(define isBicond? (isOperator '<-> 3))

Negative Normal Form

First, we need to convert the expression to NNF. This is a prerequisite of NNF.

NNF Rules

There were a number of simplification rules used for NNF. We implement a function for each of them.

We need to replace conditional statements with their definition.

\( \begin{align} (A \implies B) = (\neg A \vee B) \end{align} \)

;Rule 1: Definition of Implies
;(A->B) = (~A v B)
;input-contract: A valid implies expression
;output-contract: The expression rewritten as an or
(define (defOfImplies expr)
  (list 'v (list '~ (op1 expr)) (op2 expr))
)
(display "Def of Implies Example:\n")
(display (defOfImplies '(-> X Y)))(newline)
; Returns '(v (~ X) Y)

We also have a definition for the Bi-Conditional.

\( \begin{align} (A \iff B) = (A \implies B) \wedge (B \implies A) \end{align} \)

;Rule 2: Definition of Bi-Conditional
;(A <-> B) = (A->B) & (B->A)
;input-contract: A valid bi-conditional expression
;output-contract: The expression rewritten as an or+implies
(define (defOfBicond expr)
  (list '&
        (list '-> (op1 expr) (op2 expr))
        (list '-> (op2 expr) (op1 expr))
  )
)
(display "Def of Bi-Conditional Example:\n")
(display (defOfBicond '(<-> X Y)))(newline)
; Returns '(v (-> X Y) (-> Y X))

We also need to apply DeMorgan’s. This version works on a disjunction.

\( \begin{align} \neg(A \vee B) = (\neg A) \wedge (\neg B) \end{align} \)

;Rule 3: DeMorgan on Disjunction
;~(A v B) = (~A & ~B)
;input-contract: A valid boolean expression with negative applied to or
;output-contract: The expression rewritten using DeMorgan's Law
(define (deMorganDis expr)
  (list '&
        (list '~ (op1 (op1 expr)))
        (list '~ (op2 (op1 expr)))
  )
)
(display "DeMorgan on Disjunction Example:\n")
(display (deMorganDis '(~ (v X Y))))(newline)
; Returns '(& (~ X) (~ Y))

The DeMorgan’s Law version for conjunctions is also needed.

\( \begin{align} \neg(A \wedge B) = (\neg A) \vee (\neg B) \end{align} \)

;Rule 4: DeMorgan on Conjunction
;~(A & B) = (~A v ~B)
;input-contract: A valid boolean expression with negative applied to and
;output-contract: The expression rewritten using DeMorgan's Law
(define (deMorganConj expr)
  (list 'v
        (list '~ (op1 (op1 expr)))
        (list '~ (op2 (op1 expr)))
  )
)
(display "DeMorgan on Conjunction Example:\n")
(display (deMorganConj '(~ (& X Y))))(newline)
; Returns '(v (~ X) (~ Y))

The last rule we need is double negative elimination.

\( \begin{align} \neg \neg A = A \end{align} \)

;Rule 5: Double Negative Elimination
;~ ~ A = A
;input-contract: A valid boolean expression with a double negative
;output-contract: The expression with double negative removed
(define (doubleNeg expr)
  (op1 (op1 expr))
)
(display "Double Negative Elimination Example:\n")
(display (doubleNeg '(~ (~ (v A B)))))(newline)
; Returns '(v A B)

Is NNF?

To know when we should apply the rules, we need to know if the expression is in NNF form or not. We need to search the expression recursively. If we hit a point where a negation is above another operator, we know the expression is not in NNF.

;Determine if a Function is in NNF form or not
;input-contract: A valid boolean expression
;output-contract: #t if in NNF and #f otherwise
(define (isNNF? expr)
  (cond
    ;These operators are fine, but check operands
    [(or (isAnd? expr) (isOr? expr))
     (and (isNNF? (op1 expr)) (isNNF? (op2 expr)))]
    ;These operators are not allowed
    [(isImplies? expr) #f]
    [(isBicond? expr) #f]
    ;Not cannot be applied to operators
    [(isNot? expr) (not (list? (op1 expr)))]
    ;None of the above
    [else #t]
  )
)

Apply Rules

We have a number of rules. We need to determine which to apply when. This function tests an expression to see if any rules apply. If not, it searches recursively.

;Apply Rules of NNF
;Applies any rules it finds to the expression
;input-contract: A boolean expression
;output-contract: an equivalent boolean expression with rules applied
(define (simplifyNNF expr)
  (cond
    ;Operator Defs
    [(isImplies? expr) (defOfImplies expr)]
    [(isBicond? expr) (defOfBicond expr)]
    ;DeMorgan
    [(and (isNot? expr) (isOr? (op1 expr)))
     (deMorganDis expr)]
    [(and (isNot? expr) (isAnd? (op1 expr)))
     (deMorganConj expr)]
    ;Double Negative
    [(and (isNot? expr) (isNot? (op1 expr)))
     (doubleNeg expr)]
    ;Basic Operators
    [(isNot? expr) (list '~ (simplifyNNF (op1 expr)))]
    [(isAnd? expr) (list '& (simplifyNNF (op1 expr))
                         (simplifyNNF (op2 expr)))]
    [(isOr? expr) (list 'v (simplifyNNF (op1 expr))
                        (simplifyNNF (op2 expr)))]
    ;None of the above
    [else expr]
  )
)

Convert to NNF

To convert an expression to NNF, we just apply the rules repeatedly. If we apply them over and over again, eventually we will make it to NNF form.

;Convert to NNF
;Apply Rules until the expression is in NNF
;input-contract: a valid boolean expression
;output-contract: the same expression in NNF
(define (nnf expr)
  ;(display expr)(newline) ;Uncomment to see steps
  (if (isNNF? expr)
      expr
      (nnf (simplifyNNF expr))
  )
)

(display "Convert to NNF Examples:\n")
(display (nnf '(<-> A B)))(newline)
; Returns '(v (v (~ A) B) (v (~ B) A))
(display (nnf '(~ (<-> A B))))(newline)
; Returns '(& (& A (~ B)) (& B (~ A)))
(display (nnf '(~ (& (<-> A B) (-> (~ C) D)))))(newline)
; Returns '(v (v (& A (~ B)) (& B (~ A))) (& (~ C) (~ D)))
(display (nnf '(~ (& A (v B C)))))(newline)
; Returns (v ~A (& (~ B) (~ C)))

Conjunctive Normal Form

Once and expression is in NNF, we can apply one additional rule to convert it to CNF.

CNF Rules

We need to distribute disjunctions into conjunctions. We don’t need to worry about cases where both sides have a conjunction. That is just two applications of the rule. Notice that computers don’t understand rules can be flipped around the operator. We need to implement both versions.

\( \begin{align} (A \wedge B) \vee C =& (A \vee C) \wedge (B \vee C)\\ A \vee (B \wedge C) =& (A \vee B) \wedge (A \vee C) \end{align} \)

;Rule 1: Distribute Or
;(A & B) v C = (A v C) & (B v C)
;A v (B & C) = (A v B) & (A v C)
;input-contract: A boolean expression that needs to be
;                distributed
;output-contract: The expression after distribution
(define (distributeOr expr)
  (if (isAnd? (op1 expr))
      (list '&
            (list 'v (op1 (op1 expr))
                     (op2 expr))
            (list 'v (op2 (op1 expr))
                  (op2 expr))
      )
      (list '&
            (list 'v (op1 expr)
                     (op1 (op2 expr)))
            (list 'v (op1 expr)
                  (op2 (op2 expr)))
      )
 )
)
(display "Distribution Examples:\n")
(display (distributeOr '(v (& A B) C)))(newline)
; Returns '(& (v A C) (v B C))
(display (distributeOr '(v A (& B C))))(newline)
; Returns '(& (v A B) (v A C))

Is CNF?

We need to check if an expression is in CNF form. This way we know we can stop simplifying.

;Check if an expression is in CNF form
;input-contract: A valid boolean expression
;output-contract: #t if in CNF and #f otherwise
(define (isCNF? expr)
  (cond
    [(not (isNNF? expr)) #f]
    [(and (isOr? expr)
          (or (isAnd? (op1 expr)) (isAnd? (op2 expr))))
     #f]
    [(or (isAnd? expr) (isOr? expr))
     (and (isCNF? (op1 expr)) (isCNF? (op2 expr)))]
    [else #t]
  )

Apply CNF rules

This function checks to see if the CNF rules apply. If they do, it simplifies the expression.

;Apply Rules of CNF Form
;Applies any rules it finds once
;input-contract: a valid boolean expression
;output-contract: the expression simplified using rules
(define (simplifyCNF expr)
  (cond
    [(not (isNNF? expr)) (nnf expr)]
    [(and (isOr? expr)
          (or (isAnd? (op1 expr)) (isAnd? (op2 expr))))
     (distributeOr expr)]
    [(isAnd? expr) (list '&
           (simplifyCNF (op1 expr))
           (simplifyCNF (op2 expr)))]
    [(isOr? expr) (list 'v
           (simplifyCNF (op1 expr))
           (simplifyCNF (op2 expr)))]
    [(isNot? expr) (list '~
           (simplifyCNF (op1 expr)))]
    [else expr]
    )
)

Simplify CNF

To simplify an expression to CNF, we just apply the rules until the expression is in CNF form.

;Convert to CNF
;Repeatedly apply the rules until you reach CNF form
;input-contract: a valid boolean expression
;output-contract: an equivalent expression in CNF Form
(define (cnf expr)
  (if (isCNF? expr)
      expr
      (cnf (simplifyCNF expr))))

(display "CNF Examples:\n")
(display (cnf '(v (& A B) (& C D))))(newline)
; Returns '(& (& (v A C) (v A D)) (& (v B C) (v B D)))
(display (cnf '(~ (<-> A B))))(newline)
; Returns '(& (& (v A B) (v A (~ A))) (& (v (~ B) B) (v (~ B) (~ A))))

Full Code Example

The full file is provided below.

#lang racket
;Mark Boady
;Drexel University 2021

;This code simplifies an expression to CNF.

;----------------------------------------
;Section 1: Basic Predicates and Helpers
;----------------------------------------

;Get the first operand of an expression
;input-contract: A valid expression
;output-contact: The first operand
(define (op1 exp)
  (second exp)
)
;Get the second operand of an expression
;input-contract: A valid expression
;output-contact: The second operand
(define (op2 exp)
  (third exp)
)

;Detect Expression Type
;Given an operator and list length
;creates a procedure to detect expressions of that format
;input-contract: (and (symbol? op) (integer? len))
;output-contract: (procedure? (isOperator op len))
(define (isOperator op len)
  (lambda (expr)
    (and
     (list? expr)
     (equal? (length expr) len)
     (equal? op (first expr))
    )
 )
)
;Define the formats we need
;Negation only takes 1 input
;Other Boolean Operators are 2 inputs and the operator
(define isNot? (isOperator '~ 2) )
(define isAnd? (isOperator '& 3) )
(define isOr?  (isOperator 'v 3) )
(define isImplies? (isOperator '-> 3))
(define isBicond? (isOperator '<-> 3))


;----------------------------------------
;Section 2: Convert to NNF
;----------------------------------------

;Rule 1: Definition of Implies
;(A->B) = (~A v B)
;input-contract: A valid implies expression
;output-contract: The expression rewritten as an or
(define (defOfImplies expr)
  (list 'v (list '~ (op1 expr)) (op2 expr))
)
(display "Def of Implies Example:\n")
(display (defOfImplies '(-> X Y)))(newline)
; Returns '(v (~ X) Y)

;Rule 2: Definition of Bi-Conditional
;(A <-> B) = (A->B) & (B->A)
;input-contract: A valid bi-conditional expression
;output-contract: The expression rewritten as an or+implies
(define (defOfBicond expr)
  (list '&
        (list '-> (op1 expr) (op2 expr))
        (list '-> (op2 expr) (op1 expr))
  )
)
(display "Def of Bi-Conditional Example:\n")
(display (defOfBicond '(<-> X Y)))(newline)
; Returns '(v (-> X Y) (-> Y X))

;Rule 3: DeMorgan on Disjunction
;~(A v B) = (~A & ~B)
;input-contract: A valid boolean expression with negative applied to or
;output-contract: The expression rewritten using DeMorgan's Law
(define (deMorganDis expr)
  (list '&
        (list '~ (op1 (op1 expr)))
        (list '~ (op2 (op1 expr)))
  )
)
(display "DeMorgan on Disjunction Example:\n")
(display (deMorganDis '(~ (v X Y))))(newline)
; Returns '(& (~ X) (~ Y))

;Rule 4: DeMorgan on Conjunction
;~(A & B) = (~A v ~B)
;input-contract: A valid boolean expression with negative applied to and
;output-contract: The expression rewritten using DeMorgan's Law
(define (deMorganConj expr)
  (list 'v
        (list '~ (op1 (op1 expr)))
        (list '~ (op2 (op1 expr)))
  )
)
(display "DeMorgan on Conjunction Example:\n")
(display (deMorganConj '(~ (& X Y))))(newline)
; Returns '(v (~ X) (~ Y))

;Rule 5: Double Negative Elimination
;~ ~ A = A
;input-contract: A valid boolean expression with a double negative
;output-contract: The expression with double negative removed
(define (doubleNeg expr)
  (op1 (op1 expr))
)
(display "Double Negative Elimination Example:\n")
(display (doubleNeg '(~ (~ (v A B)))))(newline)
; Returns '(v A B)

;Determine if a Function is in NNF form or not
;input-contract: A valid boolean expression
;output-contract: #t if in NNF and #f otherwise
(define (isNNF? expr)
  (cond
    ;These operators are fine, but check operands
    [(or (isAnd? expr) (isOr? expr))
     (and (isNNF? (op1 expr)) (isNNF? (op2 expr)))]
    ;These operators are not allowed
    [(isImplies? expr) #f]
    [(isBicond? expr) #f]
    ;Not cannot be applied to operators
    [(isNot? expr) (not (list? (op1 expr)))]
    ;None of the above
    [else #t]
  )
)

;Apply Rules of NNF
;Applies any rules it finds to the expression
;input-contract: A boolean expression
;output-contract: an equivalent boolean expression with rules applied
(define (simplifyNNF expr)
  (cond
    ;Operator Defs
    [(isImplies? expr) (defOfImplies expr)]
    [(isBicond? expr) (defOfBicond expr)]
    ;DeMorgan
    [(and (isNot? expr) (isOr? (op1 expr)))
     (deMorganDis expr)]
    [(and (isNot? expr) (isAnd? (op1 expr)))
     (deMorganConj expr)]
    ;Double Negative
    [(and (isNot? expr) (isNot? (op1 expr)))
     (doubleNeg expr)]
    ;Basic Operators
    [(isNot? expr) (list '~ (simplifyNNF (op1 expr)))]
    [(isAnd? expr) (list '& (simplifyNNF (op1 expr))
                         (simplifyNNF (op2 expr)))]
    [(isOr? expr) (list 'v (simplifyNNF (op1 expr))
                        (simplifyNNF (op2 expr)))]
    ;None of the above
    [else expr]
  )
)


;Convert to NNF
;Apply Rules until the expression is in NNF
;input-contract: a valid boolean expression
;output-contract: the same expression in NNF
(define (nnf expr)
  ;(display expr)(newline) ;Uncomment to see steps
  (if (isNNF? expr)
      expr
      (nnf (simplifyNNF expr))
  )
)

(display "Convert to NNF Examples:\n")
(display (nnf '(<-> A B)))(newline)
; Returns '(v (v (~ A) B) (v (~ B) A))
(display (nnf '(~ (<-> A B))))(newline)
; Returns '(& (& A (~ B)) (& B (~ A)))
(display (nnf '(~ (& (<-> A B) (-> (~ C) D)))))(newline)
; Returns '(v (v (& A (~ B)) (& B (~ A))) (& (~ C) (~ D)))
(display (nnf '(~ (& A (v B C)))))(newline)
; Returns (v ~A (& (~ B) (~ C)))


;----------------------------------------
; Section 3: Convert CNF
;----------------------------------------

;Rule 1: Distribute Or
;(A & B) v C = (A v C) & (B v C)
;A v (B & C) = (A v B) & (A v C)
;input-contract: A boolean expression that needs to be
;                distributed
;output-contract: The expression after distribution
(define (distributeOr expr)
  (if (isAnd? (op1 expr))
      (list '&
            (list 'v (op1 (op1 expr))
                     (op2 expr))
            (list 'v (op2 (op1 expr))
                  (op2 expr))
      )
      (list '&
            (list 'v (op1 expr)
                     (op1 (op2 expr)))
            (list 'v (op1 expr)
                  (op2 (op2 expr)))
      )
 )
)
(display "Distribution Examples:\n")
(display (distributeOr '(v (& A B) C)))(newline)
; Returns '(& (v A C) (v B C))
(display (distributeOr '(v A (& B C))))(newline)
; Returns '(& (v A B) (v A C))

;Check if an expression is in CNF form
;input-contract: A valid boolean expression
;output-contract: #t if in CNF and #f otherwise
(define (isCNF? expr)
  (cond
    [(not (isNNF? expr)) #f]
    [(and (isOr? expr)
          (or (isAnd? (op1 expr)) (isAnd? (op2 expr))))
     #f]
    [(or (isAnd? expr) (isOr? expr))
     (and (isCNF? (op1 expr)) (isCNF? (op2 expr)))]
    [else #t]
  )
)

;Apply Rules of CNF Form
;Applies any rules it finds once
;input-contract: a valid boolean expression
;output-contract: the expression simplified using rules
(define (simplifyCNF expr)
  (cond
    [(not (isNNF? expr)) (nnf expr)]
    [(and (isOr? expr)
          (or (isAnd? (op1 expr)) (isAnd? (op2 expr))))
     (distributeOr expr)]
    [(isAnd? expr) (list '&
           (simplifyCNF (op1 expr))
           (simplifyCNF (op2 expr)))]
    [(isOr? expr) (list 'v
           (simplifyCNF (op1 expr))
           (simplifyCNF (op2 expr)))]
    [(isNot? expr) (list '~
           (simplifyCNF (op1 expr)))]
    [else expr]
    )
)

;Convert to CNF
;Repeatedly apply the rules until you reach CNF form
;input-contract: a valid boolean expression
;output-contract: an equivalent expression in CNF Form
(define (cnf expr)
  (if (isCNF? expr)
      expr
      (cnf (simplifyCNF expr))))

(display "CNF Examples:\n")
(display (cnf '(v (& A B) (& C D))))(newline)
; Returns '(& (& (v A C) (v A D)) (& (v B C) (v B D)))
(display (cnf '(~ (<-> A B))))(newline)
; Returns '(& (& (v A B) (v A (~ A))) (& (v (~ B) B) (v (~ B) (~ A))))

Conclusion

Any boolean expression can be converted to CNF form. This is a purely mechanical process. It can be implemented recursively. We can let a computer apply the rules for us. This code every produces a value as a result. It takes symbolic expressions and rewrites them into different but equivalent expressions.

previous

Normal Forms

next

SAT Solvers