Skip to content

Instantly share code, notes, and snippets.

@atbradley
Created February 22, 2021 15:51
Show Gist options
  • Save atbradley/298718fc8f3c2cf8d34d62ceada32af0 to your computer and use it in GitHub Desktop.
Save atbradley/298718fc8f3c2cf8d34d62ceada32af0 to your computer and use it in GitHub Desktop.
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)];
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment