OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 17.1.2011 (Swansea) */
00002 /* Copyright 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/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00028 
00029 
00030 /* *******************
00031    * Boolean vectors *
00032    *******************
00033 */
00034 
00035 /*
00036   A "boolean value" is either 0 or 1.
00037 */
00038 
00039 boolval_p(v) := is(v=0) or is(v=1)$
00040 
00041 /* Translating Maxima-truth-values into boolean values: */
00042 tv2boolval(t) := if t then 1 else 0$
00043 
00044 /*
00045   A "boolean vector" ("bv") of length k (k in NN_0) is a list v of length k
00046   with entries 0, 1.
00047 */
00048 
00049 bv_p(v) := listp(v) and every_s(boolval_p,v)$
00050 
00051 /* The set of all boolean vectors of length k: */
00052 all_bv(k) := apply(cartesian_product, create_list({0,1},i,1,k))$
00053 
00054 /* The 2^k boolean vectors of length k in lexicographical order: */
00055 lex_bv_l(k) := cartesian_product_l(create_list([0,1],i,1,k))$
00056 /* Unranking for 1 <= i <= 2^k: */
00057 unrank_lex_bv(i,k) := if k=0 then [] else int2polyadic_padd(i-1,2,k)$
00058 /* Ranking of boolean vectors: */
00059 rank_lex_bv(x) := polyadic2int(x,2) + 1$
00060 
00061 
00062 /* Translating boolean vectors into (standardised) DNF-clauses (using the
00063    positions as variables):
00064 */
00065 bv2c(v) := bv2c_wv(v,create_list(i,i,1,length(v)))$
00066 /* More generally, supplying a vector V of boolean variables (of the same
00067    length as v):
00068 */
00069 bv2c_wv(v,V) := setify((2*v - 1) * V)$
00070 
00071 /* Translating boolean vectors into hyperedges consisting of the indices
00072    of the position where the vector is true:
00073 */
00074 bv2he(v) := setify(sublist_indices(v,lambda([x],x=1)))$
00075 
00076 
00077 /* *********************
00078    * Boolean functions *
00079    *********************
00080 */
00081 
00082 /*
00083   A "boolean function" ("bf") is a function with the following properties:
00084 
00085    - implicitly a size-domain S <= NN_0 is given
00086    - for every n in S there is an m_n in NN_0 such that for all boolean vectors
00087      x of length n the term f(x) is a boolean vector of length m_m.
00088 
00089   f is an "n x m bf" if n in S and m_n = m.
00090 */
00091 
00092 /* Testing whether f is a n x m boolean function: */
00093 bf_nm_p(f,n,m) :=
00094  every_s(lambda([x], 
00095            block([y:f(x)], listp(y) and is(length(y)=m) and bv_p(y))),
00096          all_bv(n))$
00097 
00098 
00099 /* ********************************
00100    * Some basic boolean functions *
00101    ********************************
00102 */
00103 
00104 /* Functions with size-domain NN_0 and m=1: */
00105 
00106 zero_bf : lambda([x], [0])$
00107 one_bf : lambda([x], [1])$
00108 
00109 and_bf : lambda([x], [lmin(x)])$
00110 or_bf : lambda([x], [lmax(x)])$
00111 
00112 xor_bf : lambda([x], [mod(apply("+", x),2)])$
00113 
00114 /* Functions with size-domain NN_0 and m=n: */
00115 
00116 id_bf : identity$
00117 neg_bf : lambda([x], 1-x)$
00118 
00119 /* Integer representations: */
00120 
00121 and_ibo(x,y):=?boole(?boole\-and,x,y)$
00122 or_ibo(x,y):=?boole(?boole\-ior,x,y)$
00123 xor_ibo(x,y):=?boole(?boole\-xor,x,y)$
00124 /* These functions are also in the Maxima-package "functs" (however with
00125    defective definitions), with names "logand, logor, logxor".
00126    "ibo" for "integer boolean operation".
00127 */
00128 
00129 
00130 /* ***************
00131    * Conversions *
00132    ***************
00133 */
00134 
00135 /* The "bit-vector presentation" of an n x 1 boolean function f is the boolean
00136    vector of length 2^n containing all values of f, applied to the 
00137    lexicographical ordering of inputs:
00138 */
00139 bf2bv(f_, n) := map(lambda([x], first(f_(x))), lex_bv_l(n))$
00140 bv2bf(fv) := buildq([a : il2ary(fv)], lambda([x], [a[rank_lex_bv(x)]]))$
00141 
00142 /* Boolean functions as full DNF resp. DNF (the clause-order follows the
00143    lexicographical order of the boolean vectors):
00144 */
00145 bf2fulldnf_fcl(f,n) := [create_list(i,i,1,n), map(bv2c, sublist(lex_bv_l(n), lambda([x],is(f(x)=[1]))))]$
00146 bf2fullcnf_fcl(f,n) := [create_list(i,i,1,n), map(bv2c, 1 - sublist(lex_bv_l(n), lambda([x],is(f(x)=[0]))))]$
00147 /* Converting a boolean function as full DNF into into a boolean function: */
00148 fulldnf2bf_cs(F) := buildq([F], lambda([x], tv2boolval(elementp(bv2c(x),F))))$
00149 
00150 
00151 /* The "DNF hypergraph representation" of an n x 1 boolean function f
00152    is obtained from its full DNF by taking the variable as vertices and
00153    converting the clauses into hyperedges by removing the negative literals.
00154 */
00155 /* Converting a boolean function given as a full DNF into its DNF hypergraph
00156    representation:
00157 */
00158 fulldnf2dnfhg_ofcs2ohg(FF) :=
00159  [ FF[1], map(lambda([C],subset(C,lambda([x],is(x>0)))), FF[2]) ]$
00160 /* Translating a boolean function as set-system into a boolean function: */
00161 dnfhg2bf_ses(S) := buildq([S], lambda([x], tv2boolval(elementp(bv2he(x), S))))$
00162 
00163 
00164 /* *****************
00165    * Constructions *
00166    *****************
00167 */
00168 
00169 /* The component-wise negation of a boolean function: */
00170 negation_bf(f) := buildq([f], lambda([x],1-f(x)))$
00171 
00172 /* The composition of boolean functions (first f, then g): */
00173 composition_bf(g,f) := buildq([f,g], lambda([x], g(f(x))))$
00174 square_bf(f) := composition_bf(f,f)$
00175 
00176 /* A boolean n x m function f as a boolean (n+m) x 1 function: */
00177 bf2relation_bf(f,n) := buildq([f,n], lambda([x], tv2boolval(is(f(take_l(n,x))=rest(x,n)))))$
00178 bf2relation_fulldnf_cl(f,n) :=
00179  map(bv2c, map(lambda([x],append(x,f(x))), lex_bv_l(n)))$
00180 bf2relation_fullcnf_fcs(f,n) := block(
00181  [F : map(comp_sl,bf2relation_fulldnf_cl(f,n))],
00182   if emptyp(F) then [{},{{}}]
00183   else block([N : length(first(F))],
00184     [setn(N), setdifference(full_cs(N), setify(F))]))$
00185 
00186 /* The boolean n x 1 function giving the i-th output bit of the boolean n x m
00187    function f: */
00188 bfnm2n1(f,i) := buildq([f,n,i], lambda([x], [f(x)[i]]))$
00189