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],
00059  R : int2polyadic_padd(n-1, N, 3),
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