Crossing the River Safely

For the sake of brain scrambling, we're going to solve this ancient puzzle using Imandra (again!). As most polyvalent farmers will tell you, going to the market with your pet wolf, tastiest goat, and freshest cabbage is sometimes difficult as they tend to have appetite for one another. The good news is that there is a way to cross this river safely anyway.

First we should define the problem by tallying our goods and looking around.

In [1]:
type location =
  | Boat
  | LeftCoast
  | RightCoast
  | Eaten

type boat =
  | Left
  | Right

type good = Cabbage | Goat | Wolf
Out[1]:
type location = Boat | LeftCoast | RightCoast | Eaten
type boat = Left | Right
type good = Cabbage | Goat | Wolf

This problem is delicate and will require multiple steps to be solved. Each step should take us from a state to another state (where, hopefully, no cabbage nor goat was hurt).

In [2]:
type state = {
  cabbage : location;
  goat : location;
  wolf : location;
  boat : boat;
}
Out[2]:
type state = {
  cabbage : location;
  goat : location;
  wolf : location;
  boat : boat;
}

We can define a few helpers:

In [3]:
let get_location (s:state) (g:good) = match g with
  | Cabbage -> s.cabbage
  | Goat -> s.goat
  | Wolf -> s.wolf

let set_location (s:state) (g:good) (l:location) = match g with
  | Cabbage -> { s with cabbage = l}
  | Goat    -> { s with goat    = l}
  | Wolf    -> { s with wolf    = l}

let boat_empty (s:state) =
  (s.cabbage <> Boat) &&
  (s.goat    <> Boat) &&
  (s.wolf    <> Boat)
Out[3]:
val get_location : state -> good -> location = <fun>
val set_location : state -> good -> location -> state = <fun>
val boat_empty : state -> bool = <fun>

Now, transition from a state to the next one is done via actions:

In [4]:
type action =
  | Pick of good
  | Drop of good
  | CrossRiver

let process_action (s:state) (m:action) : state =
  match m with
  | CrossRiver -> { s with boat = match s.boat with Left -> Right | Right -> Left }
  | Pick x -> begin
    if not @@ boat_empty s then s else
    match get_location s x, s.boat with
    |  LeftCoast ,  Left -> set_location s x Boat
    | RightCoast , Right -> set_location s x Boat
    | _ -> s
  end
  | Drop x -> begin
    match get_location s x, s.boat with
    | Boat ,  Left -> set_location s x LeftCoast
    | Boat , Right -> set_location s x RightCoast
    | _ -> s
  end
;;

let process_eating s =
  match s.boat, s.cabbage, s.goat, s.wolf with
  | Right, LeftCoast, LeftCoast, _    -> Some { s with cabbage = Eaten }
  | Right, _ , LeftCoast, LeftCoast   -> Some { s with goat = Eaten }
  |  Left, RightCoast, RightCoast, _  -> Some { s with cabbage = Eaten }
  |  Left, _ , RightCoast, RightCoast -> Some { s with goat = Eaten }
  | _  -> None

(* is… it a bad state? *)
let anything_eaten s =
  s.cabbage = Eaten || s.goat = Eaten

let one_step s a =
  if anything_eaten s then s
  else
    match process_eating s with
    | Some s -> s
    | None ->
      process_action s a

(* process many actions. Note that we have to specify that [acts] is
   the argument that proves termination *)
let rec many_steps s acts =
  match acts with
  | [] -> s
  | a :: acts ->
    let s' = one_step s a in
    many_steps s' acts
[@@adm 1n]


let solved s =
  s.cabbage = RightCoast
  && s.goat = RightCoast
  && s.wolf = RightCoast
  && s.boat = Right
;;
Out[4]:
type action = Pick of good | Drop of good | CrossRiver
val process_action : state -> action -> state = <fun>
val process_eating : state -> state option = <fun>
val anything_eaten : state -> bool = <fun>
val one_step : state -> action -> state = <fun>
val many_steps : state -> action list -> state = <fun>
val solved : state -> bool = <fun>
termination proof

Termination proof

call `many_steps (one_step s (List.hd acts)) (List.tl acts)` from `many_steps s acts`
original:many_steps s acts
sub:many_steps (one_step s (List.hd acts)) (List.tl acts)
original ordinal:Ordinal.Int (_cnt acts)
sub ordinal:Ordinal.Int (_cnt (List.tl acts))
path:[acts <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
num checks:8
arith assert lower:14
arith tableau max rows:5
arith tableau max columns:15
arith pivots:8
rlimit count:2723
mk clause:29
datatype occurs check:22
mk bool var:119
arith assert upper:12
datatype splits:14
decisions:36
arith row summations:9
propagations:30
conflicts:13
arith fixed eqs:5
datatype accessor ax:17
arith conflicts:2
arith num rows:5
arith assert diseq:1
datatype constructor ax:33
num allocs:7006204
final checks:6
added eqs:117
del clause:12
arith eq adapter:13
memory:17.340000
max memory:17.340000
Expand
  • start[0.010s]
      let (_x_0 : int) = count.list count.action acts in
      let (_x_1 : action list) = List.tl acts in
      let (_x_2 : int) = count.list count.action _x_1 in
      acts <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
      ==> not (_x_1 <> [])
          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into:
    let (_x_0 : action list) = List.tl acts in
    let (_x_1 : int) = count.list count.action _x_0 in
    let (_x_2 : int) = count.list count.action acts in
    not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
    || not (acts <> [] && (_x_2 >= 0) && (_x_1 >= 0))
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • unroll
        expr:
        (|Ordinal.<<| (|Ordinal.Int_79/boot|
                        (|count.list_431/server|
                          (|ge…
        expansions:
        • unroll
          expr:
          (|count.list_431/server| (|get.::.1_411/server| acts_419/server))
          expansions:
          • unroll
            expr:
            (|count.list_431/server| acts_419/server)
            expansions:
            • Unsat
            In [5]:
            (* initial state, on the west bank of Anduin with empty pockets and fuzzy side-kicks *)
            let init_state = {
              cabbage = LeftCoast;
              goat = LeftCoast;
              wolf = LeftCoast;
              boat = Left;
            }
            
            Out[5]:
            val init_state : state =
              {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
            

            We are now ready to ask for a solution! Because we're looking for a given solution rather than a universal proof, instance is the most natural.

            In [6]:
            #timeout 10_000;;
            
            instance (fun l -> solved @@ many_steps init_state l) ;;
            
            Out[6]:
            - : action list -> bool = <fun>
            module CX : sig val l : action list end
            
            Instance (after 18 steps, 22.152s):
            let l : action list =
              let (_x_0 : action) = Pick Goat in
              let (_x_1 : action) = Drop Goat in
              [_x_0; CrossRiver; _x_1; CrossRiver; Pick Cabbage; CrossRiver;
               Drop Cabbage; _x_0; CrossRiver; _x_1; Pick Wolf; CrossRiver; Drop Wolf;
               CrossRiver; _x_0; CrossRiver; _x_1]
            
            Instance
            proof attempt
            ground_instances:18
            definitions:0
            inductions:0
            search_time:
            22.152s
            details:
            Expand
            smt_stats:
            num checks:37
            rlimit count:41264010
            mk clause:73846
            datatype occurs check:1252
            restarts:427
            mk bool var:1189718
            datatype splits:1775421
            decisions:273861
            propagations:7381888
            conflicts:72393
            datatype accessor ax:10296
            minimized lits:838431
            datatype constructor ax:1425341
            final checks:36
            added eqs:18965317
            del clause:51345
            dyn ack:39
            time:2.685000
            memory:326.400000
            max memory:327.770000
            num allocs:68325077851.000000
            Expand
            • start[22.152s]
                let (_x_0 : state)
                    = many_steps
                      {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
                      ( :var_0: )
                in
                (_x_0.cabbage = RightCoast)
                && ((_x_0.goat = RightCoast)
                    && ((_x_0.wolf = RightCoast) && (_x_0.boat = Right)))
            • simplify

              into:
              let (_x_0 : state)
                  = many_steps
                    {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
                    ( :var_0: )
              in
              (_x_0.cabbage = RightCoast) && (_x_0.goat = RightCoast)
              && (_x_0.wolf = RightCoast) && (_x_0.boat = Right)
              expansions:
              []
              rewrite_steps:
                forward_chaining:
                • unroll
                  expr:
                  (many_steps_1315/client
                    (|rec_mk.state_468/server|
                      LeftCoast_1246/client
                      LeftCoast_1246/cl…
                  expansions:
                  • unroll
                    expr:
                    (many_steps_1315/client
                      (one_step_1311/client
                        (|rec_mk.state_468/server|
                          LeftCoast_1246/…
                    expansions:
                    • unroll
                      expr:
                      (many_steps_1315/client
                        (one_step_1311/client
                          (one_step_1311/client
                            (|rec_mk.state_468/s…
                      expansions:
                      • unroll
                        expr:
                        (let ((a!1 (one_step_1311/client
                                     (one_step_1311/client
                                       (one_step_1311/cl…
                        expansions:
                        • unroll
                          expr:
                          (let ((a!1 (one_step_1311/client
                                       (one_step_1311/client
                                         (one_step_1311/cl…
                          expansions:
                          • unroll
                            expr:
                            (let ((a!1 (one_step_1311/client
                                         (one_step_1311/client
                                           (one_step_1311/cl…
                            expansions:
                            • unroll
                              expr:
                              (let ((a!1 (one_step_1311/client
                                           (one_step_1311/client
                                             (one_step_1311/cl…
                              expansions:
                              • unroll
                                expr:
                                (let ((a!1 (one_step_1311/client
                                             (one_step_1311/client
                                               (one_step_1311/cl…
                                expansions:
                                • unroll
                                  expr:
                                  (let ((a!1 (one_step_1311/client
                                               (one_step_1311/client
                                                 (one_step_1311/cl…
                                  expansions:
                                  • unroll
                                    expr:
                                    (let ((a!1 (one_step_1311/client
                                                 (one_step_1311/client
                                                   (one_step_1311/cl…
                                    expansions:
                                    • unroll
                                      expr:
                                      (let ((a!1 (one_step_1311/client
                                                   (one_step_1311/client
                                                     (one_step_1311/cl…
                                      expansions:
                                      • unroll
                                        expr:
                                        (let ((a!1 (one_step_1311/client
                                                     (one_step_1311/client
                                                       (one_step_1311/cl…
                                        expansions:
                                        • unroll
                                          expr:
                                          (let ((a!1 (one_step_1311/client
                                                       (one_step_1311/client
                                                         (one_step_1311/cl…
                                          expansions:
                                          • unroll
                                            expr:
                                            (let ((a!1 (one_step_1311/client
                                                         (one_step_1311/client
                                                           (one_step_1311/cl…
                                            expansions:
                                            • unroll
                                              expr:
                                              (let ((a!1 (one_step_1311/client
                                                           (one_step_1311/client
                                                             (one_step_1311/cl…
                                              expansions:
                                              • unroll
                                                expr:
                                                (let ((a!1 (one_step_1311/client
                                                             (one_step_1311/client
                                                               (one_step_1311/cl…
                                                expansions:
                                                • unroll
                                                  expr:
                                                  (let ((a!1 (one_step_1311/client
                                                               (one_step_1311/client
                                                                 (one_step_1311/cl…
                                                  expansions:
                                                  • unroll
                                                    expr:
                                                    (let ((a!1 (one_step_1311/client
                                                                 (one_step_1311/client
                                                                   (one_step_1311/cl…
                                                    expansions:
                                                    • Sat (Some let l : action list = let (_x_0 : action) = Pick Goat in let (_x_1 : action) = Drop Goat in [_x_0; CrossRiver; _x_1; CrossRiver; Pick Cabbage; CrossRiver; Drop Cabbage; _x_0; CrossRiver; _x_1; Pick Wolf; CrossRiver; Drop Wolf; CrossRiver; _x_0; CrossRiver; _x_1] )

                                                    That seems to take a bit of time, because this problem is not that easy for Imandra's unrolling algorithm. Let's try [@@blast] to see if we can get a result faster:

                                                    In [7]:
                                                    instance (fun l -> solved @@ many_steps init_state l)
                                                    [@@blast] ;;
                                                    
                                                    Out[7]:
                                                    - : action list -> bool = <fun>
                                                    module CX : sig val l : action list end
                                                    
                                                    Instance (after 72 steps, 0.169s):
                                                    let l : action list =
                                                      let (_x_0 : action) = Pick Goat in
                                                      let (_x_1 : action) = Drop Goat in
                                                      [_x_0; CrossRiver; _x_1; CrossRiver; Pick Wolf; CrossRiver; Drop Wolf;
                                                       _x_0; CrossRiver; _x_1; Pick Cabbage; CrossRiver; Drop Cabbage;
                                                       CrossRiver; _x_0; CrossRiver; _x_1]
                                                    
                                                    Instance

                                                    It only took a fraction of second! 🎉

                                                    Now we have a clear plan for crossing the river. How to sell the goat and cabbage is left as an exercise to the reader.