OKlibrary  0.2.1.6
Permutations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 19.12.2009 (Swansea) */
00002 /* Copyright 2009, 2011, 2012 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/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Permutations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Primality/PrimeImplicatesImplicants.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00026 
00027 /* Evaluation of permutation P of {1,...,2^n}: */
00028 evalpermasbf(P) := block(
00029   [F : perm2cnffcs(P)[2], Pr, S, Min, pr,nec,min,s, L],
00030    Pr : min_2resolution_closure_cs(F),
00031    pr : length(Pr),
00032    S : rsubsumption_hg(Pr,F),
00033    nec : length(S[2]),
00034    Min : all_minequiv_bvs_rsubhg(S),
00035    min : length(Min),
00036    s : length(first(Min)),
00037    [pr, nec, s, min]
00038 )$
00039 
00040 /* For n >= 0, runs through the permutations P of {1,..,2^n}, determines the
00041    4-tuple [pr, nec, s, min], the number of prime implicates, the number of 
00042    irredundant clauses amongst them, the number of clauses in a minimum
00043    CNF representation, and the number of such representations.
00044    Returned is a hash-map, which for the occurring 4-tuples returns the
00045    list of permutations P belonging to them.
00046    If oklib_monitor is true, then the new permutations and their statistics
00047    are printed, together with a total count.
00048 */
00049 investigate_permutations(n) := block(
00050  [m : 2^n, h : sm2hm({}), count:0, countf:0,
00051   monitor : oklib_monitor, oklib_monitor: false],
00052  for P in permutations(setn(m)) do block([t, L],
00053    count:count+1,
00054    if monitor and oklib_monitor_level=0 then printf(true, "~d ", count),
00055    t : evalpermasbf(P),
00056    if monitor and oklib_monitor_level >= 1 then print(count, P, t),
00057    L : ev_hm(h,t),
00058    if monitor and L=false then (countf:countf+1, print("NEW:", countf, P, t)),
00059    set_hm(h,t, if L=false then [P] else cons(P,L))
00060  ),
00061  return(h))$
00062 
00063 /* Only run through the transpositions: */
00064 investigate_transpositions(n) := block(
00065  [m : 2^n, h : sm2hm({}), count:0, countf:0,
00066   monitor : oklib_monitor, oklib_monitor: false],
00067  for S in powerset(setn(m),2) do block([p1:first(S), p2:second(S),P],
00068    count:count+1,
00069    if monitor and oklib_monitor_level=0 then printf(true, "~d ", count),
00070    P : create_list(if i=p1 then p2 elseif i=p2 then p1 else i, i,1,m),
00071    t : evalpermasbf(P),
00072    if monitor and oklib_monitor_level >= 1 then print(count, P, t),
00073    L : ev_hm(h,t),
00074    if monitor and L=false then (countf:countf+1, print("NEW:", countf, P, t)),
00075    set_hm(h,t, if L=false then [P] else cons(P,L))
00076  ),
00077  return(h))$
00078 
00079 
00080 /* Output the occurring tuples t together with the number of permutations
00081    belonging to them:
00082 */
00083 ev_ip(h) := block([L : hm2sm(h)],
00084  for p in L do print(first(p), length(second(p))))$
00085