OKlibrary  0.2.1.6
Sudoku.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 5.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2011, 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
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")\$
00026 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")\$
00027 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")\$
00028
00029
00030 /* *************
00031    * Variables *
00032    *************
00033 */
00034
00035 /* Variables for the direct encoding are "sdk(i,j,k)", meaning that
00036    field (i,j) carries number k: */
00037 kill(sdk)\$
00038 declare(sdk, noun)\$
00039 declare(sdk, posfun)\$
00040 sdk_var(i,j,k) := nounify(sdk)(i,j,k)\$
00041 /* Here we have 1 <= i, j <= N, where N = p^2 is the dimension of the whole
00042    matrix, while p is the "box dimension" (p=3 for the standard Sudoku
00043    problems, while N=9).
00044 */
00045
00046 /* The list of variables for Sudoku formulas in direct encoding
00047    of box-dimension p: */
00048 var_sdk(p) := block([N : p^2],
00049  create_list(sdk_var(i,j,k), i,1,N, j,1,N, k,1,N))\$
00050
00051 /* Standardise all Sudoku-variables in term T w.r.t. direct encoding
00052    (for box-dimension p): */
00053 standardise_sdk(T,p) := block([N : p^2],
00054  ev(T, sdk(i,j,k) := (i-1)*N^2 + (j-1)*N + (k-1) +1, sdk))\$
00055 /* For standardised variable n, compute the corresponding sdk-variable.
00056    Prerequisite: p >= 1, 1 <= n <= (p^2)^3.
00057 */
00058 invstandardise_sdk(n,p) := block([N : p^2, R],
00060  apply(sdk_var,1+R))\$
00061
00062
00063 /* *************************
00064    * The basic translation *
00065    *************************
00066 */
00067
00068 /* Realise constraints for different numbers in each row: */
00069 sdk_different_rows_cl(p) := block([N : p^2],
00070  create_list({-sdk_var(i,j1,k), -sdk_var(i,j2,k)},
00071                     i,1,N, k,1,N, j1,1,N-1, j2,j1+1,N))\$
00072
00073 /* Realise constraints for different numbers in each column: */
00074 sdk_different_columns_cl(p) := block([N : p^2],
00075  create_list({- sdk_var(i1,j,k), - sdk_var(i2,j,k)},
00076                     j,1,N, k,1,N, i1,1,N-1, i2,i1+1,N))\$
00077
00078
00079 /* Given coordinates 1 <= i,j <= p of one of the N boxes, compute the list of
00080    coordinates of the N fields in the box (from top-left to bottom-right):
00081 */
00082 sdk_positions_box(i,j,p) := block(
00083  [row_offset : p * (i-1), column_offset : p * (j-1)],
00084  create_list([row_offset + r, column_offset + c], r,1,p, c,1,p))\$
00085
00086 /* Realise constraints for different numbers in each box: */
00087 sdk_different_boxes_cl(p) := block([N : p^2, L : []],
00088  for i : 1 thru p do
00089   for j : 1 thru p do block([P : sdk_positions_box(i,j,p)],
00090    for k : 1 thru N do
00091     for p1 : 1 thru N-1 do
00092      for p2 : p1+1 thru N do
00093       L : cons({- sdk_var(P[p1][1],P[p1][2],k), - sdk_var(P[p2][1],P[p2][2],k)}, L)),
00094  L)\$
00095
00096 /* Realise constraints that every field carries a number: */
00097 sdk_all_fields_cl(p) := block([N : p^2],
00098  create_list(setify(create_list(sdk_var(i,j,k), k,1,N)), i,1,N, j,1,N))\$
00099
00100
00101 /* The Sudoku problem in weak form (direct encoding) as formal clause-list: */
00102 weak_sdk_fcl(p) := [var_sdk(p),
00103  append(sdk_different_rows_cl(p),
00104         sdk_different_columns_cl(p),
00105         sdk_different_boxes_cl(p),
00106         sdk_all_fields_cl(p))]\$
00107 weak_sdk_stdfcl(p) := standardise_sdk(weak_sdk_fcl(p),p)\$
00108 weak_sdk_fcs(p) := fcl2fcs(weak_sdk_fcl(p))\$
00109 weak_sdk_stdfcs(p) := fcl2fcs(weak_sdk_stdfcl(p))\$
00110
00111
00112 /* Output an "empty" Sudoku problem to a file, using the weak translation
00113    and direct encoding: */
00114 output_weak_sdk(p,filename) := block([FF : weak_sdk_stdfcl(p)],
00115   output_fcl_v(
00116     sconcat(
00117 "The Sudoku problem (weak form) with box-dimension ", p, ".
00118 c Generated by the OKlibrary at Maxima-level."),
00119     FF,
00120     filename,
00121     []))\$
00122 output_weak_sdk_stdname(p) :=
00123   output_weak_sdk(p,sconcat("Weak_Sudoku_Box_dim_",p,".cnf"))\$
00124
00125
00126 /* **************************
00127    * Additional constraints *
00128    **************************
00129 */
00130
00131 /* Realise constraints that every row contains all numbers: */
00132 sdk_all_rows_cl(p) := block([N : p^2],
00133  create_list(setify(create_list(sdk_var(i,j,k),j,1,N)), i,1,N, k,1,N))\$
00134
00135 /* Realise constraints that every column contains all numbers: */
00136 sdk_all_columns_cl(p) := block([N : p^2],
00137  create_list(setify(create_list(sdk_var(i,j,k),i,1,N)), j,1,N, k,1,N))\$
00138
00139 /* Realise constraints that every box contains all numbers: */
00140 sdk_all_boxes_cl(p) := block([N : p^2],
00141  create_list(setify(create_list(sdk_var(p[1],p[2],k),p,sdk_positions_box(i,j,p))),
00142   i,1,p, j,1,p, k,1,N))\$
00143
00144 /* Realise constraints that every field carries at most one number: */
00145 sdk_different_fields_cl(p) := block([N : p^2],
00146   create_list({-sdk_var(i,j,k1), -sdk_var(i,j,k2)},
00147          i,1,N, j,1,N, k1,1,N-1, k2,k1+1,N))\$
00148
00149
00150 /* The Sudoku problem in dual weak form (direct encoding) as formal
00151    clause-list: */
00152 dual_weak_sdk_fcl(p) := [var_sdk(p),
00153  append(sdk_all_rows_cl(p),
00154         sdk_all_columns_cl(p),
00155         sdk_all_boxes_cl(p),
00156         sdk_different_fields_cl(p))]\$
00157 dual_weak_sdk_stdfcl(p) := standardise_sdk(dual_weak_sdk_fcl(p),p)\$
00158 dual_weak_sdk_fcs(p) := fcl2fcs(dual_weak_sdk_fcl(p))\$
00159 dual_weak_sdk_stdfcs(p) := fcl2fcs(dual_weak_sdk_stdfcl(p))\$
00160
00161
00162 /* Output an "empty" Sudoku problem to a file, using the dual weak translation
00163    and direct encoding: */
00164 output_dual_weak_sdk(p,filename) := block([FF : dual_weak_sdk_stdfcl(p)],
00165   output_fcl_v(
00166     sconcat(
00167 "The Sudoku problem (dual weak form) with box-dimension ", p, ".
00168 c Generated by the OKlibrary at Maxima-level."),
00169     FF,
00170     filename,
00171     []))\$
00172 output_dual_weak_sdk_stdname(p) :=
00173   output_dual_weak_sdk(p,sconcat("Dual_Weak_Sudoku_Box_dim_",p,".cnf"))\$
00174
00175
00176 /* The strong Sudoku problem (direct encoding) as formal clause-list: */
00177 strong_sdk_fcl(p) := [var_sdk(p),
00178  append(weak_sdk_fcl(p)[2], dual_weak_sdk_fcl(p)[2])]\$
00179 strong_sdk_stdfcl(p) := standardise_sdk(strong_sdk_fcl(p),p)\$
00180 strong_sdk_fcs(p) := fcl2fcs(strong_sdk_fcl(p))\$
00181 strong_sdk_stdfcs(p) := fcl2fcs(strong_sdk_stdfcl(p))\$
00182 strong_sdk_stdofcs(p) := fcs2fcl(strong_sdk_stdfcs(p))\$
00183
00184
00185 /* Output an "empty" Sudoku problem to a file, using the strong translation
00186    and direct encoding: */
00187 output_strong_sdk(p,filename) := block([FF : strong_sdk_stdfcl(p)],
00188   output_fcl_v(
00189     sconcat(
00190 "The Sudoku problem (strong form) with box-dimension ", p, ".
00191 c Generated by the OKlibrary at Maxima-level."),
00192     FF,
00193     filename,
00194     []))\$
00195 output_strong_sdk_stdname(p) :=
00196   output_strong_sdk(p,sconcat("Strong_Sudoku_Box_dim_",p,".cnf"))\$
00197
00198
00199 /* ***************
00200    * Mixed forms *
00201    ***************
00202 */
00203
00204 /* The weak form, plus either the long or the binary clauses from the
00205    dual weak form:
00206 */
00207
00208 weakpl_sdk_fcl(p) := [var_sdk(p),
00209  append(sdk_different_rows_cl(p),
00210         sdk_different_columns_cl(p),
00211         sdk_different_boxes_cl(p),
00212         sdk_all_fields_cl(p),
00213         sdk_all_rows_cl(p),
00214         sdk_all_columns_cl(p),
00215         sdk_all_boxes_cl(p))]\$
00216 weakpl_sdk_stdfcl(p) := standardise_sdk(weakpl_sdk_fcl(p),p)\$
00217 weakpl_sdk_fcs(p) := fcl2fcs(weakpl_sdk_fcl(p))\$
00218 weakpl_sdk_stdfcs(p) := fcl2fcs(weakpl_sdk_stdfcl(p))\$
00219
00220 weakpb_sdk_fcl(p) := [var_sdk(p),
00221  append(sdk_different_rows_cl(p),
00222         sdk_different_columns_cl(p),
00223         sdk_different_boxes_cl(p),
00224         sdk_all_fields_cl(p),
00225         sdk_different_fields_cl(p))]\$
00226 weakpb_sdk_stdfcl(p) := standardise_sdk(weakpb_sdk_fcl(p),p)\$
00227 weakpb_sdk_fcs(p) := fcl2fcs(weakpb_sdk_fcl(p))\$
00228 weakpb_sdk_stdfcs(p) := fcl2fcs(weakpb_sdk_stdfcl(p))\$
00229
00230 output_weakpl_sdk(p,filename) := block([FF : weakpl_sdk_stdfcl(p)],
00231   output_fcl_v(
00232     sconcat(
00233 "The Sudoku problem (weak-pl form) with box-dimension ", p, ".
00234 c Generated by the OKlibrary at Maxima-level."),
00235     FF,
00236     filename,
00237     []))\$
00238 output_weakpl_sdk_stdname(p) :=
00239   output_weakpl_sdk(p,sconcat("WeakPl_Sudoku_Box_dim_",p,".cnf"))\$
00240
00241 output_weakpb_sdk(p,filename) := block([FF : weakpb_sdk_stdfcl(p)],
00242   output_fcl_v(
00243     sconcat(
00244 "The Sudoku problem (weak-pb form) with box-dimension ", p, ".
00245 c Generated by the OKlibrary at Maxima-level."),
00246     FF,
00247     filename,
00248     []))\$
00249 output_weakpb_sdk_stdname(p) :=
00250   output_weakpb_sdk(p,sconcat("WeakPb_Sudoku_Box_dim_",p,".cnf"))\$
00251
00252
00253 /* The dual weak form, plus either the long or the binary clauses from the
00254    weak form:
00255 */
00256
00257 dual_weakpl_sdk_fcl(p) := [var_sdk(p),
00258  append(sdk_all_rows_cl(p),
00259         sdk_all_columns_cl(p),
00260         sdk_all_boxes_cl(p),
00261         sdk_different_fields_cl(p),
00262         sdk_all_fields_cl(p))]\$
00263 dual_weakpl_sdk_stdfcl(p) := standardise_sdk(dual_weakpl_sdk_fcl(p),p)\$
00264 dual_weakpl_sdk_fcs(p) := fcl2fcs(dual_weakpl_sdk_fcl(p))\$
00265 dual_weakpl_sdk_stdfcs(p) := fcl2fcs(dual_weakpl_sdk_stdfcl(p))\$
00266
00267 dual_weakpb_sdk_fcl(p) := [var_sdk(p),
00268  append(sdk_all_rows_cl(p),
00269         sdk_all_columns_cl(p),
00270         sdk_all_boxes_cl(p),
00271         sdk_different_fields_cl(p),
00272         sdk_different_rows_cl(p),
00273         sdk_different_columns_cl(p),
00274         sdk_different_boxes_cl(p))]\$
00275 dual_weakpb_sdk_stdfcl(p) := standardise_sdk(dual_weakpb_sdk_fcl(p),p)\$
00276 dual_weakpb_sdk_fcs(p) := fcl2fcs(dual_weakpb_sdk_fcl(p))\$
00277 dual_weakpb_sdk_stdfcs(p) := fcl2fcs(dual_weakpb_sdk_stdfcl(p))\$
00278
00279 output_dual_weakpl_sdk(p,filename) := block([FF : dual_weakpl_sdk_stdfcl(p)],
00280   output_fcl_v(
00281     sconcat(
00282 "The Sudoku problem (dual_weak-pl form) with box-dimension ", p, ".
00283 c Generated by the OKlibrary at Maxima-level."),
00284     FF,
00285     filename,
00286     []))\$
00287 output_dual_weakpl_sdk_stdname(p) :=
00288   output_dual_weakpl_sdk(p,sconcat("Dual_WeakPl_Sudoku_Box_dim_",p,".cnf"))\$
00289
00290 output_dual_weakpb_sdk(p,filename) := block([FF : dual_weakpb_sdk_stdfcl(p)],
00291   output_fcl_v(
00292     sconcat(
00293 "The Sudoku problem (dual_weak-pb form) with box-dimension ", p, ".
00294 c Generated by the OKlibrary at Maxima-level."),
00295     FF,
00296     filename,
00297     []))\$
00298 output_dual_weakpb_sdk_stdname(p) :=
00299   output_dual_weakpb_sdk(p,sconcat("Dual_WeakPb_Sudoku_Box_dim_",p,".cnf"))\$
00300
00301
00302 /* ************
00303    * Measures *
00304    ************
00305 */
00306
00307 /* Number of variables: */
00308 nvar_sdk(p) := p^6\$
00309
00310 /* List of clause-counts for weak_sdk as with ncl_list_fcl: */
00311 ncl_list_weak_sdk_fcl(p) := if p = 0 then [] elseif p = 1 then [[1,1]] else
00312  block([N : p^2], return([ [2, 3 * N^2 * binomial(N,2)], [N, N^2] ]))\$
00313 ncl_list_weak_sdk_fcs(p) := if p = 0 then [] elseif p = 1 then [[1,1]] else
00314  block([N : p^2], return([ [2, 3 * N^2 * binomial(N,2) - N^2 * N * (p-1)], [N, N^2] ]))\$
00315 /* List of clause-counts for dual_weak_sdk as with ncl_list: */
00316 ncl_list_dual_weak_sdk_fcl(p) := if p = 0 then [] elseif p = 1 then [[1,3]] else
00317  block([N : p^2], return([[2, N^2 * binomial(N,2)], [N, 3 * N^2]]))\$
00318 ncl_list_dual_weak_sdk_fcs(p) := if p = 0 then [] elseif p = 1 then [[1,1]] else
00319  block([N : p^2], return([[2, N^2 * binomial(N,2)], [N, 3 * N^2]]))\$
00320 /* List of clause-counts for strong_sdk as with ncl_list: */
00321 ncl_list_strong_sdk_fcl(p) := if p = 0 then [] elseif p = 1 then [[1,4]] else
00322  block([N : p^2], return([ [2, 4 * N^2 * binomial(N,2)], [N, 4 * N^2] ]))\$
00323 ncl_list_strong_sdk_fcs(p) := if p = 0 then [] elseif p = 1 then [[1,1]] else
00324  block([N : p^2], return([ [2, 4 * N^2 * binomial(N,2) - N^2 * N * (p-1)], [N, 4 * N^2] ]))\$
00325
00326 /* Total number of clauses: */
00327 ncl_weak_sdk_fcl(p) := block([L : ncl_list_weak_sdk_fcl(p)],
00328  return(sum_l(map(second,L))))\$
00329 ncl_weak_sdk_fcs(p) := block([L : ncl_list_weak_sdk_fcs(p)],
00330  return(sum_l(map(second,L))))\$
00331 ncl_dual_weak_sdk_fcl(p) := block([L : ncl_list_dual_weak_sdk_fcl(p)],
00332  return(sum_l(map(second,L))))\$
00333 ncl_dual_weak_sdk_fcs(p) := block([L : ncl_list_dual_weak_sdk_fcs(p)],
00334  return(sum_l(map(second,L))))\$
00335 ncl_strong_sdk_fcl(p) := block([L : ncl_list_strong_sdk_fcl(p)],
00336  return(sum_l(map(second,L))))\$
00337 ncl_strong_sdk_fcs(p) := block([L : ncl_list_strong_sdk_fcs(p)],
00338  return(sum_l(map(second,L))))\$
00339
00340
00341 /* Number of literal occurrences: */
00342 nlitocc_weak_sdk_fcl(p) := block([L : ncl_list_weak_sdk_fcl(p)],
00343  return(sum_l(map("*",map(first,L),map(second,L)))))\$
00344 nlitocc_weak_sdk_fcs(p) := block([L : ncl_list_weak_sdk_fcs(p)],
00345  return(sum_l(map("*",map(first,L),map(second,L)))))\$
00346 nlitocc_dual_weak_sdk_fcl(p) := block([L : ncl_list_dual_weak_sdk_fcl(p)],
00347  return(sum_l(map("*",map(first,L),map(second,L)))))\$
00348 nlitocc_dual_weak_sdk_fcs(p) := block([L : ncl_list_dual_weak_sdk_fcs(p)],
00349  return(sum_l(map("*",map(first,L),map(second,L)))))\$
00350 nlitocc_strong_sdk_fcl(p) := block([L : ncl_list_strong_sdk_fcl(p)],
00351  return(sum_l(map("*",map(first,L),map(second,L)))))\$
00352 nlitocc_strong_sdk_fcs(p) := block([L : ncl_list_strong_sdk_fcs(p)],
00353  return(sum_l(map("*",map(first,L),map(second,L)))))\$
00354
00355
00356 /* ********************
00357    * Creating puzzles *
00358    ********************
00359 */
00360
00361 /* For the direct encoding */
00362
00363 /* Field settings as unit-clauses, already standardised. Input is a list L
00364    of triples [i,j,k], meaning that field [i,j] carries number k.
00365    Prerequisite is that all fields are in range allowed by p.
00366 */
00367 sdk_fields_stdcl(L,p) := map(set, map(lambda([t],standardise_sdk(t,p)),map(lambda([t],apply(sdk_var,t)), L)))\$
00368
00369 /* Output a complete Sudoku problem ("puzzle") to a file, using the strong
00370    translation:
00371 */
00372 output_sdk_puzzle(p,L,comment,filename) := block(
00373  [FF : strong_sdk_stdofcs(p),
00374   F : sdk_fields_stdcl(L,p)],
00375   output_fcl_v(
00376     sconcat(
00377 "The Sudoku problem (strong form) with box-dimension ", p, ", and with additional fields set.
00378 c Generated by the OKlibrary at Maxima-level.
00379 c ", comment),
00380     [FF[1], append(FF[2],F)],
00381     filename,
00382     []))\$
00383
00384 /* Some special cases: */
00385
00386 EasterMonster : [
00387  [1,1,1],[1,9,2],
00388  [2,2,9],[2,4,4],[2,8,5],
00389  [3,3,6],[3,7,7],
00390  [4,2,5],[4,4,9],[4,6,3],
00391  [5,5,7],
00392  [6,4,8],[6,5,5],[6,8,4],
00393  [7,1,7],[7,7,6],
00394  [8,2,3],[8,6,9],[8,8,8],
00395  [9,3,2],[9,9,1]]\$
00396
00397 output_sdk_EasterMonster() :=
00398  output_sdk_puzzle(3,EasterMonster,"Problem EasterMonster in [The Hidden Logic of Sudoku, Berthier].","S_EasterMonster.cnf")\$
00399
00400
```