diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-11 19:38:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-11 19:38:03 +0100 |
commit | 47c1289ff658a5aec71635d79ffe30bb29a07876 (patch) | |
tree | 56cf6b959e37fed88c492d34defd3d7ec40e7148 /content/zettel/2d3.md | |
parent | fbe0fc62120348f582dc4db2b614078943d0764b (diff) | |
download | zk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.tar.gz zk-web-47c1289ff658a5aec71635d79ffe30bb29a07876.zip |
Add content
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 |