Problem solving with linear implication

Linear implication is a serious and very convenient problem solving tool, which allows avoiding explicit handling of complex data-structures. Let's suppose we want to walk through a (possibly circular) graph structure without looping.

With linear implication this becomes: 

path(X,X,[X]).
path(X,Z,[X|Xs]):-linked(X,Y),path(Y,Z,Xs).

linked(X,Y):-c(X,Ys),member(Y,Ys).

go(Xs):-
  c(1,[2,3]) -: c(2,[1,4]) -: c(3,[1,5]) -: c(4,[1,5]) -:
  path(1,5,Xs).

or 

path(X,X,[X]).
path(X,Z,[X|Xs]):-c(X,Y),path(Y,Z,Xs).

% data

go(Xs):-
  (c(1,X1):-c1(X1)) -: 
  (c(2,X2):-c2(X2)) -: 
  (c(3,X3):-c3(X3)) -: 
  (c(4,X4):-c4(X4)) -:
  path(1,5,Xs).

c1(2).
c1(3).

c2(1).
c2(4).

Some finite domain constraint solving can also be done quite efficiently (1.3 seconds on a Sparc 10-20 for the SEND + MORE = MONEY puzzle - see file progs/lconstr.pl). 

% Program: linear implication based FD constraint solving
% Author: Paul Tarau, 1995

% cryptarithmetic puzzle solver -see progs/lconstr.pl
% a kind of "constraint solving with linear implication"

example1(
   [s,e,n,d,m,o,r,e,y]=[S,E,N,D,M,O,R,E,Y],
   [S,E,N,D]+
   [M,O,R,E]=
 [M,O,N,E,Y],
 _
).

% Addition of two numbers - simplified version -
sum(As, Bs, Cs) :- sum(As, Bs, 0, Cs).

sum([], [], Carry, [Carry]).
sum([A|As], [B|Bs], Carry, [C|Cs]) :- !,
	add2digits(A,B,Carry,C,NewCarry),
        sum(As, Bs, NewCarry, Cs).

add2digits(A,B,Carry,Result,NewCarry):-
  bind(A),bind(B),
  add_with_carry(10,A,B,Carry,Result,NewCarry).

add_with_carry(Base,A,B,Carry,Result,NewCarry):-
  S is A+B+Carry,
  Result is S mod Base,
  NewCarry is S // Base,
  new_digit(Result).

bind(A):-var(A),!,digit(A).
bind(_).

new_digit(A):-digit(A),!.
new_digit(_).

solve(As,Bs,Cs,Z):-
  digit(0)-:digit(1)-:digit(2)-:digit(3)-:digit(4)-:digit(5)-:
  digit(6)-:digit(7)-:digit(8)-:digit(9)-:
  ( sum(As,Bs,Cs),
    Z>0
  ).

puzzle:-
    init(Vars,Puzzle,Names),
    Puzzle=(Xs+Ys=Zs),Zs=[Z|_],
    reverse(Xs,As),                   % see progs/lconstr.pl
    reverse(Ys,Bs),
    reverse(Zs,Cs),
      solve(As,Bs,Cs,Z),
      show_answer(Vars,Names,Puzzle), % see progs/lconstr.pl
    fail.
puzzle:-
    write('no (more) answers'),nl,nl.

go:-
  (init(X,Y,Z):-example1(X,Y,Z))-:puzzle,
  fail.

Notice how linearly assumed digit/1 facts are consumed by bind/1 and new_digit/1 to enforce constraints as early as possible inside the addition loop.