Syndicate: Cannibals versus Missionaries.txt

[404 <404@jodi.org>]

\ Cannibals versus Missionaries.txt

\
\ A band of three missionaries and three cannibals must cross
\ a river.  Their boat can only hold two persons.  If, at any time,
\ cannibals outnumber missionaries on one bank or the other, then
\ the cannibals will eat the missionaries.  Can the party find
\ a sequence of boat traversals which will allow the group to
\ attain the opposite bank without any change in population?

Logic: HyperRes;                        \ hyperresolution
Predicate: situ;                        \ situation
Function: MW,CW;          \ Missionaries on West, Cannibals on West
Function: B,ME,CE;        \ Boat, Missionaries/Cannibals on East
Constant: w,e;            \ West, East

Axiom:
\ You can move two missionaries from west to east:
~situ(MW(x),CW(x1),B(w),ME(x2),CE(x3)) |
  situ(MW(x - 2),CW(x1),B(e),ME(x2 + 2),CE(x3)) |
  unless((x - 2) < 0) |
  unless(((x - 2) > 0) & ((x - 2) < x1)) |
  unless((x2 + 2) < x3) ;
\
\ You can move two missionaries from east to west:
~situ(MW(x),CW(x1),B(e),ME(x2),CE(x3)) |
  unless((x2 - 2) < 0) |
  unless(((x2 - 2) > 0) & ((x2 - 2) < x3)) |
  unless((x + 2) < x1) |
  situ(MW(x + 2),CW(x1),B(W),ME(x2 - 2),CE(x3));
\
\ You can move two cannibals from west to east:
~situ(MW(x),CW(x1),B(w),ME(x2),CE(x3)) |
  unless((x1 - 2) < 0) |
  unless((x2 > 0) & (x2 < (x3 + 2))) |
  situ(MW(x),CW(x1 - 2),B(e),ME(x2),CE(x3 + 2));
\
\ You can move two cannibals from east to west:
~situ(MW(x),CW(x1),B(e),ME(x2),CE(x3)) |
  unless((x3 - 2) < 0) |
  unless((x > 0) & (x < (x1 + 2))) |
  situ(MW(x),CW(x1 + 2),B(w),ME(x2),CE(x3 - 2));
\
\ You can move one cannibal and one missionary from west to east:
~situ(MW(x),CW(x1),B(w),ME(x2),CE(x3)) |
  unless((x - 1) < 0) |
  unless((x1 - 1) < 0) |
  unless(x2 < x3) |
  situ(MW(x - 1),CW(x1 - 1),B(e),ME(x2 + 1),CE(x3 + 1));
\
\ You can move one cannibal and one missionary from east to west:
~situ(MW(x),CW(x1),B(e),ME(x2),CE(x3)) |
  unless((x2 - 1) < 0) |
  unless((x3 - 1) < 0) |
  unless(x < x1) |
  situ(MW(x + 1),CW(x1 + 1),B(w),ME(x2 - 1),CE(x3 - 1));
\
\ You can move one cannibal from west to east:
~situ(MW(x),CW(x1),B(w),ME(x2),CE(x3)) |
  unless((x1 - 1) < 0) |
  unless((x2 > 0) & (x2 < (x1 + 1))) |
  situ(MW(x),CW(x1 - 1),B(e),ME(x2),CE(x3 + 1));
\
\ You can move one cannibal from east to west:
~situ(MW(x),CW(x1),B(e),ME(x2),CE(x3)) |
  unless((x3 - 1) < 0) |
  unless((x > 0) & (x < (x1 + 1))) |
  situ(MW(x),CW(x1 + 1),B(w),ME(x2),CE(x3 - 1));
\
\ You can move one missionary from west to east:
~situ(MW(x),CW(x1),B(w),ME(x2),CE(x3)) |
  unless((x - 1) < 0) |
  unless((x2 + 1) < x3) |
  unless(((x - 1) > 0) & ((x - 1) < x1)) |
  situ(MW(x - 1),CW(x1),B(e),ME(x2 + 1),CE(x3));
\
\ You can move one missionary from east to west:
~situ(MW(x),CW(x1),B(e),ME(x2),CE(x3)) |
  unless((x2 - 1) < 0) |
  unless(((x2 - 1) > 0) & ((x2 - 1) < x3)) |
  unless((x + 1) < x1) |
  situ(MW(x + 1),CW(x1),B(w),ME(x2 - 1),CE(x3));
\
Assert:
\ Initial situation: 3 missionaries & 3 cannibals on west.
situ(MW(3),CW(3),B(w),ME(0),CE(0));

\ Objective: 3 missionaries and 3 cannibals on east.
\ (We claim that it can't be achieved -- that way, when it is
\ achieved, the inference process will detect a contradiction and stop.)
~situ(MW(0),CW(0),B(e),ME(3),CE(3));

LimitF: 10;
LimitV: 10;
LimitC: 20;