OKlibrary  0.2.1.6
Symmetries.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 30.4.2008 (Guangzhou) */
00002 /* Copyright 2008, 2009 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/Graphs/Lisp/Basic.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/CombinatorialMatrices/Lisp/Isomorphisms.mac")$
00029 
00030 
00031 /* ****************************************
00032    * Isomorphism testing via backtracking *
00033    ****************************************
00034 */
00035 
00036 /* Checks whether two clause-sets are isomorphic (where renaming
00037    of variables and flipping is considered), by using a direct backtracking 
00038    approach:
00039 */
00040 is_isomorphic_btr_cs(F1,F2) :=
00041  is_isomorphic_btr_fcs(cs_to_fcs(F1), cs_to_fcs(F2))$
00042 /* Checks whether two formal clause-sets are isomorphic: */
00043 is_isomorphic_btr_fcs(FF1,FF2) := block(
00044  if elementp({},FF1[2]) then (
00045    if not elementp({},FF2[2]) then return(false))
00046  elseif elementp({},FF2[2]) then return(false),
00047  block(
00048  [V1o : var_cs(FF1[2]), V2o : var_cs(FF2[2]),
00049   F1r, F2r, n, V, F1, F2, degl1, degl2, map_poss : []],
00050   if nvar_f(FF1) # nvar_f(FF2) then return(false),
00051   if length(V1o) # length(V2o) then return(false),
00052   n : length(V1o), V : setn(n),
00053   if emptyp(V) then return(true),
00054   F1r : standardise_fcs([V1o,FF1[2]]),
00055   F2r : standardise_fcs([V2o,FF2[2]]),
00056   F1 : disjoin({},F1r[1][2]), F2 : disjoin({},F2r[1][2]),
00057   degl1 : all_literal_degrees_fcs([V,F1]),
00058   degl2 : all_literal_degrees_fcs([V,F2]),
00059   block([deg_pairs : sm2hm({})],
00060     for v in V do block([deg : [ev_hm(degl2,v), ev_hm(degl2,-v)]],
00061       if deg[1] = deg[2] then
00062         set_hm(deg_pairs, deg, union({v,-v}, ev_hm_d(deg_pairs, deg, {})))
00063       else (
00064         set_hm(deg_pairs, deg, adjoin(v, ev_hm_d(deg_pairs, deg, {}))),
00065         set_hm(deg_pairs, reverse(deg), adjoin(-v, ev_hm_d(deg_pairs, reverse(deg), {}))))
00066     ),
00067     for v in V do block([deg : [ev_hm(degl1,v), ev_hm(degl1,-v)]],
00068       map_poss : endcons([v,ev_hm_d(deg_pairs, deg, {})], map_poss))
00069   ),
00070   map_poss : sort(map_poss, lambda([p1,p2], is(length(p1[2]) < length(p2[2])))),
00071   is_isomorphic_btr_piso(sm2hm({}), {}, map_poss, F1)))$
00072 
00073 /* Additional a partial isomorphism as a hash-map from variables
00074    to literals is given, with its domain, the map of possibilities
00075    for mapping remaining variables (sorted by ascending sets
00076    of possibilities), and the set of remaining clauses from F1 to
00077    be mapped to clauses in F1.
00078    Prerequisite: map_possibilities, rem_clauses are not empty.
00079    Inherits F1, F2.
00080 */
00081 is_isomorphic_btr_piso(part_iso,domain_piso,map_possibilities,rem_clauses) := block(
00082  [B : first(map_possibilities), v, Y, found_iso : false],
00083   v : B[1], Y : B[2],
00084   domain_piso : adjoin(v,domain_piso),
00085   for y in Y unless found_iso do block(
00086    [inconsistent : false, to_be_removed : {}],
00087     set_hm(part_iso,v,y),
00088     for C in rem_clauses unless inconsistent do (
00089       if subsetp(var_c(C), domain_piso) then
00090         if not elementp(substitute_c(C,part_iso), F2) then
00091           inconsistent : true
00092         else
00093           to_be_removed : adjoin(C,to_be_removed)
00094     ),
00095     if not inconsistent then block(
00096      [new_rem_clauses : setdifference(rem_clauses, to_be_removed),
00097       new_map_possibilities : copylist(rest(map_possibilities))],
00098       if emptyp(new_rem_clauses) then found_iso : true else (
00099         for i : 1 thru length(new_map_possibilities) do block(
00100          [P : new_map_possibilities[i]],
00101           new_map_possibilities[i] : [P[1], setdifference(P[2],{y,-y})]),
00102         new_map_possibilities : sort(new_map_possibilities,
00103           lambda([p1,p2], is(length(p1[2]) < length(p2[2])))),
00104         if is_isomorphic_btr_piso(
00105           part_iso,domain_piso,new_map_possibilities,new_rem_clauses)
00106         then found_iso : true
00107       )
00108     )
00109   ),
00110   del_hm(part_iso,v),
00111   return(found_iso))$    
00112 
00113 
00114 /* **********************************************
00115    * Isomorphism testing via graph isomorphisms *
00116    **********************************************
00117 */
00118 
00119 /* Checks whether two formal clause-sets are isomorphic (where renaming
00120    of variables and flipping is considered), by using the 
00121    digraph-isomorphism-check from the Maxima graphs-package:
00122 */
00123 is_isomorphic_fcs(FF1,FF2) :=
00124  if ncl_list_fcs(FF1) # ncl_list_fcs(FF2) then false
00125  elseif variable_degrees_list_cs(FF1[2]) # variable_degrees_list_cs(FF2[2]) then false
00126  elseif literal_degrees_list_fcs(FF1) # literal_degrees_list_fcs(FF2) then false
00127  else is_isomorphic(
00128    dg2mdg(var_lit_clause_digraph_tr(FF1)),
00129    dg2mdg(var_lit_clause_digraph_tr(FF2)))$
00130 /* The variation for clause-sets as inputs */
00131 is_isomorphic_cs(F1,F2) := is_isomorphic_fcs(cs_to_fcs(F1),cs_to_fcs(F2))$
00132 /* In case one FF1 is compared with many FF2, store the data for FF1. */
00133 prepare_iso_fcs(FF1, storage_var) := (
00134   storage_var :: [
00135     ncl_list_fcs(FF1),
00136     variable_degrees_list_cs(FF1[2]),
00137     literal_degrees_list_fcs(FF1),
00138     dg2mdg(var_lit_clause_digraph_tr(FF1))])$
00139 is_isomorphic_prep_fcs(FF2, storage_var) := block(
00140  [store : ev(storage_var)],
00141   if store[1] # ncl_list_fcs(FF2) then false
00142   elseif store[2] # variable_degrees_list_cs(FF2[2]) then false
00143   elseif store[3] # literal_degrees_list_fcs(FF2) then false
00144   else is_isomorphic(
00145     store[4],
00146     dg2mdg(var_lit_clause_digraph_tr(FF2))))$
00147 
00148 
00149 /* **********************************************
00150    * Isomorphism testing via matrix isomorphism *
00151    **********************************************
00152 */
00153 
00154 is_varisomorphic_com_fcs_p(FF1,FF2) :=
00155   is_isomorphic_rowpermall_com_p(cl_var_com_fcs(FF1), cl_var_com_fcs(FF2))$
00156 
00157 
00158 /* **********************************
00159    * Isomorphism classes management *
00160    **********************************
00161 */
00162 
00163 /* For a set of formal clause-sets, determines a subset of non-isomorphic
00164    representatives: */
00165 representatives_fcs(SFF) := block([classes : equiv_classes(SFF, is_isomorphic_btr_fcs)],
00166   return(map(choose_element, classes)))$
00167 /* The variation for a set of clause-sets: */
00168 representatives_cs(SF) := block([classes : equiv_classes(SF, is_isomorphic_btr_cs)],
00169   return(map(choose_element, classes)))$
00170 
00171 /* A "hash-repository of isomorphism types" is a hash-map using the
00172    value of "fcs_identifier" as key, and with a set of pairwise
00173    non-isomorphic formal clause-sets as value. */
00174 
00175 fcs_identifier(FF) := [nvar_f(FF), ncl_fcs(FF), literal_degrees_list_fcs(FF), ncl_list_fcs(FF)]$
00176 
00177 /* Given a hash_repository repo of isomormphism types, check whether a
00178    given formal clause-set is already contained or not, and in the latter
00179    case insert it into the repository.
00180    Returns true iff FF has been inserted.
00181    repo is a hash-map of isomorphism types.
00182 */
00183 manage_repository_isomorphism_types(FF, repo) := block(
00184  [p : fcs_identifier(FF), candidates],
00185   candidates : ev_hm(repo,p),
00186   if candidates = false then (
00187     set_hm(repo,p,{FF}), return(true))
00188   else block([found : false],
00189     for GG in candidates unless found do
00190       if is_isomorphic_btr_fcs(FF,GG) then found : true,
00191     if found then return(false) else (
00192       set_hm(repo,p,adjoin(FF,candidates)),
00193       return(true))))$
00194 
00195 
00196 /* *******************************
00197    * Analysing hash-repositories *
00198    *******************************
00199 */
00200 
00201 /* Compute the sorted list of pairs [deficiency, count] for a given
00202    hash-repository:
00203 */
00204 analyse_isorepo_def(repository) := block(
00205  [M : hm2sm(repository), h : sm2hm({})],
00206   for P in M do block([count : length(P[2]), def : P[1][2] - P[1][1]],
00207     set_hm(h,def,ev_hm_d(h,def,0)+count)),
00208   sort(listify(hm2sm(h)),lambda([P1,P2], is(P1[1] < P2[1]))))$
00209 /* Returns the set of all clause-sets in the repository. */
00210 analyse_isorepo_set(repository) :=
00211  family_sets_union(map(second,hm2sm(repository)),
00212                    lambda([S],map(fcs2cs,S)))$
00213 /* Returns the sorted list [deficiency, set of clause-sets]: */
00214 analyse_isorepo_defset(repository) := block(
00215  [M : hm2sm(repository), h : sm2hm({})],
00216   for P in M do block([def : P[1][2] - P[1][1]],
00217     set_hm(h,def,union(ev_hm_d(h,def,{}), map(fcs2cs,P[2])))),
00218   sort(listify(hm2sm(h)),lambda([P1,P2], is(P1[1] < P2[1]))))$
00219 
00220