OKlibrary  0.2.1.6
GeneralisedTicTacToe.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 26.11.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/Generators/Generators.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Colouring.mac")$
00024 
00025 
00026 /* *********************************
00027    * k in a line on an m x n board *
00028    *********************************
00029 */
00030 
00031 /* Boolean clause-sets, using variables colv([i,j]) */
00032 
00033 /* For k >= 3, these clause-sets are all satisfiable:
00034    First two rows:             010101...
00035                                010101...
00036    next two rows:              101010...
00037                                101010...
00038    and then repeat that scheme:
00039     - clearly the row-hyperedges are not monocoloured;
00040     - every column-hyperedge must contain rows from different
00041       types of blocks, and thus is not monocoloured;
00042     - finally ever diagonal must contain two consecutive rows
00043       from the same block, and thus is not monocoloured.
00044 */
00045 
00046 gttt_ofcs(k,m,n) := tcol2sat_ohg2fcl(gttt_ohg(k,m,n))$
00047 
00048 /* Standardisation */
00049 
00050 standardise_gttt(n) := buildq([n],
00051  lambda([t], ev(t, colv(p):=second(p)+(first(p)-1)*n, colv)))$
00052 
00053 invstandardise_gttt(n) := buildq([n],
00054  lambda([i], block([d:divide(i-1,n)+1], colv_var([first(d),second(d)]))))$
00055 
00056 gttt_stdofcs(k,m,n) := standardise_gttt(n)(gttt_ofcs(k,m,n))$
00057 
00058 /* Output */
00059 
00060 output_gttt(k,m,n,filename) := outputext_fcl(
00061  sconcat(k, " in a row on a ", m, " times ", n, " board."),
00062  gttt_stdofcs(k,m,n),
00063  filename)$
00064 
00065 output_gttt_stdname(k,m,n) := output_gttt(k,m,n,
00066  sconcat("TicTacToc_",k,"-",m,"-",n,".cnf"))$
00067 
00068