! Sudoku.txt - axioms for Sudoku puzzle solution !/ for paper "A More General Specification Language" Progress Toward the Holy Grail Workshop August 28, 2017, Melbourne, Australia part of ICLP'17 ! Our top-level axiom defines a program that reads an input text file with ! a Sudoku puzzle and writes an output file that shows the input puzzle ! along with its solution. (Program %infile %outfile)< ! Program valid exprs for Sudoku solver (sudoku_in %infile %inarr), ! map input file to 9x9 board array ! Array is just a sequence of 9 rows each with 9 elements, ! each of which is a digit '1'-'9' or underscore character. ! (A digit '0' in the input file prevents a solution.) (sudoku_soln %inarr %outarr), ! solve the Sudoku puzzle! ! Output array is input array with '_' chars replaced with digits. (sudoku_out %inarr %outarr %outfile). ! we output both puzzle & solution ! If the input puzzle has more than one solution, then a Program ! valid expression is generated for each solution. ! The input file contains 9 lines each with 9 digit/underscore characters. ! Characters other than digit/_ are ignored. ! Additional lines (without any digit/_ characters) are ignored. ! An example input file could look as follows: _ 1 _ _ 8 _ _ _ _ 6 5 _ | 7 _ _ | 4 _ _ -- spacing and non-digit/_ chars ignored _ _ _ _ 2 4 _ 9 _ ---------+---------+--------- -- lines without digit/_ chars ignored _ 9 _ _ _ 7 6 _ _ ... ! sudoku_in - map an input text file to a 9x9 array of digits and _ chars ! On input, all characters except digits and _ are treated as blanks. ! At this point digit 0 is treated like digits 1-9. (sudoku_in () ()). (sudoku_in (%line \$lines) ((% \$) \$d_rows))< (sudoku_in_line %line (% \$)), ! line has one or more digit and _ chars (sudoku_in (\$lines) (\$d_rows)). (sudoku_in (%line \$lines) (\$d_rows))< (sudoku_in_line %line ()), ! line doesn't have any digit or _ chars (sudoku_in (\$lines) (\$d_rows)). ! Note that lines with digit and _ characters produce an array row. ! Lines without any digit and _ characters are skipped. ! If array is not exactly 9x9 then we won't get a solution. ! sudoku_in_line - get just the digit and _ characters from a line ! (sudoku_in_line ) ! - note that 0 is included in the set of digits (but there won't be a soln) (sudoku_in_line () ()). (axioms ! a higher-order form! ((sudoku_in_line ( %d_ \$chars) (%d_ \$d_)) ( in %d_ %digit_))) ((sudoku_in_line (%~d_ \$chars) ( \$d_)) (not_in %~d_ %digit_))) )< (sudoku_in_line (\$chars) (\$d_)), (== %digit_ "0123456789_"). ! we allow '0' here but won't get a solution ! The corresponding output file in the Program valid expression is as follows: Sudoku Puzzle Input: _ 1 _ | _ 8 _ | _ _ _ 6 5 _ | 7 _ _ | 4 _ _ _ _ _ | _ 2 4 | _ 9 _ ---------+---------+--------- _ 9 _ | _ _ 7 | 6 _ _ ... Solution: 2 1 4 | 9 8 6 | 5 7 3 6 5 9 | 7 3 1 | 4 2 8 8 7 3 | 5 2 4 | 1 9 6 ---------+---------+--------- 4 9 8 | 2 1 7 | 6 3 5 ... ! sudoku_out - form output file with nicely formated input and solved puzzle (sudoku_out %inarr %outarr (" Sudoku Puzzle" ! title is centered over board "" "Input:" \$inlines "" "Solution:" \$outlines ))< (sudoku_out_arr %inarr (\$inlines)), ! both input & output arrays displayed (sudoku_out_arr %outarr (\$outlines)). ! sudoku_out_arr - output Sudoku array to a nicely formated block of lines ! (sudoku_out_arr <9x9 digit/_ array> ) (sudoku_out_arr %arr (\$lns1-3 %sep_ln \$lns4-6 %sep_ln \$lns7-9))< (3=parts %arr %3_3rows), ! partition array rows into 3-row subseqs ((map (map sudoku_out_row)) %3_3rows ((\$lns1-3) (\$lns4-6) (\$lns7-9))), ! map each row into an output line (== %sep_ln " ---------+---------+---------"). ! separator line ! 1 2 3 4 5 6 7 8 9 -- digits wrt sep line ! sudoku_out_row - map row of Sudoku array to output line (sudoku_out_line %row (' ' \$str1-3 '|' \$str4-6 '|' \$str7-9))< ! form line (3=parts %row (%3_3elems), ! partition row into 3-elem subseqs ((map (map sudoku_out_elem)) %3_3elems %3_3strs), ! map row's elements to blank-surrounded strings ((map concat*) %3_3strs ((\$str1-3) (\$str4-6) (\$str7-9))). ! concat element strings into 3-element strings ! sudoku_out_elem - surround each Sudoku element character with blanks (sudoku_out_elem % (' ' % ' ')). ! '3' -> " 3 " ! sudoku_soln - get an instance of input array that satisfies perm dig property (sudoku_soln %inarr %outarr)< (instance '_' %inarr %outarr), ! '_' instanced with arbitrary exprs (sudoku_rows %outarr %rows), ! rows of board (sudoku_cols %outarr %cols), ! columns of board (sudoku_subarrs %outarr %subarrs), ! 3x3 subarrays of board ! -- these 3x3 subarrs are expressed as 9 9-elem sequences (concat* (%rows %cols %subarrs) %allseqs), (1* perm "123456789" %allseqs). ! all sequences of the output array are permutations of 1-9 (sudoku_rows %arr %arr). ! array is already a sequence of rows (sudoku_cols %arr %cols)< ! columns of sudoku board (transpose %arr %cols). ! transpose to get columns (sukoku_subarrs %arr %subarrs)< ! get the 9 3x3 arrays as sequences (3=parts %arr %3_3row_groups), ! sequence of 3-row groups ((map (map 3=parts)) %3_3row_groups %3_3row_3elem_seqs), ! map each row of 3-row groups into three sequences of 3 elements ((map transpose) %3_3row_3elem_seqs %3x3_3x3subarrs), ! get 3x3 subarrays grouped in 3-row groups (concat* %3x3_3x3subarrs %3x3subarrs), ! get seq of 9 3x3 subarrays ((map concat*) %3x3subarrs %subarrs). ! flatten 3x3 subarrs into seqs