Tseitin - Maple Help

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

• 

The Tseitin command 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).

• 

It is possible to transform a boolean formula into CNF simply by repeated use of De Morgan's law, however in general this will result in an exponential increase in the number of terms. The result of Tseitin's transformation is linear in the number of Boolean operators in b.

• 

The result of the Tseitin command will typically include additional variables not present in the original expression.

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