OKlibrary  0.2.1.6
Hypergraphs.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 31.12.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 2010, 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 
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/Basic.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/CombinatorialMatrices/Lisp/Basics.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00030 
00031 
00032 
00033 /* *******************************************
00034    * Clause-variable matrices and variations *
00035    *******************************************
00036 */
00037 
00038 /* A formal clause-set as a hypergraph: */
00039 /* RENAME: fcs2hg */
00040 hyp_fcs(FF) := [literals_v(FF[1]), FF[2]]$
00041 fcs2hg(FF) := hyp_fcs(FF)$
00042 
00043 
00044 /* The clause-variable graph of a formal clause-set (also "incidence graph").
00045    The set of vertices is the disjoint-sum of the clauses ("left") and the
00046    variables ("right").
00047 */
00048 /* RENAME: clvar_fcs2g */
00049 clvar_g(FF) := [set_sumn(FF[2], FF[1]),
00050   family_sets_union(FF[2], 
00051     lambda([C], map(lambda([x],{[C,1],[var_l(x),2]}), C)))]$
00052 clvar_fcs2g(FF) := clvar_g(FF)$
00053 
00054 
00055 /* The variable-hypergraph of a formal clause-set: */
00056 /* RENAME: var_fcs2hg */
00057 var_hyp(FF) := [FF[1], map(var_c,FF[2])]$
00058 var_fcs2hg(FF) := var_hyp(FF)$
00059 var_fcs2ghg(FF) := [FF[1], FF[2], lambda([H],var_c(H))]$
00060 
00061 
00062 /* The variable-interaction graph (or "primal graph") of a formal clause-set: */
00063 /* RENAME vi_fcs2g */
00064 vig_fcs(FF) := section_hyp(var_hyp(FF),2)$
00065 vi_fcs2g(FF) := vig_fcs(FF)$
00066 
00067 
00068 /* The common-variable graph of a clause-set (this is also the
00069    "stochastic-dependence graph"). */
00070 /* RENAME: cv_cs2g */
00071 cvg_cs(F) := [F, 
00072  subset(powerset(F,2), lambda([S], 
00073         block([L : listify(S)], not disjointp(var_c(L[1]), var_c(L[2])))))]$
00074 cv_cs2g(F) := cvg_cs(F)$
00075 
00076 
00077 /* The combinatorial clause-variable matrix of a formal clause-set: */
00078 /* RENAME: clvar_fcs2com */
00079 cl_var_com_fcs(FF) := [FF[2], FF[1], lambda([C,v], 
00080   if elementp(v, C) then +1 else if elementp(-v,C) then -1 else 0)]$
00081 clvar_fcs2com(FF) := cl_var_com_fcs(FF)$
00082 /* Remark: abs_com(clvar_fcs2com(FF)) = hypver_ghg2com(var_fcs2ghg(FF)). */
00083 /* RENAME: clvar_ofcs2ocom */
00084 cl_var_ocom_ofcs(FF) := [FF[2], FF[1], lambda([C,v], 
00085   if elementp(v, C) then +1 else if elementp(-v,C) then -1 else 0)]$
00086 clvar_ofcs2ocom(FF) := cl_var_ocom_ofcs(FF)$
00087 clvar_fcl2ocom(FF) := cl_var_ocom_ofcs(FF)$
00088 
00089 /* The inverse operation, creating a formal clause-set from a
00090    combinatorial matrix, using the columns as variables (positive entries
00091    yield positive literals, negative entries negative literals).
00092    Prerequisite: The columns indices can serve as variables.
00093    The matrix entries are not restricted to {-1,0,+1}, only the
00094    relation "<" must be applicable.
00095 */
00096 clvar_com2fcs(M) := [M[2], 
00097  map(lambda([i], disjoin(0,
00098   map(lambda([j], block([x : M[3](i,j)], 
00099    if x > 0 then j elseif x < 0 then -j else 0)), M[2]))), 
00100  M[1])]$
00101 clvar_ocom2fcl(M) := [M[2],
00102  map(lambda([i], disjoin(0, setify(
00103   map(lambda([j], block([x : M[3](i,j)], 
00104    if x > 0 then j elseif x < 0 then -j else 0)),
00105   M[2])))),
00106  M[1])]$
00107 /* Now taking a Maxima matrix as input: */
00108 clvar_m2fcs(M) := clvar_com2fcs(m2com(M))$
00109 /* If the column-indices can not serve as variables, use the function-argument
00110    make_var to create variables as make_var(j) ("w" in the name is for
00111    wrapper):
00112 */
00113 clvar_w_com2fcs(M,make_var) := [map(make_var,M[2]), 
00114  map(lambda([i], disjoin(0,
00115   map(lambda([j], block([x : M[3](i,j)], 
00116    if x > 0 then make_var(j) elseif x < 0 then -make_var(j) else 0)), M[2]))), 
00117  M[1])]$
00118 clvar_w_ocom2fcl(M,make_var) := [map(make_var,M[2]),
00119  map(lambda([i], disjoin(0, setify(
00120   map(lambda([j], block([x : M[3](i,j)], 
00121    if x > 0 then make_var(j) elseif x < 0 then -make_var(j) else 0)),
00122   M[2])))),
00123  M[1])]$
00124 
00125 
00126 /* The clause-intersection matrix (as square combinatorial matrix)
00127    of a clause-set (for each pair of clauses the number of common literals
00128    minus the number of clashing literals). */
00129 cl_int_scom_cs(F) := block([FF : cs_to_fcs(F), M],
00130  M : cl_var_com_fcs(FF),
00131   return(com2scom(prod_com(M, trans(M)))))$
00132 /* The clause-var-intersection matrix (as square combinatorial matrix)
00133    of a clause-set (for each pair of clauses the number of common variables).
00134 */
00135 cl_varint_scom_cs(F) := block([FF : cs_to_fcs(F), M],
00136  M : abs_com(cl_var_com_fcs(FF)),
00137   return(com2scom(prod_com(M, trans(M)))))$
00138 
00139 
00140 /* The variable-intersection matrix (as square combinatorial matrix)
00141    of a formal clause-set (for each pair of variables the number of 
00142    occurrences with the same sign occurrences minus the number of 
00143    occurrences with opposite signs) */
00144 var_int_scom_fcs(FF) := block([M : cl_var_com_fcs(FF)],
00145   return(com2scom(prod_com(trans(M), M))))$
00146 
00147 
00148 /* The directed variable-literal-clause graph of a formal
00149    clause-set (from a variable to its two literals, from a
00150    literal to its clauses).
00151    Literals are here represented as pairs [v,+1] resp. [v,-1].
00152 */
00153 /* RENAME: varlitcl_fcs2dg */
00154 var_lit_clause_digraph(FF) := block([Var,Lit,Cl,V,E],
00155   Var : listify(FF[1]),
00156   Lit : create_list([v,j], v,Var, j,[-1,1]),
00157   Cl : listify(FF[2]),
00158   V : append(Var,Lit,Cl),
00159   E : append(
00160         create_list([v,[v,j]], v,Var, j,[-1,1]),
00161         create_list([x,C], x,Lit, 
00162           C,sublist(Cl,lambda([D],elementp(x[2]*x[1],D)))
00163         )
00164       ),
00165   return([setify(V),setify(E)]))$
00166 /* The transitive closure of var_lit_clause_digraph. */
00167 /* RENAME: varlitcltr_fcs2dg */
00168 var_lit_clause_digraph_tr(FF) := block(
00169  [G : var_lit_clause_digraph(FF),Var,Cl,E],
00170   Var : listify(FF[1]),
00171   Cl : listify(FF[2]),
00172   E :  create_list([v,C], v,Var, 
00173           C,sublist(Cl,lambda([D],elementp(v,var_c(D))))),
00174   return([G[1],union(G[2],setify(E))]))$
00175 
00176 
00177 /* ***************************************
00178    * Implication graphs (and variations) *
00179    ***************************************
00180 */
00181 
00182 /* The directed implication graph of a formal clause-set (only considering
00183    clauses of length 1 or 2). */
00184 /* RENAME: imp_fcs2dg(FF) */
00185 implication_dg_fcs(FF) := block(
00186  [F1 : map(listify,listify(scls_k(FF[2],1))), 
00187   F2 : map(listify,listify(scls_k(FF[2],2)))],
00188   [literals_v(FF[1]), setify(append(create_list([-U[1],U[1]],U,F1), 
00189       create_list([-C[1],C[2]],C,F2), create_list([-C[2],C[1]],C,F2)))])$
00190 
00191 
00192 /* ************
00193    * Measures *
00194    ************
00195 */
00196 
00197 /* The minimal degree of the common-variable graph: */
00198 min_degree_cvg_cs(F) := if emptyp(F) then inf else
00199   min_degree(g2mg(cvg_cs(F)))[1]$
00200 /* The maximal degree of the common-variable graph */
00201 max_degree_cvg_cs(F) := if emptyp(F) then minf else
00202   max_degree(g2mg(cvg_cs(F)))[1]$
00203 
00204 
00205 /* The deficiency of a formal clause-set: */
00206 deficiency_fcs(FF) := length(FF[2]) - length(FF[1])$
00207 /* The deficiency of a clause-set */
00208 deficiency_cs(F) := deficiency_fcs(cs2fcs(F))$
00209 
00210 /* The maximal deficiency of a formal clause-set: */
00211 max_deficiency_fcs(FF) := length(FF[2]) - length(max_matching(g2mg(clvar_g(FF))))$
00212 
00213 /* The surplus of a formal clause-set, computed by definition: */
00214 surplus_bydef_fcs(FF) := if emptyp(FF[1]) then 0 else
00215   lmin(map(lambda([V], length(scs_V(FF[2],V)) - length(V)), disjoin({},powerset(FF[1]))))$
00216 surplus_bydef_cs(F) := surplus_bydef_fcs(cs2fcs(F))$
00217 
00218 
00219 /* ************
00220    * Analysis *
00221    ************
00222 */
00223 
00224 var_disjointfcsp(FF1,FF2) := disjointp(FF1[1],FF2[1])$
00225 var_disjointcsp(F1,F2) := var_disjointfcsp(cs_to_fcs(F1),cs_to_fcs(F2))$
00226 
00227 /* The set of accumulation variables of a clause-set (those variables which
00228    after splitting create variable-disjoint clause-sets). */
00229 accumulation_variables_cs(F) := block([V : var_cs(F), result : {}],
00230   for v in V do 
00231     if var_disjointcsp(apply_pa({v},F), apply_pa({-v},F)) then
00232       result : adjoin(v,result),
00233   return(result))$
00234 
00235 /* The set of full variables (occurring in every clause) of a
00236    formal clause-set. */
00237 full_variables_fcs(FF) := block([F : FF[2], D, c : ncl_f(FF)],
00238  if F = {} then return(FF[1]) elseif F = {{}} then return({}),
00239  D : hm2sm(variable_degrees_cs(F)),
00240  return(map(lambda([P],first(P)),subset(D, lambda([P], is(second(P)=c))))))$
00241 full_variables_cs(F) := full_variables_fcs(cs_to_fcs(F))$
00242