+++
title = "Converting a formula to CNF"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["2d2"]
forwardlinks = ["2d4"]
zettelid = "2d3"
+++

This can be quite easy, as each construct can be converted to CNF
recursively.

``` text
convert(P & Q) -> convert(P) & convert(Q) convert(P | Q) -> foreach convert(Q)
-> q_i | convert(P)
```

However, this can result in an exponential growth of the formula. There
are other techniques that will transform the formula into a
equisatisfiable formula, which is not equivalent to the original, but
enough so for the purpose of a satisfiability check. These can be
transformations such as the Tseitin transformation ([\#2d4]).

  [\#2d4]: /zettel/2d4