Logic
Tseitin
apply Tseitin's transformation
Calling Sequence
Parameters
Description
Examples
References
Compatibility
Tseitin(b)
b
-
Boolean expression
Tseitin accepts an arbitrary Boolean expression b and returns an expression in conjunctive normal form (CNF) which is equisatisfiable, that is, a satisfying assignment of truth values exists for b if and only if a satisfying assignment exists for Tseitin(b).
The result of the Tseitin command will typically include additional variables not present in the original expression.
Note that it is possible to transform a boolean formula into CNF simply by repeated use of De Morgan's law, and this will produce an expression which is not merely equisatisfiable but logically equivalent. However, in general this will result in an exponential increase in the number of terms. By contrast the result of Tseitin's transformation is linear in the number of Boolean operators in b.
withLogic:
Tseitina &or b &and c
&orB0∧B0∨¬a∧B0∨¬B∧¬B0∨a∨B∧¬B∨b∧¬B∨c∧B∨¬b∨¬c
Tseitina &implies b
&andb∨¬a
Illustrate the difference in increase in expression size between a straightforward application of De Morgan's law and the Tseitin transform.
E ≔ `&or`X1 &and Y1,X2 &and Y2,X3 &and Y3,X4 &and Y4,X5 &and Y5,X6 &and Y6,X7 &and Y7,X8 &and Y8
E≔X1∧Y1∨X2∧Y2∨X3∧Y3∨X4∧Y4∨X5∧Y5∨X6∧Y6∨X7∧Y7∨X8∧Y8
Result_DeMorgan ≔ Logic:-NormalizeE,form=CNF
Result_DeMorgan≔X1∨X2∨X3∨X4∨X5∨X6∨X7∨X8∧X1∨X2∨X3∨X4∨X5∨X6∨X7∨Y8∧X1∨X2∨X3∨X4∨X5∨X6∨X8∨Y7∧X1∨X2∨X3∨X4∨X5∨X6∨Y7∨Y8∧X1∨X2∨X3∨X4∨X5∨X7∨X8∨Y6∧X1∨X2∨X3∨X4∨X5∨X7∨Y6∨Y8∧X1∨X2∨X3∨X4∨X5∨X8∨Y6∨Y7∧X1∨X2∨X3∨X4∨X5∨Y6∨Y7∨Y8∧X1∨X2∨X3∨X4∨X6∨X7∨X8∨Y5∧X1∨X2∨X3∨X4∨X6∨X7∨Y5∨Y8∧X1∨X2∨X3∨X4∨X6∨X8∨Y5∨Y7∧X1∨X2∨X3∨X4∨X6∨Y5∨Y7∨Y8∧X1∨X2∨X3∨X4∨X7∨X8∨Y5∨Y6∧X1∨X2∨X3∨X4∨X7∨Y5∨Y6∨Y8∧X1∨X2∨X3∨X4∨X8∨Y5∨Y6∨Y7∧X1∨X2∨X3∨X4∨Y5∨Y6∨Y7∨Y8∧X1∨X2∨X3∨X5∨X6∨X7∨X8∨Y4∧X1∨X2∨X3∨X5∨X6∨X7∨Y4∨Y8∧X1∨X2∨X3∨X5∨X6∨X8∨Y4∨Y7∧X1∨X2∨X3∨X5∨X6∨Y4∨Y7∨Y8∧X1∨X2∨X3∨X5∨X7∨X8∨Y4∨Y6∧X1∨X2∨X3∨X5∨X7∨Y4∨Y6∨Y8∧X1∨X2∨X3∨X5∨X8∨Y4∨Y6∨Y7∧X1∨X2∨X3∨X5∨Y4∨Y6∨Y7∨Y8∧X1∨X2∨X3∨X6∨X7∨X8∨Y4∨Y5∧X1∨X2∨X3∨X6∨X7∨Y4∨Y5∨Y8∧X1∨X2∨X3∨X6∨X8∨Y4∨Y5∨Y7∧X1∨X2∨X3∨X6∨Y4∨Y5∨Y7∨Y8∧X1∨X2∨X3∨X7∨X8∨Y4∨Y5∨Y6∧X1∨X2∨X3∨X7∨Y4∨Y5∨Y6∨Y8∧X1∨X2∨X3∨X8∨Y4∨Y5∨Y6∨Y7∧X1∨X2∨X3∨Y4∨Y5∨Y6∨Y7∨Y8∧X1∨X2∨X4∨X5∨X6∨X7∨X8∨Y3∧X1∨X2∨X4∨X5∨X6∨X7∨Y3∨Y8∧X1∨X2∨X4∨X5∨X6∨X8∨Y3∨Y7∧X1∨X2∨X4∨X5∨X6∨Y3∨Y7∨Y8∧X1∨X2∨X4∨X5∨X7∨X8∨Y3∨Y6∧X1∨X2∨X4∨X5∨X7∨Y3∨Y6∨Y8∧X1∨X2∨X4∨X5∨X8∨Y3∨Y6∨Y7∧X1∨X2∨X4∨X5∨Y3∨Y6∨Y7∨Y8∧X1∨X2∨X4∨X6∨X7∨X8∨Y3∨Y5∧X1∨X2∨X4∨X6∨X7∨Y3∨Y5∨Y8∧X1∨X2∨X4∨X6∨X8∨Y3∨Y5∨Y7∧X1∨X2∨X4∨X6∨Y3∨Y5∨Y7∨Y8∧X1∨X2∨X4∨X7∨X8∨Y3∨Y5∨Y6∧X1∨X2∨X4∨X7∨Y3∨Y5∨Y6∨Y8∧X1∨X2∨X4∨X8∨Y3∨Y5∨Y6∨Y7∧X1∨X2∨X4∨Y3∨Y5∨Y6∨Y7∨Y8∧X1∨X2∨X5∨X6∨X7∨X8∨Y3∨Y4∧X1∨X2∨X5∨X6∨X7∨Y3∨Y4∨Y8∧X1∨X2∨X5∨X6∨X8∨Y3∨Y4∨Y7∧X1∨X2∨X5∨X6∨Y3∨Y4∨Y7∨Y8∧X1∨X2∨X5∨X7∨X8∨Y3∨Y4∨Y6∧X1∨X2∨X5∨X7∨Y3∨Y4∨Y6∨Y8∧X1∨X2∨X5∨X8∨Y3∨Y4∨Y6∨Y7∧X1∨X2∨X5∨Y3∨Y4∨Y6∨Y7∨Y8∧X1∨X2∨X6∨X7∨X8∨Y3∨Y4∨Y5∧X1∨X2∨X6∨X7∨Y3∨Y4∨Y5∨Y8∧X1∨X2∨X6∨X8∨Y3∨Y4∨Y5∨Y7∧X1∨X2∨X6∨Y3∨Y4∨Y5∨Y7∨Y8∧X1∨X2∨X7∨X8∨Y3∨Y4∨Y5∨Y6∧X1∨X2∨X7∨Y3∨Y4∨Y5∨Y6∨Y8∧X1∨X2∨X8∨Y3∨Y4∨Y5∨Y6∨Y7∧X1∨X2∨Y3∨Y4∨Y5∨Y6∨Y7∨Y8∧X1∨X3∨X4∨X5∨X6∨X7∨X8∨Y2∧X1∨X3∨X4∨X5∨X6∨X7∨Y2∨Y8∧X1∨X3∨X4∨X5∨X6∨X8∨Y2∨Y7∧X1∨X3∨X4∨X5∨X6∨Y2∨Y7∨Y8∧X1∨X3∨X4∨X5∨X7∨X8∨Y2∨Y6∧X1∨X3∨X4∨X5∨X7∨Y2∨Y6∨Y8∧X1∨X3∨X4∨X5∨X8∨Y2∨Y6∨Y7∧X1∨X3∨X4∨X5∨Y2∨Y6∨Y7∨Y8∧X1∨X3∨X4∨X6∨X7∨X8∨Y2∨Y5∧X1∨X3∨X4∨X6∨X7∨Y2∨Y5∨Y8∧X1∨X3∨X4∨X6∨X8∨Y2∨Y5∨Y7∧X1∨X3∨X4∨X6∨Y2∨Y5∨Y7∨Y8∧X1∨X3∨X4∨X7∨X8∨Y2∨Y5∨Y6∧X1∨X3∨X4∨X7∨Y2∨Y5∨Y6∨Y8∧X1∨X3∨X4∨X8∨Y2∨Y5∨Y6∨Y7∧X1∨X3∨X4∨Y2∨Y5∨Y6∨Y7∨Y8∧X1∨X3∨X5∨X6∨X7∨X8∨Y2∨Y4∧X1∨X3∨X5∨X6∨X7∨Y2∨Y4∨Y8∧X1∨X3∨X5∨X6∨X8∨Y2∨Y4∨Y7∧X1∨X3∨X5∨X6∨Y2∨Y4∨Y7∨Y8∧X1∨X3∨X5∨X7∨X8∨Y2∨Y4∨Y6∧X1∨X3∨X5∨X7∨Y2∨Y4∨Y6∨Y8∧X1∨X3∨X5∨X8∨Y2∨Y4∨Y6∨Y7∧X1∨X3∨X5∨Y2∨Y4∨Y6∨Y7∨Y8∧X1∨X3∨X6∨X7∨X8∨Y2∨Y4∨Y5∧X1∨X3∨X6∨X7∨Y2∨Y4∨Y5∨Y8∧X1∨X3∨X6∨X8∨Y2∨Y4∨Y5∨Y7∧X1∨X3∨X6∨Y2∨Y4∨Y5∨Y7∨Y8∧X1∨X3∨X7∨X8∨Y2∨Y4∨Y5∨Y6∧X1∨X3∨X7∨Y2∨Y4∨Y5∨Y6∨Y8∧X1∨X3∨X8∨Y2∨Y4∨Y5∨Y6∨Y7∧X1∨X3∨Y2∨Y4∨Y5∨Y6∨Y7∨Y8∧X1∨X4∨X5∨X6∨X7∨X8∨Y2∨Y3∧X1∨X4∨X5∨X6∨X7∨Y2∨Y3∨Y8∧X1∨X4∨X5∨X6∨X8∨Y2∨Y3∨Y7∧X1∨X4∨X5∨X6∨Y2∨Y3∨Y7∨Y8∧X1∨X4∨X5∨X7∨X8∨Y2∨Y3∨Y6∧X1∨X4∨X5∨X7∨Y2∨Y3∨Y6∨Y8∧X1∨X4∨X5∨X8∨Y2∨Y3∨Y6∨Y7∧X1∨X4∨X5∨Y2∨Y3∨Y6∨Y7∨Y8∧X1∨X4∨X6∨X7∨X8∨Y2∨Y3∨Y5∧X1∨X4∨X6∨X7∨Y2∨Y3∨Y5∨Y8∧X1∨X4∨X6∨X8∨Y2∨Y3∨Y5∨Y7∧X1∨X4∨X6∨Y2∨Y3∨Y5∨Y7∨Y8∧X1∨X4∨X7∨X8∨Y2∨Y3∨Y5∨Y6∧X1∨X4∨
