diff options
Diffstat (limited to 'content/zettel/2d3.md')
| -rw-r--r-- | content/zettel/2d3.md | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/2d3.md b/content/zettel/2d3.md new file mode 100644 index 0000000..77e5324 --- /dev/null +++ b/content/zettel/2d3.md @@ -0,0 +1,25 @@ ++++ +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 |