Logic - Maple Programming Help

Online Help

All Products    Maple    MapleSim


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

Logic

  

SymmetryGroup

  

find symmetries in a logical expression

 

Calling Sequence

Parameters

Options

Description

Definitions

Examples

References

Compatibility

Calling Sequence

SymmetryGroup(expr, opts)

Parameters

expr

-

Boolean expression in conjunctive normal form

opts

-

(optional) zero or more options as specified below

Options

• 

output=list or one of expressions or group

  

a list of one or more of the symbols expressions or group, or one of the symbols expressions or group.

  

The symbol group corresponds to the symmetry group for expr. The group is a permutation group; its elements are those permutations which preserve the Boolean structure of expr. If there are no nontrivial symmetries the group will be the trivial group.

  

The symbol expressions is the list of subexpressions of expr on which the permutations act.

Description

• 

The SymmetryGroup command computes the group of symmetries of a given Boolean expression expr.

• 

The result is a Group object and can be examined using the tools in the GroupTheory package.

• 

The expression expr must be in conjunctive normal form (CNF). If not already in CNF, expr can be converted to CNF using Normalize; alternatively, Tseitin may be used to find an equisatifiable expression in CNF.

Definitions

• 

A symmetry of a Boolean expression expr is a mapping f of each variable to some other variable or negated variable, such that the image of expr after applying f to each of its variables is a Boolean formula which is equivalent to expr.

Examples

Find symmetries for a simple Boolean expression.

withLogic:

expraorbornotcandcordornote

expraorbornotcandcordornote

(1)

GSymmetryGroupexpr

G1,102,43,85,67,911,12,1,26,7,4,105,9

(2)

We can see that the symmetry group is non-Abelian and is isomorphic to SmallGroup(8,3).

GroupTheory:-IsAbelianG

false

(3)

GroupTheory:-IdentifySmallGroupG

8,3

(4)

By invoking SymmetryGroup with the output option we can obtain the list L of subexpressions.

G,LSymmetryGroupexpr,output=group,expressions

G,L1,102,43,85,67,911,12,1,26,7,4,105,9,a,b,c,d,e,¬a,¬b,¬c,¬d,¬e,ab¬c,cd¬e

(5)

We can apply one of the generators of G to L to see an example of a symmetry in action. In this example, a is swapped with not e, b is swapped with d, and c is swapped with its negation.

genPerm1,10,2,4,3,8,5,6,7,9,11,12

gen1,102,43,85,67,911,12

(6)

GroupTheory:-ElementOrdergen,G

2

(7)

zip`=`,L,Lconvertgen,permlist,nopsL

a=¬e,b=d,c=¬c,d=b,e=¬a,¬a=e,¬b=¬d,¬c=c,¬d=¬b,¬e=a,ab¬c=cd¬e,cd¬e=ab¬c

(8)

Find symmetries and expressions for another simple Boolean expression.

exprxoryorzandnotxornotyornotzandnotxornotyornotz

exprxoryorzandnotxandyandzandnotxandyandz

(9)

G,LSymmetryGroupexpr,output=group,expressions

G,L1,24,5,2,35,6,8,9,x,y,z,¬x,¬y,¬z,xyz,¬x¬y¬z,¬x¬y¬z

(10)

GroupTheory:-GroupOrderG

12

(11)

Attempt to compute symmetries on an expression which is not in conjunctive normal form (CNF).

expraandnotbornotcordanddoraandnotaandc

expraandnotbornotcordanddoraandnotaandc

(12)

SymmetryGroupexpr

Error, (in Logic:-SymmetryGroup) not in conjunctive normal form

Convert to CNF using Normalize. Note this may be costly for large expressions.

expr_cnfNormalizeexpr,form=CNF

expr_cnfad¬a¬cad¬cd¬b¬c

(13)

Observe that the expression has no nontrivial symmetries.

GSymmetryGroupexpr_cnf

G

(14)

GroupTheory:-GroupOrderG

1

(15)

References

  

Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah. "Solving difficult instances of Boolean satisfiability in the presence of symmetry." IEEE Trans. CAD Integr. Circ. Syst. 22(9), 1117–1137 (2003). doi:10.1109/TCAD.2003.816218

Compatibility

• 

The Logic[SymmetryGroup] command was introduced in Maple 2020.

• 

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

See Also

GraphTheory[AutomorphismGroup]

GroupTheory

Logic