blob: 77e53245161f28e11f1d527a42545396a2bb154a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
|
