OKlibrary  0.2.1.6
Permutations.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 15.12.2009 (Swansea) */
00002 /* Copyright 2009, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Basics.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/CombinatorialMatrices/Lisp/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00027 
00028 oklib_plain_include(eigen)$
00029 
00030 /* *************************************
00031    * Permutations as boolean functions *
00032    *************************************
00033 */
00034 
00035 /* 
00036    We consider permutations f of {1,...,m}, where for permutations
00037    we use the list representations (so that the set of all such
00038    representations is permutations(setn(m))).
00039    See ComputerAlgebra/Algebra/Lisp/Groupoids/Groups/SymmetricGroups.mac for
00040    the symmetric group.
00041    We represent f as a boolean function, considering f as a relation.
00042 
00043    We assume m = 2^k for natural k >= 1, so that the set {1,...,m} has the
00044    same cardinality as {0,1}^k. Using a bijection R{1,...,m} -> {0,1}^k for a
00045    representation, the mapping x -> y represented by the permutation f yields
00046    the boolean list append(R(x), R(y)) of length 2k.
00047    These lists are considered as the satisfying assignments of the
00048    corresponding boolean function.
00049 
00050    We fix R: {1,...,m} -> {0,1}^k, i -> R(i) as the standard representation of
00051    i-1 in binary, with (left-)padded zeros; in other words, R(i) is the
00052    unranking of i w.r.t. the lexicographical ordering of binary vectors of
00053    length k.
00054 
00055    So the transposition [2,1] (here m=2 and k=1), that is, the
00056    map 1->2, 2->1, yields the satisfying vectors {[0,1],[1,0]}, and thus
00057    the DNF-clause-set {{-1,2},{1,-2}}.
00058    And [2,4,1,3] yields the satisfying vectors
00059    {[0,0,0,1],[0,1,1,1],[1,0,0,0],[1,1,1,0]} and the DNF-clause-set
00060    {{-1,-2,-3,4},{-1,2,3,4},{1,-2,-3,-4},{1,2,3,-4}}.
00061    This is computed by the functions below as
00062      perm2dnffcl([2,1]) = [[1,2],[{-1,2},{-2,1}]]
00063      perm2dnffcl([2,4,1,3]) =
00064        [[1,2,3,4],[{-3,-2,-1,4},{-1,2,3,4},{-4,-3,-2,1},{-4,1,2,3}]].
00065 */
00066 
00067 /* Translating a transformation T (standardised, as list) into a boolean
00068    function as a full dnf.
00069    Prerequisite: T is a transformation of {1,...,2^k} for k >= 0.
00070 */
00071 trans2dnffcl(T) := block([m : length(T), k, V, F, R],
00072   k : fld(m),
00073   V : create_list(i,i,1,2*k),
00074   R : lambda([i],unrank_lex_bv(i,k)),
00075   F : map(append, map(R,create_list(i,i,1,m)), map(R,T)),
00076   return([V, map(bv2c,F)]))$
00077 trans2dnffcs(P) := fcl2fcs(trans2dnffcl(P))$
00078 
00079 /* The special case of a permutation: */
00080 perm2dnffcl(P) := trans2dnffcl(P)$
00081 perm2dnffcs(P) := fcl2fcs(perm2dnffcl(P))$
00082 
00083 /* Now representing the transformation as cnf: */
00084 trans2cnffcs(T) := block([m : length(T), FF : trans2dnffcs(T), k],
00085   k : fld(m),
00086   return([FF[1], setdifference(all_tass(setn(2*k)), FF[2])]))$
00087 
00088 perm2cnffcs(P) := trans2cnffcs(P)$
00089 
00090 /* Output of clause-set trans2cnffcs(T) to a file: */
00091 output_trans_fullcnf(T,filename) :=
00092   output_fcs(
00093     sconcat("The transformation ", T, " in full CNF representation."),
00094     trans2cnffcs(T),
00095     filename)$
00096 output_trans_fullcnf_stdname(T) := output_trans_fullcnf(T,"Transformation_full.cnf")$
00097 /* The special case of a permutation: */
00098 output_perm_fullcnf(P,filename) := output_trans_fullcnf(P,filename)$
00099 output_perm_fullcnf_stdname(P) := output_perm_fullcnf(P,"Permutation_full.cnf")$
00100 
00101 /* A linear transformation, given as a square 0-1-matrix M of order n, as a
00102    boolean function in 2n variables, represented as DNF resp CNF:
00103 */
00104 m2dnffcl(M) := block([n : matrix_size(M)[1], L],
00105   if n = 0 then return([[],[{}]]), /* needed since Maxima doesn't have matrices with 0 rows and 1 column */
00106   L : lex_bv_l(n),
00107   [create_list(i,i,1,2*n),
00108    map(bv2c, 
00109        map(append, 
00110            L, 
00111            map(lambda([x], mod(column_m(M.columnvector(x),1),2)), L)))])$
00112 m2dnffcs(M) := fcl2fcs(m2dnffcl(M))$
00113 m2cnffcs(M) := block([n : matrix_size(M)[1], FF : m2dnffcs(M)],
00114   [FF[1], setdifference(all_tass(setn(2*n)), FF[2])])$
00115 
00116 /* Output of clause-set m2cnffcs(M) to a file: */
00117 output_m_fullcnf(M,filename) :=
00118   output_fcs(
00119     sconcat("The linear transformation ", M, " in full CNF representation."),
00120     m2cnffcs(M),
00121     filename)$
00122 output_m_fullcnf_stdname(M) := output_m_fullcnf(M,"LinearTransformation_full.cnf")$
00123