% 
% Enigma problem 1568 (Odd puzzle) in MiniZinc.
% 
% From New Scientist
% http://www.newscientist.com/article/mg20427311.100-enigma-number-1568.html
% """
% 21 October 2009 by Albert Haddad
% 
% Odd puzzle
% 
% In this multiplication sum the digits have been replaced by letters and 
% dots. Different letters stand for different digits, the same letter 
% stands for the same digit, each dot can be any digit, and leading 
% digits cannot be zero.
% 
% [
%         . . .    | num1
%       * . . .    | num2
%       -------
%         . . .    | num3
%       . . .      | num4
%     O D D        | ODD
%     ---------
%   P U Z Z L E    | PUZZLE
%   
% ]
%
% What is the six-figure odd PUZZLE?
% """

% 
% This MiniZinc model was created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc
%
include "globals.mzn"; 

int: n = 7; % number of unknown
set of int: Digits = 0..9;
var Digits: O :: is_output;
var Digits: D :: is_output;
var Digits: P :: is_output;
var Digits: U :: is_output;
var Digits: Z :: is_output;
var Digits: L :: is_output;
var Digits: E :: is_output;
array[1..n] of var Digits: x :: is_output;

var 100..999: num1 :: is_output;
var 100..999: num2 :: is_output;
var 100..999: num3 :: is_output;
var 100..999: num4 :: is_output;
var 100..999: ODD  :: is_output;
var 100000..999999: PUZZLE :: is_output;

predicate cp1d(array[int] of var int: x, array[int] of var int: y) =
  assert(index_set(x) = index_set(y),
           "cp1d: x and y have different sizes",
    forall(i in index_set(x)) ( x[i] = y[i] ) )
; 


% solve satisfy;
solve :: int_search(
             x ++ [num1,num2,num3,num4,ODD,PUZZLE], 
             first_fail, 
             indomain_min, 
             complete) 
         satisfy;

constraint
   cp1d(x, [O,D,P,U,Z,L,E]) /\
   
   all_different(x) /\

   ODD = 100*O + 10*D + D /\
   PUZZLE = 100000*P + 10000*U + 1000*Z + 100*Z + 10*L + E /\

   num1 * num2 = num3 + num4*10 + ODD*100 /\
   PUZZLE = num1 * num2 /\

   PUZZLE mod 2 = 1 /\ % PUZZLE is odd

   % And then code the "long multiplication"
   num1 * (num2 mod 10) = num3 /\
   num1 * ((num2 div 10) mod 10) = num4 /\
   num1 * (num2 div 100) = ODD
;