OKlibrary  0.2.1.6
LatinSquares.mac
Go to the documentation of this file.
00001 /* Matthew Henderson, 1.10.2008 (Berea) */
00002 /* Copyright 2008, 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/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00025 
00026 
00027 /* *****************************************
00028    * Latin square problems as SAT problems *
00029    *****************************************
00030 */
00031 
00032 /* Variables are "ls(i,j,k)", meaning that field (i,j) carries number k: */
00033 kill(ls)$
00034 declare(ls, noun)$
00035 declare(ls, posfun)$
00036 ls_var(i,j,k) := nounify(ls)(i,j,k)$
00037 
00038 /* The set of variables for latin square formulas of dimension p: */
00039 var_ls(p) := block([N : p],
00040  setify(create_list(ls_var(i,j,k), i,1,N, j,1,N, k,1,N)))$
00041 
00042 /* In the following p denotes the dimension. */
00043 
00044 /* Different numbers in each row: */
00045 ls_different_rows(p) := block([N : p],
00046  setify(create_list({- ls_var(i,j1,k), - ls_var(i,j2,k)}, i,1,N, k,1,N, j1,1,N-1, j2,j1+1,N)))$
00047 
00048 /* Different numbers in each column: */
00049 ls_different_columns(p) := block([N : p],
00050  setify(create_list({- ls_var(i1,j,k), - ls_var(i2,j,k)}, j,1,N, k,1,N, i1,1,N-1, i2,i1+1,N)))$
00051 
00052 
00053 /* Given box coordinates 1 <= i,j <= p, the list of coordinates of fields: */
00054 ls_positions_box(i,j,p) := block(
00055  [row_offset : p * (i-1), column_offset : p * (j-1)],
00056  create_list([row_offset + r, column_offset + c], r,1,p, c,1,p))$
00057 
00058 /* Every field carries a number: */
00059 ls_all_fields(p) := block([N : p],
00060  setify(create_list(setify(create_list(ls_var(i,j,k), k,1,N)), i,1,N, j,1,N)))$
00061 
00062 /* The latin square problem (weak form) as formal clause-set: */
00063 weak_ls(p) := [var_ls(p), 
00064  union(ls_different_rows(p), ls_different_columns(p), ls_all_fields(p))]$
00065 
00066 output_weak_ls(p,filename) := block([FF : standardise_fcs(weak_ls(p))],
00067   output_fcs_v(
00068     sconcat("The Latin square problem (weak form) with dimension ", p, "."), 
00069     FF[1],
00070     filename,
00071     FF[2]))$
00072 
00073 /* Every row contains all numbers: */
00074 ls_all_rows(p) := block([N : p],
00075  setify(create_list(setify(create_list(ls_var(i,j,k),j,1,N)), i,1,N, k,1,N)))$
00076 
00077 /* Every column contains all numbers: */
00078 ls_all_columns(p) := block([N : p],
00079  setify(create_list(setify(create_list(ls_var(i,j,k),i,1,N)), j,1,N, k,1,N)))$
00080 
00081 /* Every field carries a different number: */
00082 ls_different_fields(p) := block([N : p],
00083   setify(create_list({-ls_var(i,j,k1), -ls_var(i,j,k2)}, i,1,N, j,1,N, k1,1,N-1, k2,k1+1,N)))$
00084 
00085 /* The latin square problem (dual weak form) as formal clause-set: */
00086 dual_weak_ls(p) := [var_ls(p), 
00087  union(ls_all_rows(p), ls_all_columns(p), ls_different_fields(p))]$
00088 
00089 output_dual_weak_ls(p,filename) := block([FF : standardise_fcs(dual_weak_ls(p))],
00090   output_fcs_v(
00091     sconcat("The Latin square problem (dual weak form) with dimension ", p, "."), 
00092     FF[1],
00093     filename,
00094     FF[2]))$
00095 
00096 
00097 /* The strong Latin square problem as formal clause-set: */
00098 strong_ls(p) := [var_ls(p), 
00099  union(weak_ls(p)[2], dual_weak_ls(p)[2])]$
00100 
00101 output_strong_ls(p,filename) := block([FF : standardise_fcs(strong_ls(p))],
00102   output_fcs_v(
00103     sconcat("The Latin square problem (strong form) with dimension ", p, "."), 
00104     FF[1],
00105     filename,
00106     FF[2]))$
00107 
00108 
00109 /* ****************************
00110    * Orthogonality conditions *
00111    ****************************
00112 */
00113 
00114 /* Now a partially filled out latin square A is given, and
00115    a latin square B is sought, which is orthogonal to B.
00116    Matrix A is given as a square Maxima matrix of dimension p,
00117    with entries from {1,...,p}, and additionaly 0 for empty
00118    squares. For the values k in {1,...,p} the set C(k) for
00119    coordinates (i,j) with A[i,j] = k are computed, and then
00120    the orthogonality conditions are just that all C(k) must
00121    be "multicoloured" (all values for the fields of C(k) must be different).
00122 */
00123 /* Given A, compute the negative orthogonality conditions as boolean
00124    clause-set:
00125 */
00126 orthogonality_cond_ls(A) := block([p : matrix_size(A)[1], a],
00127   a : l2ary(create_list([],i,1,p)),
00128   for i : 1 thru p do
00129     for j : 1 thru p do block([v : A[i,j]],
00130       if not(v = 0) then
00131         a[v] : cons([i,j], a[v])),
00132   return(setify(
00133     create_list({-ls_var(P[1][1],P[1][2],k2),-ls_var(P[2][1],P[2][2],k2)},
00134          k,1,p, P,listify(map(listify,powerset(setify(a[k]),2))), k2,1,p))))$
00135 /* The positive orthogonality conditions as formal boolean
00136    clause-set:
00137 */
00138 orthogonality_dualcond_ls(A) := block([p : matrix_size(A)[1], a],
00139   a : l2ary(create_list([],i,1,p)),
00140   for i : 1 thru p do
00141     for j : 1 thru p do block([v : A[i,j]],
00142       if not(v = 0) then
00143         a[v] : cons([i,j], a[v])),
00144   return(setify(
00145     create_list(setify(create_list(ls_var(x[1],x[2],k), x,a[t])),
00146         t,1,p, k,1,p))))$
00147 
00148 orthogonality_strongcond_ls(A) := 
00149   union(orthogonality_cond_ls(A), orthogonality_dualcond_ls(A))$
00150 
00151 row_symmetrybreaking_ls(p) := setify(create_list({ls_var(i,1,i)},i,1,p))$
00152 
00153 exluding_solution_ls(A) := block([p : matrix_size(A)[1]],
00154   setify(create_list(-ls_var(i,j,A[i,j]), i,1,p, j,1,p)))$
00155 
00156