array [1..8] of var 1..8: LETTERS = [1, 2, 3, 4, 5, 6, 7, 8]; array [1..3] of var 0..1: carry; array [1..8] of var 0..9: dig :: output_array([1..8]); array [1..80] of var 0..1: x; constraint int_le(1, dig[3]); constraint int_lin_eq([-10, 1, 1, -1], [carry[1], dig[1], dig[2], dig[8]], 0); constraint int_lin_eq([1, -9, -1, 1], [carry[3], dig[3], dig[5], dig[7]], 0); constraint int_lin_eq([1, -10, -1, 1, 1], [carry[1], carry[2], dig[2], dig[4], dig[6]], 0); constraint int_lin_eq([1, -10, 1, -1, 1], [carry[2], carry[3], dig[2], dig[4], dig[5]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[2], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[3], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[4], x[32], x[33], x[34], x[35], x[36], x[37], x[38], x[39], x[40]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[5], x[42], x[43], x[44], x[45], x[46], x[47], x[48], x[49], x[50]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[6], x[52], x[53], x[54], x[55], x[56], x[57], x[58], x[59], x[60]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[7], x[62], x[63], x[64], x[65], x[66], x[67], x[68], x[69], x[70]], 0); constraint int_lin_eq([1, -1, -2, -3, -4, -5, -6, -7, -8, -9], [dig[8], x[72], x[73], x[74], x[75], x[76], x[77], x[78], x[79], x[80]], 0); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10]], 1); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20]], 1); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[21], x[22], x[23], x[24], x[25], x[26], x[27], x[28], x[29], x[30]], 1); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[31], x[32], x[33], x[34], x[35], x[36], x[37], x[38], x[39], x[40]], 1); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[41], x[42], x[43], x[44], x[45], x[46], x[47], x[48], x[49], x[50]], 1); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[51], x[52], x[53], x[54], x[55], x[56], x[57], x[58], x[59], x[60]], 1); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[61], x[62], x[63], x[64], x[65], x[66], x[67], x[68], x[69], x[70]], 1); constraint int_lin_eq([1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [x[71], x[72], x[73], x[74], x[75], x[76], x[77], x[78], x[79], x[80]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[1], x[11], x[21], x[31], x[41], x[51], x[61], x[71]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[2], x[12], x[22], x[32], x[42], x[52], x[62], x[72]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[3], x[13], x[23], x[33], x[43], x[53], x[63], x[73]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[4], x[14], x[24], x[34], x[44], x[54], x[64], x[74]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[5], x[15], x[25], x[35], x[45], x[55], x[65], x[75]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[6], x[16], x[26], x[36], x[46], x[56], x[66], x[76]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[7], x[17], x[27], x[37], x[47], x[57], x[67], x[77]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[8], x[18], x[28], x[38], x[48], x[58], x[68], x[78]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[9], x[19], x[29], x[39], x[49], x[59], x[69], x[79]], 1); constraint int_lin_le([1, 1, 1, 1, 1, 1, 1, 1], [x[10], x[20], x[30], x[40], x[50], x[60], x[70], x[80]], 1); solve satisfy;