%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Sudoku puzzles with Mace4 % % Run mace4 like this to get all solutions: % % % mace4 -m -1 -f thisfile % % To get the first solution only: % % % mace4 -f thisfile % % Unfortunately, Mace4 counts from 0, so you'll probably have to % translate your puzzle. If it is given with 1 ... 9, you can % simply replace 9 with 0. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% assign(domain_size, 9). % for a 9x9 puzzle assign(max_seconds, 2). % time limit set(print_models_portable). % output format formulas(sudoko_rules). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % First we have the "at most one of each" rules. % Rule 1a: At most one of each in each row. all x all y1 all y2 (f(x, y1) = f(x, y2) -> y1 = y2). % Rule 2a: At most one of each in each column. all x1 all x2 all y (f(x1, y) = f(x2, y) -> x1 = x2). % Before the "at most" rule for regions, we define "same_interval". % For 9x9 puzzles, the intervals are {0,1,2}, {3,4,5}, {6,7,8}; % same_interval(x,y) is an equivalence relation. all x same_interval(x,x). all x all y (same_interval(x,y) -> same_interval(y,x)). all x all y all z (same_interval(x,y) & same_interval(y,z) -> same_interval(x,z)). same_interval(0,1). same_interval(1,2). same_interval(3,4). same_interval(4,5). same_interval(6,7). same_interval(7,8). -same_interval(0,3). -same_interval(3,6). -same_interval(0,6). % The preceding clauses completely specify the same_interval relation. % Regions % The regions are determined by the intervals; in particular, % same_interval(x1,x2) and same_interval(y1,y2) imply that % cells f(x1,y1) and f(x2,y2) are in the same region. We could % define a 4-place relation same_region(x1,y1,x2,y2), but that % slows down mace4; instead, we'll just use same_interval in the % following rule. % Rule 3a: At most one of each in each region. all x1 all y1 all x2 all y2 ( same_interval(x1,x2) & same_interval(y1,y2) & f(x1, y1) = f(x2, y2) -> x1 = x2 & y1 = y2 ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % "At least" rules. It's sufficient to use the "at most" rules above % because those rules imply exactly one of each in each row, column, % and region. % % However, additional rules saying "at least one of each" can % be helpful (can lead to a solution with less work). These % "at least" rules are straightforward for the rows and columns. % But they but seem complicated for the regions, and the representations % we tried don't seem to help much, so "at least" rules for regions % are not included in this version. % Rule 1b: At least one of each in each row. all x all z exists y (f(x,y) = z). % Rule 2b: At least one of each in each column. all y all z exists x (f(x,y) = z). end_of_list. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Below is the specification for the puzzle shown here. Note that Mace4 % requires the numbers to be 0--8, NOT 1--9. If your puzzle has 1--9, % you can simply replace 9 with 0. % % 0 1 2 3 4 5 6 7 8 % +------------------------+ % 0 | 1 | 2 | 3 | % 1 | 2 | 3 | 4 | % 2 | 3 | 4 | 5 | % | -------+-------+------ | % 3 | 6 | 4 | 5 | % 4 | 7 | 5 | 6 | % 5 | 8 | 6 | 7 | % | -------+-------+------ | % 6 | 8 | 0 | 7 | % 7 | 0 | 1 | 8 | % 8 | 1 | 2 | 4 | % +------------------------+ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% formulas(sample_puzzle). f(0,0) = 1. f(0,3) = 2. f(0,6) = 3. f(1,1) = 2. f(1,4) = 3. f(1,7) = 4. f(2,2) = 3. f(2,5) = 4. f(2,8) = 5. f(3,0) = 6. f(3,3) = 4. f(3,6) = 5. f(4,1) = 7. f(4,4) = 5. f(4,7) = 6. f(5,2) = 8. f(5,5) = 6. f(5,8) = 7. f(6,0) = 8. f(6,3) = 0. f(6,6) = 7. f(7,1) = 0. f(7,4) = 1. f(7,7) = 8. f(8,2) = 1. f(8,5) = 2. f(8,8) = 4. end_of_list.