OKlibrary  0.2.1.6
Constructions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 23.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012, 2013 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/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00027 
00028 
00029 /* **********************
00030    * Logical operations *
00031    **********************
00032 */
00033 
00034 /* The expansion of a single clause into an equivalent full fcl w.r.t.
00035    a given list of variables.
00036    Prerequisite: var(C) and V are disjoint.
00037 */
00038 c2cl_expand(C,V) := add_elements_l(C,all_tass_l(V))$
00039 /* The same, but where V is a set of variables, and a set is returned: */
00040 c2cs_expand(C,V) := setify(add_elements_l(C,all_tass_l(listify(V))))$
00041 /* Expanding a clause-set F into an equivalent full clause-set: */
00042 expand_fcs(FF) := block([V : FF[1]],
00043 [FF[1], lunion(create_list(c2cs_expand(C,setdifference(V,var_c(C))),C,listify(FF[2])))])$
00044 expand_cs(F) := fcs2cs(expand_fcs(cs2fcs(F)))$
00045 
00046 
00047 /* The natural representation of the "and" of two clause-sets as cnf's
00048    (as n-ary operation): */
00049 and_cs([L]) := apply(union,L)$
00050 
00051 
00052 /* All non-clashing unions of the clauses of two given clause-sets, which
00053    represents the "or" of the clause-sets as cnf's. */
00054 or_cs2(F1,F2) :=
00055  map(lunion,
00056   subset(cartesian_product(F1,F2), lambda([P],not clashp(P[1],P[2]))))$
00057 /* As n-ary operation: */
00058 or_cs([L]) := block([l : length(L)],
00059  if l = 0 then {{}} elseif l = 1 then L[1]
00060  else apply(or_cs, cons(or_cs2(L[1],L[2]), rest(L,2))))$
00061 
00062 
00063 /* The natural DNF-representation of a clause-set F as CNF: */
00064 dual_cs(F) := apply(or_cs,
00065  map(lambda([C],map(set,C)), listify(F)))$
00066 /* Subsumption elimination applied to the result yields the set of
00067    all prime implicants (all minimal satisfying partial assignments).
00068 */
00069 
00070 /* Complementation (literal-wise) of a clause-set or clause-list: */
00071 comp_cs(F) := map(comp_sl, F)$
00072 comp_cl(F) := map(comp_sl, F)$
00073 comp_fcs(FF) := [FF[1], comp_cs(FF[2])]$
00074 /* Remark: comp_cs(F) is the negation of F via de Morgan, that is,
00075    if F is regarded as CNF, then comp_cs(F) as DNF is equivalent to the
00076    negation of F (and vice versa).
00077 */
00078 
00079 /* The natural negation of a clause-set: */
00080 neg_cs(F) := dual_cs(comp_cs(F))$
00081 /* Remark: In contrast to comp_cs(F), here now for a CNF F the clause-set
00082    neg_cs(F) as CNF is equivalent to the negation of F.
00083 */
00084 
00085 
00086 /* ****************************
00087    * Combinatorial operations *
00088    ****************************
00089 */
00090 
00091 /* Given a list of formal clause-sets, make them variable-disjoint
00092    by standardising the variable-sets to 1,2,..., and then take
00093    the union of them: */
00094 vardisjoint_sum_fcs([LFF]) := block([VD : make_vardisjoint_fcs(LFF)],
00095  [setn(VD[2]), lunion(map(clauses_f,VD[1]))])$
00096 
00097 /* Make formal clause-sets FF1, FF2 var-disjoint in the standard
00098    way, and if we have then n variables together, add the new
00099    variable n+1 positively to all clauses in FF1', negatively to all
00100    in FF2', and take the union. */
00101 vardisjoint_full_gluing(FF1,FF2) := block(
00102  [vd : make_vardisjoint_fcs([FF1, FF2]), GG1,GG2, n],
00103   [GG1,GG2] : vd[1], n : vd[2],
00104   return([if FF1[2] = {} and FF2[2] = {} then {} else setn(n+1),
00105           union(add_element(n+1,GG1[2]), add_element(-(n+1),GG2[2]))]))$
00106 
00107 /* Full gluing, keeping the old variables, but standardising them: */
00108 full_gluing(FF1,FF2) := block(
00109  [V : listify(union(FF1[1],FF2[1])), n, h, F1, F2],
00110   n : length(V),
00111   h : osm2hm(map("[", V, create_list(i,i,1,n))),
00112   F1 : substitute_cs(FF1[2],h),
00113   F2 : substitute_cs(FF2[2],h),
00114   return([setn(n+1), union(add_element(n+1,F1),
00115                            add_element(-(n+1),F2))]))$
00116 
00117 /* Partial gluing, standardising the variables: */
00118 /* S1 is a non-empty subset of FF1[2], S2 is a non-empty subset
00119    of FF2[2]. */
00120 partial_gluing(FF1,S1,FF2,S2) := block(
00121  [V : listify(union(FF1[1],FF2[1])), n, h, F1, F2],
00122   n : length(V),
00123   h : osm2hm(map("[", V, create_list(i,i,1,n))),
00124   F1 : setdifference(FF1[2],S1),
00125   F2 : setdifference(FF2[2],S2),
00126   F1 : substitute_cs(F1,h),
00127   F2 : substitute_cs(F2,h),
00128   S1 : substitute_cs(S1,h),
00129   S2 : substitute_cs(S2,h),
00130   return([setn(n+1), union(add_element(n+1,S1),
00131                            add_element(-(n+1),S2),
00132                            F1, F2)]))$
00133 
00134 /* For clause-sets F, G and an element C of F the "twisting of F and G on C"
00135    is the union of F minus C and G with C added to every clause:
00136 */
00137 twisting_cs(F,C,G) := union(disjoin(C,F), or_cs2({C},G))$
00138 /* Now making F, G variable-disjoint before twisting, using standardised
00139    variables 1, ..., n(F)+n(G), first variables of F, then of G: */
00140 twisting_var_disjoint_cs(F,C,G) := block(
00141  [D : make_vardisjoint_vl_fcs([cs2fcs(F), cs2fcs(G)]), V],
00142   F : D[1][1][2], G : D[1][2][2],
00143   V : D[3][1],
00144   C : substitute_c(C, osm2hm(map("[", V, create_list(i,i,1,length(V))))),
00145   twisting_cs(F,C,G))$
00146 
00147