Abductive reasoning

During my first semester in KU Leuven I took a course “Logic as Foundations for AI”. There were only 4 participants, so instead of taking we could prepare an assignment.

One of the exercises consisted of performing some abductive reasoning, about boolean circuits where some logical gates could be broken (there were ~5 gates in the circuit). And it was tedious... And I was always making an error somewhere... So I decided: “enough is enough,” and wrote a Prolog program to solve this task for me.

And it was a great success: it took me only a day to write a program that solves a task it would take two hours to solve it (provided you were extremely pedantic).

(However, I've included my program into the assignment and I suspect it may have boosted the mark I received.) ;-)

:- op(1200, xfx, ====>).

% Give all the possible explanations for Goal in KB, as conjunctive clauses
explanations(Goal, KB, Explanations) :-
    prime_implicates(KB, Implications),
    no_goal(Goal, Implications, NoGs),
    findall(Explanation, (member(X, NoGs), negate_all(X, Explanation)), Explanations).


% find all the prime implicates from KB
prime_implicates(KB, Implicates) :-
    resolution(KB, Cons),
    findall(Imp, (member(Imp, Cons), prime_implicate_(Imp, Cons)), Implicates).

prime_implicate_(_, []).
prime_implicate_(I, [H|Set]) :-
    (   \+subset(H,I)
    ;   I ==H),
    prime_implicate_(I, Set).


% resolution(KB, AllResolvents).
resolution(List, Solution) :-
    % we have to sort the clauses in order to obtain the
    % “canonical” form (useful to remove duplicates).
    findall(Sorted, (member(L,List), sort(L,Sorted)), SortedList),
    resolution2(SortedList, Solution).

resolution2(List,Solution) :-
      member(A, List),
      member(B, List),
      A \==B,
   print(A),
      resolve(A, B, R1),
      sort(R1, R),
      \+ smember(R, List),
      pretty(A,B,R),
      resolution2([R|List], Solution)
      ;
      List=Solution.

resolve(XX,YY,Z) :-
 new_var(XX,X),
 new_var(YY,Y),
    member(Rx,X),
    member(Ry, Y),
%         (   Rx=not(Ry)
%         ;   Ry=not(Rx)),
     % We must use sound unification (no cyclic terms)
 (   unify_with_occurs_check(Rx, not(Ry))
 ;   unify_with_occurs_check(Ry, not(Rx))),
    select(Ry,Y, NewY),
    select(Rx, X, NewX),
    sunion(NewX, NewY, Z).

% prover by resolution for Horn Clauses
% hresolution(+Goal, +KB, -ResolutionTrail)
% prove Goal in KB

hresolution(Goal, KB, Sol) :-
    negate(Goal, NG),
    hresolution_(NG, KB, Sol).


hresolution_(_,[],[]).
hresolution_(X, KB, [X/Y====>Resolvent|Rest]) :-
    member(Y,KB),
    resolve(X,Y, Resolvent),
    (   Resolvent = [],
        Rest=[]
    ;
        select(Y,KB, NewKB),
        hresolution_(Resolvent, NewKB, Rest)).

/* *************************
*                         *
*   Tool predicates:      *
*                         *
***************************/

% put brand new new variables in the clause
new_var(X,Y) :-
    assert(p(X)),
    retract(p(Y)).

pretty(A,B,C) :- print(A/B====>C), nl, nl.


% like select, but uses sound unification and succeeds if El is not in
% the List
minus(_, [], []).
minus(X, [X1|Tail], Tail) :-
    sunifiable(X, X1).
minus(Elem, [Head|Tail], [Head|Rest]) :-
    minus(Elem, Tail, Rest).


% sound-unifiable
sunifiable(X,Y) :-
 \+ \+ unify_with_occurs_check(X,Y).

% like member, but tests identity instead of unification (we don't
% want to instantiate X in f(X) to 1 by checking if f(r) is already in
% the KB)


smember(X,[H|_]) :-
    %X==H.
 sunifiable(X, H).
smember(X, [_|Rest]) :-
    smember(X, Rest).

sunion([], L, L1) :-
 unify_with_occurs_check(L, L1),
 !.
sunion([H|T], L, R) :-
 smember(H, L), !,
 sunion(T, L, R).
sunion([H|T], L, [H|R]) :-
 sunion(T, L, R).

negate(not(X), X) :- !.
negate(X,not(X)).

% negate all literals in an disjunctive  clause, giving a conjunctive clause
negate_all([],[]).
negate_all([H|T],[NH|NT]) :-
    negate(H, NH),
    negate_all(T, NT).

% eliminate the goal Goal form the clause
no_goal(_, [], []).
no_goal(Goal, [H|T], [NH|NT]) :-
    minus(Goal, H, NH),
    no_goal(Goal, T, NT).


test(Z):-

    List = [
            [not(tennis_elbow), sore_elbow],
            [not(tennis_elbow), tennis_player],
            [not(arthritis), treated, sore_joints],
            [sore_elbow, not(sore_joints)],
            [not(sore_joints), sore_hips]
           ],
    List2 = [
             [not(p), not(q), not(r), g],
             [p, not(q), g],
             [q, not(r), g]
            ],
    explanations(g, List2,Z).

test_nonprovable(A) :-
 List = [[p(X)], [p(X)]],
 resolution(List, A).

test_plus(Solution, Result) :-
 A=[
    [rplus(W,0,W)],
    [rplus(X, s(Y), s(Z)), not(rplus(X,Y,Z))]
   ],

 Goal = [rplus(s(s(s(0))), s(s(0)), Result)],%s(s(s(s(s(0))))))],

 hresolution(Goal, A, Solution).

Sudoku

In the last week Prolog classes writing a sudoku solver was one of the exercises. Of course, this is not such a small task, so we concentrated on writing just a part of the solver. However, when I came home I felt the very strange feeling that I want to write my own sudoku solver. So here it is.

The representation I chose is a bit different from the ones I have seen in class and in the Internet. It is neither an array (Prolog emulation of an array using arg/3) of numbers, nor a plain list of numbers. It is a list of triples of the form X/Y/Value, where X and Y are the horizontal/vertical coordinates, and Value the number in the square. At first such a representation may seem a bit strange. However, it allows us (for example) to extract whole columns and rows through unification, which simplifies things a bit.

I have written the whole program with readability and conceptual simplicity in mind. This means it is not very efficient. I planned it to be as general as possible, so in principle it should be able to sort 27x27 sudoku. However, due to the lack of efficiency this may take quite a long time (provided you had a 27x27 grid partially filled with integers from 1 to 81, of course).

%
% all the elements in a column, row, 3x3 box.
%

column(X/_, Sudoku, Column) :-
 findall(X/Y/Z , (member(X/Y/Z, Sudoku), nonvar(Z)), Column).

row(_/Y, Sudoku, Row) :-
 findall(X/Y/Z, (member(X/Y/Z, Sudoku), nonvar(Z)), Row).


% believe me or not, this was the most difficult predicate to write.
box(Base, X/Y, Sudoku, Box) :- % Base: size of the puzzle
 DiffX is (X-1) mod (Base/3),
 DiffY is (Y-1) mod (Base/3),
 StartX is X - DiffX,
 StartY is Y - DiffY,
 EndX is StartX + (Base/3) - 1,
 EndY is StartY + (Base/3)-1,
 findall(X1/Y1/Z,
         (
          between(StartX,EndX,X1),
          between(StartY, EndY, Y1),
          member(X1/Y1/Z, Sudoku),
          nonvar(Z)
         ),
         Box).

%
% We can assign the value Possible to X/Y without
% violating the rules of the sudoku.
%
possible(_,X/Y/Possible, Sudoku) :-
 member(X/Y/Possible, Sudoku),
 nonvar(Possible), !.
possible(Base, X/Y/Possible, Sudoku) :-
 column(X/Y, Sudoku, Column),
 row(X/Y, Sudoku, Row),
 box(Base, X/Y, Sudoku, Box),
 between(1,Base, Possible),
 \+member(_/_/Possible, Column),
 \+member(_/_/Possible, Row),
 \+member(_/_/Possible, Box).

% solve the puzzle, iterating through each grid
solve(_,N,N,_).
solve(Base,N,K,Solution) :-
 nth1(N, Solution, X/Y/Z),
 possible(Base, X/Y/Z, Solution),
 NewN is N+1,
 solve(Base, NewN, K, Solution).
solve(Base,Solution) :-
 N is Base*Base+1,
 solve(Base,1, N, Solution).

% the main predicate
%
sudoku(Base,Constraints, Solution) :-
 findall(X/Y/_, (between(1,Base,X), between(1,Base,Y)), Solution),
 subset(Constraints, Solution),
 solve(Base,Solution).

/*

And some example puzzles to solve:

*/

s3([3/1/3, 2/2/8,
      5/1/4, 4/2/6, 6/2/3, 4/3/5,
      8/1/9, 8/3/4,
      1/4/5, 1/6/2, 3/6/7,
      4/4/9, 5/4/1, 4/5/2, 6/5/7, 5/6/8, 6/6/6,
      7/4/3, 9/4/7, 9/6/5,
      2/7/3, 2/9/5,
      4/8/7, 5/9/6, 6/7/5, 6/8/1,
      7/9/4, 8/8/5]).

% the sudoku from class
s1([1/4/2, 1/5/3, 1/9/5,
      2/2/4, 2/3/2, 2/5/9, 2/9/3,
      3/1/3, 3/6/8, 3/7/7,
      4/3/7, 4/8/5, 4/9/6,
      5/2/9, 5/4/7, 5/5/2, 5/8/1, 5/9/4,
      6/1/5, 6/4/9,
      7/1/6, 7/6/2, 7/7/8, 7/8/4, 7/9/9,
      8/3/8, 8/6/1, 8/9/7,
      9/1/2, 9/2/5, 9/6/9, 9/7/6]).

s2([4/1/2, 5/1/3, 9/1/5,
      2/2/4, 3/2/2, 5/2/9, 9/2/3,
      1/3/3, 6/3/8, 7/3/7,
      3/4/7, 8/4/5, 9/4/6,
      2/5/9, 4/5/7, 5/5/2, 8/5/1, 9/5/4,
      1/6/5, 4/6/9,
      1/7/6, 6/7/2, 7/7/8, 8/7/4, 9/7/9,
      3/8/8, 6/8/1, 9/8/7,
      1/9/2, 2/9/5, 6/9/9, 7/9/6]).

I also wrote print_su/1, a sudoku pretty-printer. It is not very interesting, and I used findall/3 to iterate through a list and print its elements (which may be considered abusive), so I decided not to publish it here :).

Now, we can use Prolog to run the following query:

?- s1(Constraints),sudoku(9,Constraints,Sudoku), print_su(Sudoku).

1  7  3 || 4  8  5 || 6  9  2
8  4  6 || 2  9  1 || 7  3  5
9  2  5 || 7  6  3 || 1  8  4
==============================
2  5  4 || 1  7  9 || 3  6  8
3  9  1 || 8  2  6 || 5  4  7
7  6  8 || 3  5  4 || 2  1  9
==============================
4  1  7 || 9  3  2 || 8  5  6
6  8  9 || 5  1  7 || 4  2  3
5  3  2 || 6  4  8 || 9  7  1

Constraints = [1/4/2, 1/5/3, 1/9/5, 2/2/4, 2/3/2, 2/5/9, 2/9/3, ... /... /3, ... /...|...]
Sudoku = [1/1/1, 1/2/8, 1/3/9, 1/4/2, 1/5/3, 1/6/7, 1/7/4, ... /... /6, ... /...|...] 

and voilà, your sudoku is ready!

(I think that it may be sensible using constraint logic programming for solving sudoku... However, I haven't reached the chapter about CLP in my book yet, so I didn't use it. ;-))

Is a goose worth sinning?

If there's a field, where Prolog is very good from first sight, it is no doubt solving logical puzzles. You know what I mean: those where you have to tell who owns the fish, how to measure two liters of water only with a bucket of 3 liters and one of 4 liters, solve a sudoku, and so on. Of course, Prolog will be able to deal only with purely combinatorial riddles--any involving self-reference or some dose of creativity are beyond its scope.

If one was to write it in an imperative programming language, it would take quite a lot of time to write a sound representation of the solution-space and then search through it; in Prolog, you just have to declare the rules which the world of the riddle must obey, and voilà!, it outputs the right answer.

For example, the Prolog code for solving the famous Einstein's riddle is quite straight forward (see also this solution):

%% the answer is a list of five houses, in the right order.
%% each house is a list of items in the following order:
%% [Color, Nationality, Beverage, Cigaretts, Pet]

left(L, R, [L | [R | _]]).
left(L, R, [_ | Rest]) :- left(L, R, Rest).

next(X,Y,List) :-
   left(Y,X,List).
next(X,Y,List) :-
   left(X,Y,List).

einstein(List,FishOwner) :-

   List=[_,_,[_,_,milk,_,_],_,_],
   List=[[_,norwegian,_,_,_],_,_,_,_],

   member([red, brit,_,_,_],List),
   member([_,swede,_,_,dog],List),
   member([_,dane,tea,_,_],List),
   left([green,_,_,_,_],[white,_,_,_,_],List),

   member([green,_,coffee,_,_],List),
   member([_,_,_,pall_mall,bird],List),
   member([yellow,_,_,dunhill,_],List),

   next([_,_,_,blends,_],[_,_,_,_,cat],List),
   next([_,_,_,_,horse],[_,_,_,dunhill,_],List),
   member([_,_,beer,bluemaster,_],List),
   member([_,german,_,prince,_],List),
   next([blue,_,_,_,_],[_,norwegian,_,_,_],List),
   next([_,_,_,blends,_],[_,_,water,_,_],List),
   member([_,FishOwner,_,_,fish],List),

   write('The '),write(FishOwner),write(' owns the fish.').

Unfortunately, not all simple riddles are so simple for Prolog as the latter one. A good example may be the fox, goose and bag of beans puzzle. It is one of my favorite puzzles (my father told me it when I was five and it was the first real puzzle I've ever solved), so it was quite obvious that this was going to be the second program I would write.

These rules govern the movement of the farmer and his stuff:

next(state([rolnik|Tail],X), state(Tail, [rolnik|X])).
next(state(X,[rolnik|Tail]), state([rolnik|X], Tail)).

(The constants are in Polish: rolnik = farmer, koza = goat (goose), kapusta = cabbage (bag of beans), wilk = wolf (fox).)

next(state([rolnik|Animals], Right), state(NewLeft,[rolnik|Rest])) :-
   member(X,Animals),
   delete(Animals, X, NewLeft),
   append([X],Right,Rest).

next(state(Left,[rolnik|Animals]), state([rolnik|Rest],NewRight)) :-
   member(X,Animals),
   delete(Animals, X, NewRight),
   append([X],Left,Rest).

Next, we write which states of the world are acceptable, and which not:

meal(koza,kapusta). % goats eat cabbage
meal(wilk,koza). % wolfs eat goats

not_good(Bank) :-
   \+member(rolnik,Bank),
   meal(X,Y),
   subset([X,Y],Bank).


good(state(X,Y)) :-
   \+not_good(X),
   \+not_good(Y).

and the constraints we want the solution to obey:

legal_chain([X]).

legal_chain([Car, Cadr|Tail]) :- % ah, Lisp reminiscences! :-)
   next(Car,Cadr),
   good(Cadr),
   legal_chain([Cadr|Tail]).

Now, the most intuitive thing we could do now would be to state something like this:

naive-solution(Solution) :-
   Solution = [state([rolnik, koza, kapusta, wilk], []) | _],
   legal_chain(Solution),
   last(Solution, state([], [rolnik, koza, kapusta, wilk]).

However, this definitely won't work. It may be perfectly correct from the declarative and logical point of view, but, as I have said in the previous post, Prolog is not logic. It doesn't automagically find the answer--it performs a depth-first search through the solution space. And in this case, the first path Prolog selects is one of the worst for us. The farmers goes to the other side of the river, returns, goes to the other side, and... Yes, ladies and gentlemen. An infinite loop.

Of course, it is possible to solve this problem in Prolog. The only think we have to do is think about our program more... well, as a program, not as a set of propositions, and change its search behavior. For example, we could implement an iterated, depth-first search (AFAIK, this was the least invasive way of altering my code so that it started to work).

(Well, it isn't precisely iterated depth-first (it looks for the answers only at the bottom o each layer), but the idea is quite the same.)

solve(Solution,N) :-
   (
    between(1,N,X),
    length(Solution,X),
    legal_chain([state([rolnik,koza,kapusta,wilk],[])|Solution]),
    last(Solution,state([],[rolnik,koza,kapusta,wilk]))
   ),!
;
   (
    NewN is N+1,
    solve(Solution,NewN)
   ).

solution(Solution) :-
solve(Solution,1).

You may have noticed that the program does nothing to avoid loops in the solutions. However, this is fine--for every “loopy” solution there exists a shorter one without loops, so we can be sure that the first solution we will find (the shortest one) is loop-free.

The last noteworthy thing is the cut operator (the red “!” in solve). Its task is to prevent backtracking after we have found a solution. It isn't really necessary--if you removed it, the program would just try to find other answers (and would find infinitely many of them--all except one loopy). Overusing it is considered very bad style in Prolog (as someone has said, “[cut] turns Prolog from a nice declarative language into a hybrid monster. Use cuts sparingly and with a sense of having sinned.”). However, I am still learning the language and couldn't resist the temptation of trying it, as soon as I found an adequate occasion. Yes, I am a sinner, and the goose was worth it. ;-)