Logic - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Mathematics : Logic : Logic/Tseitin

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

withLogic:

Tseitina &or b &and c

&orB0B0¬aB0¬B¬B0aB¬Bb¬BcB¬b¬c

(1)

Tseitina &implies b

&andb¬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 &and Y1,X2 &and Y2,X3 &and Y3,X4 &and Y4,X5 &and Y5,X6 &and Y6,X7 &and Y7,X8 &and Y8

EX1Y1X2Y2X3Y3X4Y4X5Y5X6Y6X7Y7X8Y8

(3)

Result_DeMorganLogic:-NormalizeE,form=CNF

Result_DeMorganX1X2X3X4X5X6X7X8X1X2X3X4X5X6X7Y8X1X2X3X4X5X6X8Y7X1X2X3X4X5X6Y7Y8X1X2X3X4X5X7X8Y6X1X2X3X4X5X7Y6Y8X1X2X3X4X5X8Y6Y7X1X2X3X4X5Y6Y7Y8X1X2X3X4X6X7X8Y5X1X2X3X4X6X7Y5Y8X1X2X3X4X6X8Y5Y7X1X2X3X4X6Y5Y7Y8X1X2X3X4X7X8Y5Y6X1X2X3X4X7Y5Y6Y8X1X2X3X4X8Y5Y6Y7X1X2X3X4Y5Y6Y7Y8X1X2X3X5X6X7X8Y4X1X2X3X5X6X7Y4Y8X1X2X3X5X6X8Y4Y7X1X2X3X5X6Y4Y7Y8X1X2X3X5X7X8Y4Y6X1X2X3X5X7Y4Y6Y8X1X2X3X5X8Y4Y6Y7X1X2X3X5Y4Y6Y7Y8X1X2X3X6X7X8Y4Y5X1X2X3X6X7Y4Y5Y8X1X2X3X6X8Y4Y5Y7X1X2X3X6Y4Y5Y7Y8X1X2X3X7X8Y4Y5Y6X1X2X3X7Y4Y5Y6Y8X1X2X3X8Y4Y5Y6Y7X1X2X3Y4Y5Y6Y7Y8X1X2X4X5X6X7X8Y3X1X2X4X5X6X7Y3Y8X1X2X4X5X6X8Y3Y7X1X2X4X5X6Y3Y7Y8X1X2X4X5X7X8Y3Y6X1X2X4X5X7Y3Y6Y8X1X2X4X5X8Y3Y6Y7X1X2X4X5Y3Y6Y7Y8X1X2X4X6X7X8Y3Y5X1X2X4X6X7Y3Y5Y8X1X2X4X6X8Y3Y5Y7X1X2X4X6Y3Y5Y7Y8X1X2X4X7X8Y3Y5Y6X1X2X4X7Y3Y5Y6Y8X1X2X4X8Y3Y5Y6Y7X1X2X4Y3Y5Y6Y7Y8X1X2X5X6X7X8Y3Y4X1X2X5X6X7Y3Y4Y8X1X2X5X6X8Y3Y4Y7X1X2X5X6Y3Y4Y7Y8X1X2X5X7X8Y3Y4Y6X1X2X5X7Y3Y4Y6Y8X1X2X5X8Y3Y4Y6Y7X1X2X5Y3Y4Y6Y7Y8X1X2X6X7X8Y3Y4Y5X1X2X6X7Y3Y4Y5Y8X1X2X6X8Y3Y4Y5Y7X1X2X6Y3Y4Y5Y7Y8X1X2X7X8Y3Y4Y5Y6X1X2X7Y3Y4Y5Y6Y8X1X2X8Y3Y4Y5Y6Y7X1X2Y3Y4Y5Y6Y7Y8X1X3X4X5X6X7X8Y2X1X3X4X5X6X7Y2Y8X1X3X4X5X6X8Y2Y7X1X3X4X5X6Y2Y7Y8X1X3X4X5X7X8Y2Y6X1X3X4X5X7Y2Y6Y8X1X3X4X5X8Y2Y6Y7X1X3X4X5Y2Y6Y7Y8X1X3X4X6X7X8Y2Y5X1X3X4X6X7Y2Y5Y8X1X3X4X6X8Y2Y5Y7X1X3X4X6Y2Y5Y7Y8X1X3X4X7X8Y2Y5Y6X1X3X4X7Y2Y5Y6Y8X1X3X4X8Y2Y5Y6Y7X1X3X4Y2Y5Y6Y7Y8X1X3X5X6X7X8Y2Y4X1X3X5X6X7Y2Y4Y8X1X3X5X6X8Y2Y4Y7X1X3X5X6Y2Y4Y7Y8X1X3X5X7X8Y2Y4Y6X1X3X5X7Y2Y4Y6Y8X1X3X5X8Y2Y4Y6Y7X1X3X5Y2Y4Y6Y7Y8X1X3X6X7X8Y2Y4Y5X1X3X6X7Y2Y4Y5Y8X1X3X6X8Y2Y4Y5Y7X1X3X6Y2Y4Y5Y7Y8X1X3X7X8Y2Y4Y5Y6X1X3X7Y2Y4Y5Y6Y8X1X3X8Y2Y4Y5Y6Y7X1X3Y2Y4Y5Y6Y7Y8X1X4X5X6X7X8Y2Y3X1X4X5X6X7Y2Y3Y8X1X4X5X6X8Y2Y3Y7X1X4X5X6Y2Y3Y7Y8X1X4X5X7X8Y2Y3Y6X1X4X5X7Y2Y3Y6Y8X1X4X5X8Y2Y3Y6Y7X1X4X5Y2Y3Y6Y7Y8X1X4X6X7X8Y2Y3Y5X1X4X6X7Y2Y3Y5Y8X1X4X6X8Y2Y3Y5Y7X1X4X6Y2Y3Y5Y7Y8X1X4X7X8Y2Y3Y5Y6X1X4X7Y2Y3