OKlibrary  0.2.1.6
ClauseSets.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 19.8.2010 (Swansea) */
00002 /* Copyright 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 
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Categories/LiteralStructures.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00026 
00027 
00028 /*
00029   The "category of boolean clause-sets" has
00030 
00031    - objects [L,F], where L is a boolean literal structure, and F is a set
00032      of (finite) subsets of L;
00033    - morphisms f: [L,F] -> [L',F'] are literal structure morphisms
00034      f: L -> L' such that for all C in F we have f(C) in F'.
00035 
00036   Abbreviations for the objects: "flcls" ("f" like "formal", "l" like
00037   "literal").
00038 */
00039 
00040 /* Checking whether F is an flcls: */
00041 flcls_p(F) := listp(F) and is(length(F)=2) and
00042   blitstr_p(first(F)) and
00043   setp(second(F)) and
00044   every_s(lambda([C], subsetp(C,first(first(F)))), second(F))$
00045 
00046 /* Checking whether the flcls's F1, F2 are equal: */
00047 flcls_equalp(F1,F2) := blitstr_equalp(first(F1), first(F2)) and
00048  is(second(F1) = second(F2))$
00049 
00050 /* Checking whether f is an flcls-morphism from F1 to F2: */
00051 morphism_flcls_p(f,F1,F2) :=
00052   morphism_blitstr_p(f,first(F1),first(F2)) and
00053   every_s(lambda([C], elementp(map(f,C),second(F2))), second(F1))$
00054 
00055 /* Checking whether the flcls F has self-complementary literals: */
00056 has_scl_flcls_p(F) := has_scl_blitstr_p(first(F))$
00057 
00058 
00059 /* *****************
00060    * Constructions *
00061    *****************
00062 */
00063 
00064 /* The (unique) initial object (the empty flcls): */
00065 initial_flcls : [initial_blitstr, {}]$
00066 
00067 /* The terminal object, based on the terminal literal-structure (which has
00068    [] as the single literal, and all possible clauses):
00069 */
00070 terminal_flcls : [terminal_blitstr, {{},{[]}}]$
00071 
00072 /* The free flcls over literal-structure L (no clauses): */
00073 free_flcls(L) := [L,{}]$
00074 
00075 /* The cofree flcls over literal-structure L (all possible clauses): */
00076 cofree_flcls(L) := [L,powerset(first(L))]$
00077 
00078 /* The product-flcls of the list FL of flcls's: */
00079 product_flcls(FL) := block([
00080  L : product_blitstr(map(first,FL)),
00081  P : uaapply(cartesian_product, map(second,FL))],
00082   [L, 
00083    lunion(map(
00084            lambda([CL],
00085              subset(powerset(uaapply(cartesian_product,CL)),
00086                     lambda([C], 
00087                       every_s(
00088                        lambda([i],
00089                         elementp(map(projection_product_blitstr(i),C),
00090                                  second(FL[i]))),
00091                        create_list(i,i,1,length(FL))
00092                       )
00093                     )
00094                    )
00095                  ),
00096            P))])$
00097 /* The projections belonging to component i: */
00098 projection_product_flcls(i) := projection_product_blitstr(i)$
00099 
00100 
00101 /* ****************
00102    * Translations *
00103    ****************
00104 */
00105 
00106 /* Converting a flcls to a boolean formal clause-set, by translating the
00107    literals from F in their natural order into boolean literals, taking
00108    the first occurrence of a complementary pair as the variable.
00109    Prerequisite: F has no selfcomplementary literals, and
00110    the term "und" is not a literal.
00111 */
00112 flcls2fcls(F) := block([h : sm2hm({}), n : 0],
00113   for x in first(first(F)) do
00114     if ev_hm_d(h,x,und) = und then (
00115       n : n + 1,
00116       set_hm(h,x,n), set_hm(h,second(first(F))(x),-n)
00117     ),
00118   [setn(n), map(lambda([C], map(lambda([x], ev_hm(h,x)), C)), second(F))])$
00119 
00120 /* Converting a boolean formal clause-set to a flcls: */
00121 fcls2flcls(F) := [sl2blitstr(first(F)), second(F)]$
00122 
00123 /* Converting a flcls to a hypergraph, by forgetting the complementation
00124    and using the literals as vertices:
00125 */
00126 flcls2hg(F) := [first(first(F)),second(F)]$
00127