OKlibrary  0.2.1.6
Codes.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 29.10.2009 (Swansea) */
00002 /* Copyright 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/Satisfiability/Lisp/PseudoBoolean/CardinalityConstraints.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 
00025 
00026 /* ******************
00027    * Covering codes *
00028    ******************
00029 */
00030 
00031 /* Given the alphabet-size q, the length n of code-words, and the envisaged
00032    radius R (all natural numbers), determine the minimum size M of a subset
00033    C of {1,...,q}^n (a code) such that every word from {1,...,q}^n has
00034    Hamming-distance to an element of C at most R.
00035 */
00036 
00037 /* According to Jan-Christoph Schlage-Puchta the code C is encoded as
00038    an nxq-matrix A with entries subsets of {1,...,M} such that every
00039    row is a partition of {1,...,M}:
00040    A(i,j) is the set of indices of codewords c with c_i=j.
00041    An arbitrary element t of {1,...,q}^n is a map from {1,...,n}
00042    to {1,...,q}, that is, for every row i we select a column t(i)
00043    of A. The Hamming distance of code-word k in {1,...,M} to t
00044    is n - m, where m is the number of i in {1,...,n} such that
00045    k is in A(i,t(i)) (these indices i are the indices where
00046    code-word c_k is equal to w).
00047 
00048    The solutions of the problems created below are the code words which
00049    have a distance greater than R to all code-words.
00050 
00051    This is a QBF SAT-problem, where the "code variables" below are universal
00052    variables, while the "word variables" and the "coincidence variables"
00053    are existential variables: If the problem is satisfiable, then no covering
00054    code exists for the given parameters, while if it is unsatisfiable, then
00055    a covering code was found.
00056 */
00057 
00058 
00059 /* "Code variables", where cdv(i,j,k) means that part j of the
00060     partition of {1,...,M} represented by row i contains k, that is,
00061     element k of the code has in component i the value j.
00062 */
00063 kill(cdv)$
00064 declare(cdv, noun)$
00065 declare(cdv, posfun)$
00066 cdv_var(i,j,k) := nounify(cdv)(i,j,k)$
00067 
00068 /* "Word variables", where wrv(i,j) means that the word w
00069    selects value j in row i:
00070 */
00071 kill(wrv)$
00072 declare(wrv, noun)$
00073 declare(wrv, posfun)$
00074 wrv_var(i,j) := nounify(wrv)(i,j)$
00075 
00076 /* "Coincidence variables", where civ(i,k) means that the transversal
00077    coincides in row i with the element k of the code:
00078 */
00079 kill(civ)$
00080 declare(civ, noun)$
00081 declare(civ, posfun)$
00082 civ_var(i,k) := nounify(civ)(i,k)$
00083 
00084 
00085 /* The list of cardinality constraints involved: */
00086 coveringcode_fcrdl(q,n,R,M) := [
00087  append(create_list(cdv_var(i,j,k), i,1,n, j,1,q, k,1,M),
00088         create_list(wrv_var(i,j), i,1,n, j,1,q),
00089         create_list(civ_var(i,k), i,1,n, k,1,M)),
00090  append(create_list([1,create_list(cdv_var(i,j,k), j,1,q),1], i,1,n, k,1,M),
00091         create_list([1,create_list(wrv_var(i,j), j,1,q),1], i,1,n),
00092         create_list([0,create_list(civ_var(i,k), i,1,n),n-R-1], k,1,M))]$
00093 
00094 /* The clauses involved, in the "weak" form (only the necessary direction), 
00095    that is, the implication that if code-word k has in component i the
00096    value j and the select word t has the same value at that position,
00097    then the counting-variable is true:
00098 */
00099 coveringcode_cl(q,n,R,M) := 
00100  create_list({-cdv_var(i,j,k), -wrv_var(i,j), civ_var(i,k)}, i,1,q, j,1,n, k,1,M)$
00101 
00102 /* The complete representation, as a formal combination of clause-list and
00103    cardinality-constraint list:
00104 */
00105 coveringcode_fccrdl(q,n,R,M) := block(
00106  [F : coveringcode_fcrdl(q,n,R,M)],
00107   [F[1], coveringcode_cl(q,n,R,M), F[2]])$
00108 
00109 /* Translated into a boolean formal clause-list, using the direct
00110    translation:
00111 */
00112 coveringcode_fcl(q,n,R,M) := direct_fccrdl2fcl(coveringcode_fccrdl(q,n,R,M))$
00113 
00114 
00115 /* Quick hack for the output (not explicitly renaming the variables): */
00116 output_coveringcode(q,n,R,M,filename) := block([FF : standardise_fcl(coveringcode_fcl(q,n,R,M))],
00117   output_fcl_v(
00118     sconcat("The existence of a covering code of alphabet size ", q, ", length ", n, ", radius ", R, " and with M = ", M, "."), 
00119     FF[1],
00120     filename,
00121     FF[2]))$
00122 
00123 output_coveringcode_stdname(q,n,R,M) := output_coveringcode(q,n,R,M,
00124   sconcat("CoveringCode_",q,"-",n,"-",R,"_",M,".cnf"))$
00125