Copyright | Copyright (C) 2023 Yoo Chung |
---|---|

License | GPL-3.0-or-later |

Maintainer | dev@chungyc.org |

Safe Haskell | Safe-Inferred |

Language | GHC2021 |

Part of Ninety-Nine Haskell Problems. Some solutions are in Solutions.P52.

# Documentation

toConjunctiveNormalForm :: Formula -> Formula Source #

It is known that any boolean function can be represented in conjunctive normal form. These are conjunctions of disjunctions of literals, where literals are one of boolean values, variables, or the complement of values or variables. For example, the boolean formula \(\neg(x \wedge \neg y) \wedge (z \vee w)\) is equivalent to the conjunctive normal form \( (\neg x \vee y) \wedge (z \vee w) \).

Return the conjunctive normal form of a boolean formula. The value returned should always be a conjunction of disjunctions.

### Examples

`>>>`

Conjoin [Disjoin [Value True]]`toConjunctiveNormalForm $ Value True`

`>>>`

Conjoin [Disjoin [Complement (Variable "X")],Disjoin [Complement (Variable "Y")]]`toConjunctiveNormalForm $ Complement $ Disjoin [Variable "X", Variable "Y"]`

`>>>`

toConjunctiveNormalForm $ Disjoin [ Variable "X" , Conjoin [ Complement $ Variable "Y" , Variable "Z" ] ] :} Conjoin [Disjoin [Variable "X",Complement (Variable "Y")],Disjoin ...`:{`

### Hint

Transform a boolean formula using De Morgan's law, the distributive law, and double negation elimination to reduce nesting. Alternatively, the conjunctive normal form can be obtained easily from the truth table, although this will always require a running time exponential to the number of variables.

Represents a boolean formula.

Value Bool | A constant value. |

Variable String | A variable with given name. |

Complement Formula | Logical complement. I.e., it is true only if its clause is false. |

Disjoin [Formula] | Disjunction. I.e., it is true if any of its clauses are true. |

Conjoin [Formula] | Conjunction. I.e., it is true only if all of its clauses are true. |

#### Instances

# Supporting functions

The function below is not part of the problem.