Tseitin - Maple Help
For the best experience, we recommend viewing online help using Google Chrome or Microsoft Edge.

Online Help

All Products    Maple    MapleSim


Logic

  

Tseitin

  

apply Tseitin's transformation

 

Calling Sequence

Parameters

Description

Examples

References

Compatibility

Calling Sequence

Tseitin(b)

Parameters

b

-

Boolean expression

Description

• 

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.

Examples

> 

with⁡Logic:

> 

Tseitin⁡a&orb&andc

&or⁡B0∧B0∨¬a∧B0∨¬B∧¬B0∨a∨B∧¬B∨b∧¬B∨c∧B∨¬b∨¬c

(1)
> 

Tseitin⁡a&impliesb

&and⁡b∨¬a

(2)

Illustrate the difference in increase in expression size between a straightforward application of De Morgan's law and the Tseitin transform.

> 

E≔`&or`⁡X1&andY1,X2&andY2,X3&andY3,X4&andY4,X5&andY5,X6&andY6,X7&andY7,X8&andY8

E≔X1∧Y1∨X2∧Y2∨X3∧Y3∨X4∧Y4∨X5∧Y5∨X6∧Y6∨X7∧Y7∨X8∧Y8

(3)
> 

Result_DeMorgan≔Logic:-Normalize⁡E,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∨X7∨Y2∨Y3∨Y5∨Y6∨Y8∧X1∨X4∨X8∨Y2∨Y3∨Y5∨Y6∨Y7∧X1∨X4∨Y2∨Y3∨Y5∨Y6∨Y7∨Y8∧X1∨X5∨X6∨X7∨X8∨Y2∨Y3∨Y4∧X1∨X5∨X6∨X7∨Y2∨Y3∨Y4∨Y8∧X1∨X5∨X6∨X8∨Y2∨Y3∨Y4∨Y7∧X1∨X5∨X6∨Y2∨Y3∨Y4∨Y7∨Y8∧X1∨X5∨X7∨X8∨Y2∨Y3∨Y4∨Y6∧X1∨X5∨X7∨Y2∨Y3∨Y4∨Y6∨Y8∧X1∨X5∨X8∨Y2∨Y3∨Y4∨Y6∨Y7∧X1∨X5∨Y2∨Y3∨Y4∨Y6∨Y7∨Y8∧X1∨X6∨X7∨X8∨Y2∨Y3∨Y4∨Y5∧X1∨X6∨X7∨Y2∨Y3∨Y4∨Y5∨Y8∧X1∨X6∨X8∨Y2∨Y3∨Y4∨Y5∨Y7∧X1∨X6∨Y2∨Y3∨Y4∨Y5∨Y7∨Y8∧X1∨X7∨X8∨Y2∨Y3∨Y4∨Y5∨Y6∧X1∨X7∨Y2∨Y3∨Y4∨Y5∨Y6∨Y8∧X1∨X8∨Y2∨Y3∨Y4∨Y5∨Y6∨Y7∧X1∨Y2∨Y3∨Y4∨Y5∨Y6∨Y7∨Y8∧X2∨X3∨X4∨X5∨X6∨X7∨X8∨Y1∧X2∨X3∨X4∨X5∨X6∨X7∨Y1∨Y8∧X2∨X3∨X4∨X5∨X6∨X8∨Y1∨Y7∧X2∨X3∨X4∨X5∨X6∨Y1∨Y7∨Y8∧X2∨X3∨X4∨X5∨X7∨X8∨Y1∨Y6∧X2∨X3∨X4∨X5∨X7∨Y1∨Y6∨Y8∧X2∨X3∨X4∨X5∨X8∨Y1∨Y6∨Y7∧X2∨X3∨X4∨X5∨Y1∨Y6∨Y7∨Y8∧X2∨X3∨X4∨X6∨X7∨X8∨Y1∨Y5∧X2∨X3∨X4∨X6∨X7∨Y1∨Y5∨Y8∧X2∨X3∨X4∨X6∨X8∨Y1∨Y5∨Y7∧X2∨X3∨X4∨X6∨Y1∨Y5∨Y7∨Y8∧X2∨X3∨X4∨X7∨X8∨Y1∨Y5∨Y6∧X2∨X3∨X4∨X7∨Y1∨Y5∨Y6∨Y8∧X2∨X3∨X4∨X8∨Y1∨Y5∨Y6∨Y7∧X2∨X3∨X4∨Y1∨Y5∨Y6∨Y7∨Y8∧X2∨X3∨X5∨X6∨X7∨X8∨Y1∨Y4∧X2∨X3∨X5∨X6∨X7∨Y1∨Y4∨Y8∧X2∨X3∨X5∨X6∨X8∨Y1∨Y4∨Y7∧X2∨X3∨X5∨X6∨Y1∨Y4∨Y7∨Y8∧X2∨X3∨X5∨X7∨X8∨Y1∨Y4∨Y6∧X2∨X3∨X5∨X7∨Y1∨Y4∨Y6∨Y8∧X2∨X3∨X5∨X8∨Y1∨Y4∨Y6∨Y7∧X2∨X3∨X5∨Y1∨Y4∨Y6∨Y7∨Y8∧X2∨X3∨X6∨X7∨X8∨Y1∨Y4∨Y5∧X2∨X3∨X6∨X7∨Y1∨Y4∨Y5∨Y8∧X2∨X3∨X6∨X8∨Y1∨Y4∨Y5∨Y7∧X2∨X3∨X6∨Y1∨Y4∨Y5∨Y7∨Y8∧X2∨X3∨X7∨X8∨Y1∨Y4∨Y5∨Y6∧X2∨X3∨X7∨Y1∨Y4∨Y5∨Y6∨Y8∧X2∨X3∨X8∨Y1∨Y4∨Y5∨Y6∨Y7∧X2∨X3∨Y1∨Y4∨Y5∨Y6∨Y7∨Y8∧X2∨X4∨X5∨X6∨X7∨X8∨Y1∨Y3∧X2∨X4∨X5∨X6∨X7∨Y1∨Y3∨Y8∧X2∨X4∨X5∨X6∨X8∨Y1∨Y3∨Y7∧X2∨X4∨X5∨X6∨Y1∨Y3∨Y7∨Y8∧X2∨X4∨X5∨X7∨X8∨Y1∨Y3∨Y6∧X2∨X4∨X5∨X7∨Y1∨Y3∨Y6∨Y8∧X2∨X4∨X5∨X8∨Y1∨Y3∨Y6∨Y7∧X2∨X4∨X5∨Y1∨Y3∨Y6∨Y7∨Y8∧X2∨X4∨X6∨X7∨X8∨Y1∨Y3∨Y5∧X2∨X4∨X6∨X7∨Y1∨Y3∨Y5∨Y8∧X2∨X4∨X6∨X8∨Y1∨Y3∨Y5∨Y7∧X2∨X4∨X6∨Y1∨Y3∨Y5∨Y7∨Y8∧X2∨X4∨X7∨X8∨Y1∨Y3∨Y5∨Y6∧X2∨X4∨X7∨Y1∨Y3∨Y5∨Y6∨Y8∧X2∨X4∨X8∨Y1∨Y3∨Y5∨Y6∨Y7∧X2∨X4∨Y1∨Y3∨Y5∨Y6∨Y7∨Y8∧X2∨X5∨X6∨X7∨X8∨Y1∨Y3∨Y4∧X2∨X5∨X6∨X7∨Y1∨Y3∨Y4∨Y8∧X2∨X5∨X6∨X8∨Y1∨Y3∨Y4∨Y7∧X2∨X5∨X6∨Y1∨Y3∨Y4∨Y7∨Y8∧X2∨X5∨X7∨X8∨Y1∨Y3∨Y4∨Y6∧X2∨X5∨X7∨Y1∨Y3∨Y4∨Y6∨Y8∧X2∨X5∨X8∨Y1∨Y3∨Y4∨Y6∨Y7∧X2∨X5∨Y1∨Y3∨Y4∨Y6∨Y7∨Y8∧X2∨X6∨X7∨X8∨Y1∨Y3∨Y4∨Y5∧X2∨X6∨X7∨Y1∨Y3∨Y4∨Y5∨Y8∧X2∨X6∨X8∨Y1∨Y3∨Y4∨Y5∨Y7∧X2∨X6∨Y1∨Y3∨Y4∨Y5∨Y7∨Y8∧X2∨X7∨X8∨Y1∨Y3∨Y4∨Y5∨Y6∧X2∨X7∨Y1∨Y3∨Y4∨Y5∨Y6∨Y8∧X2∨X8∨Y1∨Y3∨Y4∨Y5∨Y6∨Y7∧X2∨Y1∨Y3∨Y4∨Y5∨Y6∨Y7∨Y8∧X3∨X4∨X5∨X6∨X7∨X8∨Y1∨Y2∧X3∨X4∨X5∨X6∨X7∨Y1∨Y2∨Y8∧X3∨X4∨X5∨X6∨X8∨Y1∨Y2∨Y7∧X3∨X4∨X5∨X6∨Y1∨Y2∨Y7∨Y8∧X3∨X4∨X5∨X7∨X8∨Y1∨Y2∨Y6∧X3∨X4∨X5∨X7∨Y1∨Y2∨Y6∨Y8∧X3∨X4∨X5∨X8∨Y1∨Y2∨Y6∨Y7∧X3∨X4∨X5∨Y1∨Y2∨Y6∨Y7∨Y8∧X3∨X4∨X6∨X7∨X8∨Y1∨Y2∨Y5∧X3∨X4∨X6∨X7∨Y1∨Y2∨Y5∨Y8∧X3∨X4∨X6∨X8∨Y1∨Y2∨Y5∨Y7∧X3∨X4∨X6∨Y1∨Y2∨Y5∨Y7∨Y8∧X3∨X4∨X7∨X8∨Y1∨Y2∨Y5∨Y6∧X3∨X4∨X7∨Y1∨Y2∨Y5∨Y6∨Y8∧X3∨X4∨X8∨Y1∨Y2∨Y5∨Y6∨Y7∧X3∨X4∨Y1∨Y2∨Y5∨Y6∨Y7∨Y8∧X3∨X5∨X6∨X7∨X8∨Y1∨Y2∨Y4∧X3∨X5∨X6∨X7∨Y1∨Y2∨Y4∨Y8∧X3∨X5∨X6∨X8∨Y1∨Y2∨Y4∨Y7∧X3∨X5∨X6∨Y1∨Y2∨Y4∨Y7∨Y8∧X3∨X5∨X7∨X8∨Y1∨Y2∨Y4∨Y6∧X3∨X5∨X7∨Y1∨Y2∨Y4∨Y6∨Y8∧X3∨X5∨X8∨Y1∨Y2∨Y4∨Y6∨Y7∧X3∨X5∨Y1∨Y2∨Y4∨Y6∨Y7∨Y8∧X3∨X6∨X7∨X8∨Y1∨Y2∨Y4∨Y5∧X3∨X6∨X7∨Y1∨Y2∨Y4∨Y5∨Y8∧X3∨X6∨X8∨Y1∨Y2∨Y4∨Y5∨Y7∧X3∨X6∨Y1∨Y2∨Y4∨Y5∨Y7∨Y8∧X3∨X7∨X8∨Y1∨Y2∨Y4∨Y5∨Y6∧X3∨X7∨Y1∨Y2∨Y4∨Y5∨Y6∨Y8∧X3∨X8∨Y1∨Y2∨Y4∨Y5∨Y6∨Y7∧X3∨Y1∨Y2∨Y4∨Y5∨Y6∨Y7∨Y8∧X4∨X5∨X6∨X7∨X8∨Y1∨Y2∨Y3∧X4∨X5∨X6∨X7∨Y1∨Y2∨Y3∨Y8∧X4∨X5∨X6∨X8∨Y1∨Y2∨Y3∨Y7∧X4∨X5∨X6∨Y1∨Y2∨Y3∨Y7∨Y8∧X4∨X5∨X7∨X8∨Y1∨Y2∨Y3∨Y6∧X4∨X5∨X7∨Y1∨Y2∨Y3∨Y6∨Y8∧X4∨X5∨X8∨Y1∨Y2∨Y3∨Y6∨Y7∧X4∨X5∨Y1∨Y2∨Y3∨Y6∨Y7∨Y8∧X4∨X6∨X7∨X8∨Y1∨Y2∨Y3∨Y5∧X4∨X6∨X7∨Y1∨Y2∨Y3∨Y5∨Y8∧X4∨X6∨X8∨Y1∨Y2∨Y3∨Y5∨Y7∧X4∨X6∨Y1∨Y2∨Y3∨Y5∨Y7∨Y8∧X4∨X7∨X8∨Y1∨Y2∨Y3∨Y5∨Y6∧X4∨X7∨Y1∨Y2∨Y3∨Y5∨Y6∨Y8∧X4∨X8∨Y1∨Y2∨Y3∨Y5∨Y6∨Y7∧X4∨Y1∨Y2∨Y3∨Y5∨Y6∨Y7∨Y8∧X5∨X6∨X7∨X8∨Y1∨Y2∨Y3∨Y4∧X5∨X6∨X7∨Y1∨Y2∨Y3∨Y4∨Y8∧X5∨X6∨X8∨Y1∨Y2∨Y3∨Y4∨Y7∧X5∨X6∨Y1∨Y2∨Y3∨Y4∨Y7∨Y8∧X5∨X7∨X8∨Y1∨Y2∨Y3∨Y4∨Y6∧X5∨X7∨Y1∨Y2∨Y3∨Y4∨Y6∨Y8∧X5∨X8∨Y1∨Y2∨Y3∨Y4∨Y6∨Y7∧X5∨Y1∨Y2∨Y3∨Y4∨Y6∨Y7∨Y8∧X6∨X7∨X8∨Y1∨Y2∨Y3∨Y4∨Y5∧X6∨X7∨Y1∨Y2∨Y3∨Y4∨Y5∨Y8∧X6∨X8∨Y1∨Y2∨Y3∨Y4∨Y5∨Y7∧X6∨Y1∨Y2∨Y3∨Y4∨Y5∨Y7∨Y8∧X7∨X8∨Y1∨Y2∨Y3∨Y4∨Y5∨Y6∧X7∨Y1∨Y2∨Y3∨Y4∨Y5∨Y6∨Y8∧X8∨Y1∨Y2∨Y3∨Y4∨Y5∨Y6∨Y7∧Y1∨Y2∨Y3∨Y4∨Y5∨Y6∨Y7∨Y8

(4)
> 

length⁡Result_DeMorgan

8200

(5)
> 

Result_Tseitin≔Tseitin⁡E:

> 

length⁡Result_Tseitin

895

(6)

References

  

Tseitin, G.S. On the complexity of derivation in propositional calculus. In A. O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125, 1970.

Compatibility

• 

The Logic[Tseitin] command was introduced in Maple 2016.

• 

For more information on Maple 2016 changes, see Updates in Maple 2016.

See Also

Logic

Logic[Normalize]

Logic[Satisfy]