SymmetryGroup - Maple Help

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

Logic

 SymmetryGroup
 find symmetries in a logical expression

 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.

 > $\mathrm{with}\left(\mathrm{Logic}\right):$
 > $\mathrm{expr}≔\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}c\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(c\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}d\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}e\right)$
 ${\mathrm{expr}}{≔}\left({a}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{b}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{c}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({c}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{d}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{e}\right)$ (1)
 > $G≔\mathrm{SymmetryGroup}\left(\mathrm{expr}\right)$
 ${G}{≔}⟨\left({1}{,}{2}\right)\left({6}{,}{7}\right){,}\left({4}{,}{10}\right)\left({5}{,}{9}\right){,}\left({1}{,}{10}\right)\left({2}{,}{4}\right)\left({3}{,}{8}\right)\left({5}{,}{6}\right)\left({7}{,}{9}\right)\left({11}{,}{12}\right)⟩$ (2)

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

 > $\mathrm{GroupTheory}:-\mathrm{IsAbelian}\left(G\right)$
 ${\mathrm{false}}$ (3)
 > $\mathrm{GroupTheory}:-\mathrm{IdentifySmallGroup}\left(G\right)$
 ${8}{,}{3}$ (4)

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

 > $G,L≔\mathrm{SymmetryGroup}\left(\mathrm{expr},\mathrm{output}=\left[\mathrm{group},\mathrm{expressions}\right]\right)$
 ${G}{,}{L}{≔}⟨\left({1}{,}{2}\right)\left({6}{,}{7}\right){,}\left({4}{,}{10}\right)\left({5}{,}{9}\right){,}\left({1}{,}{10}\right)\left({2}{,}{4}\right)\left({3}{,}{8}\right)\left({5}{,}{6}\right)\left({7}{,}{9}\right)\left({11}{,}{12}\right)⟩{,}\left[{a}{,}{b}{,}{c}{,}{d}{,}{e}{,}{¬}{a}{,}{¬}{b}{,}{¬}{c}{,}{¬}{d}{,}{¬}{e}{,}{a}{\vee }{b}{\vee }\left({¬}{c}\right){,}{c}{\vee }{d}{\vee }\left({¬}{e}\right)\right]$ (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.

 > $\mathrm{gen}≔\mathrm{Perm}\left(\left[\left[1,10\right],\left[2,4\right],\left[3,8\right],\left[5,6\right],\left[7,9\right],\left[11,12\right]\right]\right)$
 ${\mathrm{gen}}{≔}\left({1}{,}{10}\right)\left({2}{,}{4}\right)\left({3}{,}{8}\right)\left({5}{,}{6}\right)\left({7}{,}{9}\right)\left({11}{,}{12}\right)$ (6)
 > $\mathrm{GroupTheory}:-\mathrm{ElementOrder}\left(\mathrm{gen},G\right)$
 ${2}$ (7)
 > $\mathrm{zip}\left(\mathrm{=},L,L\left[\mathrm{convert}\left(\mathrm{gen},\mathrm{permlist},\mathrm{nops}\left(L\right)\right)\right]\right)$
 $\left[{a}{=}{¬}{e}{,}{b}{=}{d}{,}{c}{=}{¬}{c}{,}{d}{=}{b}{,}{e}{=}{¬}{a}{,}{¬}{a}{=}{e}{,}{¬}{b}{=}{¬}{d}{,}{¬}{c}{=}{c}{,}{¬}{d}{=}{¬}{b}{,}{¬}{e}{=}{a}{,}{a}{\vee }{b}{\vee }\left({¬}{c}\right){=}{c}{\vee }{d}{\vee }\left({¬}{e}\right){,}{c}{\vee }{d}{\vee }\left({¬}{e}\right){=}{a}{\vee }{b}{\vee }\left({¬}{c}\right)\right]$ (8)

Find symmetries and expressions for another simple Boolean expression.

 > $\mathrm{expr}≔\left(x\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}x\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}y\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}z\right)$
 ${\mathrm{expr}}{≔}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{y}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{z}\right)$ (9)
 > $G,L≔\mathrm{SymmetryGroup}\left(\mathrm{expr},\mathrm{output}=\left[\mathrm{group},\mathrm{expressions}\right]\right)$
 ${G}{,}{L}{≔}⟨\left({1}{,}{2}\right)\left({4}{,}{5}\right){,}\left({2}{,}{3}\right)\left({5}{,}{6}\right){,}\left({8}{,}{9}\right)⟩{,}\left[{x}{,}{y}{,}{z}{,}{¬}{x}{,}{¬}{y}{,}{¬}{z}{,}{x}{\vee }{y}{\vee }{z}{,}\left({¬}{x}\right){\vee }\left({¬}{y}\right){\vee }\left({¬}{z}\right){,}\left({¬}{x}\right){\vee }\left({¬}{y}\right){\vee }\left({¬}{z}\right)\right]$ (10)
 > $\mathrm{GroupTheory}:-\mathrm{GroupOrder}\left(G\right)$
 ${12}$ (11)

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

 > $\mathrm{expr}≔\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}c\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}d\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(d\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}a\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}c\right)$
 ${\mathrm{expr}}{≔}\left({a}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{b}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{c}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{d}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({d}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{a}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({a}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{c}\right)$ (12)
 > $\mathrm{SymmetryGroup}\left(\mathrm{expr}\right)$

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

 > $\mathrm{expr_cnf}≔\mathrm{Normalize}\left(\mathrm{expr},\mathrm{form}=\mathrm{CNF}\right)$
 ${\mathrm{expr_cnf}}{≔}\left({a}{\vee }{d}\right){\wedge }\left(\left({¬}{a}\right){\vee }\left({¬}{c}\right)\right){\wedge }\left({a}{\vee }{d}{\vee }\left({¬}{c}\right)\right){\wedge }\left({d}{\vee }\left({¬}{b}\right){\vee }\left({¬}{c}\right)\right)$ (13)

Observe that the expression has no nontrivial symmetries.

 > $G≔\mathrm{SymmetryGroup}\left(\mathrm{expr_cnf}\right)$
 ${G}{≔}⟨⟩$ (14)
 > $\mathrm{GroupTheory}:-\mathrm{GroupOrder}\left(G\right)$
 ${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.