cryptarithm.mzn

enum LETTERS = {dmy, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z};
LETTERS: dummy = dmy;

array[int, int] of LETTERS: ADDENDS;
array[int] of LETTERS: SOLUTION;
array[int] of LETTERS: USED;

array[LETTERS] of var 0..9: solution;

constraint solution[dummy] = 0;

%%% Count all dummies in an array
function int: count_dummies(array[int] of LETTERS: arr) = sum(i in index_set(arr))(arr[i]==dummy);


%%% Function to add up one line (from ADDENDS or SOLUTION)
function var int: line_to_number(array[int] of LETTERS: line) = sum(i in index_set(line))
                                                               ( let { var int: cod = count_dummies(line); }
                                                                 in solution[line[i]] * 10^(max(index_set(line))-i-cod));


%% CONSTRAINTS
% First letter of each addend and solution can't be zero.
constraint forall(r in index_set_1of2(ADDENDS))(solution[ADDENDS[r,1]] > 0);
constraint solution[SOLUTION[1]] > 0;


% All letters used in the problem must be different.
include "alldifferent.mzn";
constraint alldifferent(i in index_set(USED))(solution[USED[i]]);


% Addition must be correct.
constraint sum(i in index_set_1of2(ADDENDS))(line_to_number(row(ADDENDS, i))) = 
           line_to_number(SOLUTION);


solve satisfy;
%output ["\(solution)"];
output [ show(USED[i]) ++ ": " ++ show(solution[USED[i]]) ++ ", " | i in index_set(USED)];

cryptarithm.py

import json, re, string
import pymzn

def cryptarithm(problem):
    """
    Uses the MiniZinc model cryptarithm.mzn to solve the cryptarithm 
    given in `problem` (example problem: "SEND+MORE=MONEY").
    
    Returns a 2-tuple (data dictionary for MiniZinc, solution dictionary)
    """
    data = {}
    
    prob = problem.upper().replace(' ', '')
    
    (addends, solution) = prob.split('=')
    addends = addends.split('+')
    
    letters = set(re.sub('[+=\s]', '', prob))
    data['USED'] = letters
    
    #Have to pad the addends with dummies to make them all the same length.
    maxaddendlen = max(len(x) for x in addends)
    addends = [list(add) + ['dmy']*(maxaddendlen-len(add)) for add in addends]
    data['ADDENDS'] = addends
    
    solution = list(solution)
    data['SOLUTION'] = solution
    
    try:
        solns = pymzn.minizinc('cryptarithm.mzn', data=data, output_mode='json')[0]
        sol = json.loads(solns)['solution']
        sol.pop(0)
        sol = {k: v for k, v in zip(string.ascii_uppercase, sol) if k in data['USED']}
    except:
        sol = None
    return (data, sol)