/* SEND+MORE=MONEY in Picat using bv module. Solve the alphametic problem SEND+MORE=MONEY using distinct digits for the letters. sendmore and sendmore2 are using base 10, and sendmore_base use "any" base. Also some non-CP variants. This uses the bv module. Model created by Hakan Kjellerstrand, hakank@gmail.com See also my Picat page: http://www.hakank.org/picat/ */ import util. import sat. import bv_utils. main => go. /* digits = [9,5,6,7,1,0,8,2] [send = 9567,more = 1085,money = 10652] 0.023s */ go ?=> nolog, Base = 10, time2(sendmore(Base,Digits,SEND,MORE,MONEY)), print_solution(Base,Digits,SEND,MORE,MONEY), fail, nl. go => true. /* An example in larger bases: * Base 2**64 (18446744073709551616) digits = [18446744073709551615,9223372036854775807,9223372036854775808,11858621190241854609,1,0,18446744073709551614,2635249153387078800] [send = 115792089237316195420432434140994567471181948770576261599686577603155470132369,more = 6277101735386680764176071790128604879538059935785238396927,money = 115792089237316195426709535876381248235358020560704866479224637538940708529296] [send = [18446744073709551615,9223372036854775807,9223372036854775808,11858621190241854609],more = [1,0,18446744073709551614,9223372036854775807],money = [1,0,9223372036854775808,9223372036854775807,2635249153387078800]] * Base 2**128 (340282366920938463463374607431768211456) digits = [340282366920938463463374607431768211455,67516342643043345925272739569749131263,67516342643043345925272739569749131264,303823541893695056663727328064078760228,1,0,340282366920938463463374607431768211454,31057517615799939125625460202059680035] [send = 13407807929942597099574024998205846127447781672768299390418480625863707059470023065626464419794740489037158802711709479102537893132502403142200584138017060,more = 39402006196394479212279040100143613805195531359702762863371864389254409679349867547688707985343371748339247332655103,money = 13407807929942597099574024998205846127487183678964693869630759665963850673275218596986167182658112353426413212391059346650226601117845774890539831470672163] [send = [340282366920938463463374607431768211455,67516342643043345925272739569749131263,67516342643043345925272739569749131264,303823541893695056663727328064078760228],more = [1,0,340282366920938463463374607431768211454,67516342643043345925272739569749131263],money = [1,0,67516342643043345925272739569749131264,67516342643043345925272739569749131263,31057517615799939125625460202059680035]] * Base 2**255 (57896044618658097711785492504343953926634992332820282019728792003956564819968) digits = [57896044618658097711785492504343953926634992332820282019728792003956564819967,35840408573455012869200542978879590526012138110694415606479133308450643116031,35840408573455012869200542978879590526012138110694415606479133308450643116032,26420814012482862051013220785712518656996127453746946167202827957370246660096,1,0,57896044618658097711785492504343953926634992332820282019728792003956564819966,4365177967279777208428271260248155256373273231621079753953169261864324956159] [send = 11235582092889474423308157442431404585112356118389416079589380072358292237843736266361313132224987716582461284036949852186192280940561135122009712969405584068682264565387411858109211405197104479300060654636279621478144759418799933383704485174164751527982243263387910829117267459859388532892103781858316124160,more = 194064761537588616893622436057812819407110752139587076392381504753256369085800462743342286752855703250060517798673253992226595603858782689291466350387665949193076676715965409680263638860179099858024758423769112257897514806492004351,money = 11235582092889474423308157442431404585112356118389416079589380072358292237843930331122850720841881339018519096856356962938331868016953516626762969338491384531425606852140267561359271922995777733292287250240138404167436225769187599332897561850880716937662506902248089928975292218283157645150001296664808128511] [send = [57896044618658097711785492504343953926634992332820282019728792003956564819967,35840408573455012869200542978879590526012138110694415606479133308450643116031,35840408573455012869200542978879590526012138110694415606479133308450643116032,26420814012482862051013220785712518656996127453746946167202827957370246660096],more = [1,0,57896044618658097711785492504343953926634992332820282019728792003956564819966,35840408573455012869200542978879590526012138110694415606479133308450643116031],money = [1,0,35840408573455012869200542978879590526012138110694415606479133308450643116032,35840408573455012869200542978879590526012138110694415606479133308450643116031,4365177967279777208428271260248155256373273231621079753953169261864324956159]] */ go1 ?=> garbage_collect(400_000_000), nolog, % Base = 2**64, % Base = 2**128, Base = 2**255, % Base = 2**256, % too large println(base=Base), time2(sendmore(Base,Digits,SEND,MORE,MONEY)), print_solution(Base,Digits,SEND,MORE,MONEY), MONEY_BITS = MONEY.bti.to_string.len, println(money_bits=MONEY_BITS), fail, nl. go1 => true. % 0.02s go2 => nolog, Base = 10, sendmore2(Base,Digits,SEND,MORE,MONEY), print_solution(Base,Digits,SEND,MORE,MONEY), fail, nl. go2 => true. go3 ?=> nolog, foreach(Base in 2..30) nl, println(base=Base), if sendmore2(Base,Digits,SEND,MORE,MONEY) then print_solution(Base,Digits,SEND,MORE,MONEY) end end, nl. go3 => true. /* The number of solutions for different bases. Base 2: 0 Base 3: 0 Base 4: 0 Base 5: 0 Base 6: 0 Base 7: 0 Base 8: 0 Base 9: 0 Base 10: 1 Base 11: 3 Base 12: 6 Base 13: 10 Base 14: 15 Base 15: 21 Base 16: 28 Base 17: 36 Base 18: 45 Base 19: 55 Base 20: 66 Base 21: 78 Base 22: 91 Base 23: 105 Base 24: 120 Base 25: 136 Base 26: 153 Base 27: 171 Base 28: 190 Base 29: 210 Base 30: 231 All lengths: [0,0,0,0,0,0,0,0,1,3,6,10,15,21,28,36,45,55,66,78,91,105,120,136,153,171,190,210,231] CPU time 47.279 seconds. Backtracks: 0 Note that this (from N>=10) is a pattern of the triangular numbers. (The CP version in send_more_money.pi takes 0.004s. However, the SAT is much slower: 23.078s) */ go4 ?=> nolog, Lens = [], foreach(Base in 2..30) Count = count_all(sendmore(Base,_Digits,_SEND,_MORE,_MONEY)), Lens := Lens ++ [Count], printf("Base %d: %d \n", Base, Count), end, printf("All lengths: %w\n", Lens). go4 => true. /* With carry: Base 10: digits = [9,5,6,7,1,0,8,2] carry = [1,1,0,1] Base 11: digits = [10,5,6,8,1,0,9,2] carry = [1,1,0,1] digits = [10,7,8,6,1,0,9,2] carry = [1,1,0,1] digits = [10,6,7,8,1,0,9,3] carry = [1,1,0,1] Base 2**512 digits = [13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084095,397489927350648685363280566611389491154831830453998278787549955692955108786726917815292999446100926655838374625898860277404577111736318,397489927350648685363280566611389491154831830453998278787549955692955108786726917815292999446100926655838374625898860277404577111736319,13407807929942597099216284063591941031407536655840281269921172902433697128815290195608015790594753440572767864483152244617712776429073410538587143907835904,1,0,13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084094,39748992736743589291451401859277383352443289165931377529293174499096601214576930698029005742767120419797268243025700869558072013488126] carry = [1,1,0,1] Base 2**1023 digits = [78649074650226320963157102097019832095786492828725912557125660506508045664906671370559958828553297009240049822443734593975720523856307272340620750904769929415273453373378649808382221075545166177260723791537190023866690923524827510644836985861611916258965848424506505479976920098084875883365468394210598060030,11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008575,0,44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034268,1,33706746278668423269924472327294213755337068355168248238768140217074876713531430587382839497951413003960021352475886254561023081652703116717408893244901398320831480017162278489306666175233642647397453053515938581657153252939211790276358708226405106968128220753359930919990108613464946807156629311804542025728,56177910464447372116540787212157022925561780591947080397946900361791461189219050978971399163252355006600035587459810424268371802754505194529014822074835663868052466695270464148844443625389404412329088422526564302761922088232019650460597847044008511613547034588933218199983514355774911345261048853007570042878,11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008539] carry = [1,1,1,1] */ go5 => nolog, % Base = 10, % Base = 11, % Base = 2**512, Base = 2**1023, % Base = 2**1024, % too large sendmore_carry(Base,Digits,Carry), println(digits=Digits.bti), println(carry=Carry.bti), nl, fail, nl. % % % sendmore(Digits,SEND,MORE,MONEY) => sendmore(10,Digits,SEND,MORE,MONEY). sendmore(Base,Digits,SEND,MORE,MONEY) => Digits = make_bv_array(8,0,Base-1), Digits = {S,E,N,D,M,O,R,Y}, bv_all_different(Digits), bv_gt(S,0), bv_gt(M,0), B1 = Base**1, B2 = Base**2, B3 = Base**3, B4 = Base**4, % println([b1=B1,b2=B2,b3=B3,4=B4]), SEND = bv_sum([bv_mul(S,B3),bv_mul(E,B2),bv_mul(N,B1),D]), MORE = bv_sum([bv_mul(M,B3),bv_mul(O,B2),bv_mul(R,B1),E]), MONEY = bv_sum([bv_mul(M,B4),bv_mul(O,B3),bv_mul(N,B2),bv_mul(E,B1),Y]), bv_add(SEND,MORE).bv_eq(MONEY), Vars = Digits ++ SEND ++ MORE ++ MONEY, solve(Vars). % % Using scalar_product % sendmore2(Digits,SEND,MORE,MONEY) => sendmore2(10,Digits,SEND,MORE,MONEY). sendmore2(Base,Digits,SEND,MORE,MONEY) => Digits = make_bv_array(8,0,Base-1), Digits = {S,E,N,D,M,O,R,Y}, bv_all_different(Digits), bv_gt(S, 0), bv_gt(M, 0), Base4 = [1000,100,10,1], Base5 = [10000,1000,100,10,1], SEND = scalar_product_bv(Base4,[S,E,N,D]), MORE = scalar_product_bv(Base4,[M,O,R,E]), MONEY = scalar_product_bv(Base5,[M,O,N,E,Y]), bv_add(SEND,MORE).bv_eq(MONEY), Vars = Digits ++ SEND ++ MORE ++ MONEY, solve(Vars). print_solution(Base,Digits,SEND,MORE,MONEY) => nonvar(Digits), Digits = {S,E,N,D,M,O,R,Y}, println(digits=Digits.bti), if Base == 10 then println([send=SEND.bti,more=MORE.bti,money=MONEY.bti]) else println([send=SEND.bti,more=MORE.bti,money=MONEY.bti]), println([send=[S,E,N,D].bti,more=[M,O,R,E].bti,money=[M,O,N,E,Y].bti]) end, nl. % % With carry % % C4 C3 C2 C1 % S E N D % + M O R E % --------------- % = M O N E Y % sendmore_carry(Base,Digits,Carry) => Digits = make_bv_array(8,0,Base-1), Digits = {S,E,N,D,M,O,R,Y}, Carry = make_bv_array(4,0,Base-1), Carry = {C1,C2,C3,C4}, bv_all_different(Digits), S.bv_gt(0), M.bv_gt(0), C4.bv_eq(M), bv_add(C3,S).bv_add(M).bv_eq(bv_add(O,bv_mul(Base,C4))), bv_add(C2,E).bv_add(O).bv_eq(bv_add(N,bv_mul(Base,C3))), bv_add(C1,N).bv_add(R).bv_eq(bv_add(E,bv_mul(Base,C2,))), bv_add(D,E).bv_eq(bv_add(Y,bv_mul(Base,C1))), solve(Digits ++ Carry).