%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 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.
