River Crossing

We start with a standard river crossing puzzle in which we ferry everyone across the river with these rules:

Up to two people can fit on the boat.
The man cannot be with either girl without the woman.
The woman cannot be with either boy without the man.
The convict cannot be with anyone without the jailer.
The children and convict cannot ferry themselves.

We start by stating what symbols are possible. We will have 0 mean on the farside of the river and 1 mean the nearside, so the goal is for each individual to go from 0 to 1.

Sym{ 0 1 }

Now we want to define all of the variables which can be either 0 or 1.

Board{ Man Woman Boy1 Boy2 Girl1 Girl2 Jailer Convict Boat }

Next, we will state the initial state and end state of the world we are modeling.

Start{ 1 1 1 1 1 1 1 1 1 }
End{ 0 0 0 0 0 0 0 0 0 }

We can now define an object. Objects are used to represent a piece of the board for which we can define constraints or possible transitions. The object we will define now is the boat with two riders.

Obj BoatTwo { boat rider1 rider2 }

We can define the transitions that can be done to objects. The transition we are defining now is the boat going up or down.

Trans Up:BoatTwo { 1 1 1 => 0 0 0 }
Trans Down:BoatTwo { 0 0 0 => 1 1 1 }

Although we have defined the object, we have not yet matched it up to any board cells, we do this with DesObj. The Boat board cell will always be the boat object cell, but the riders can be different and are defined by our rules. # indicates a comment.

# woman and either girl
DesObj WomanGirl1:BoatTwo { Boat Woman Girl1 }
DesObj WomanGirl2:BoatTwo { Boat Woman Girl2 }

# man and either boy
DesObj ManBoy1:BoatTwo { Boat Man Boy1 }
DesObj ManBoy2:BoatTwo { Boat Man Boy2 }

# woman and man
DesObj WomanMan:BoatTwo { Boat Woman Man }

# jailer and anyone
DesObj JailerMan:BoatTwo { Boat Jailer Man }
DesObj JailerWoman:BoatTwo { Boat Jailer Woman }
DesObj JailerBoy1:BoatTwo { Boat Jailer Boy1 }
DesObj JailerBoy2:BoatTwo { Boat Jailer Boy2 }
DesObj JailerGirl1:BoatTwo { Boat Jailer Girl1 }
DesObj JailerGirl2:BoatTwo { Boat Jailer Girl2 }
DesObj JailerConvict:BoatTwo { Boat Jailer Convict }

Next, we need to define the boat with only one passenger.

Obj BoatOne { boat rider }
Trans Up:BoatOne { 1 1 => 0 0 }
Trans Down:BoatOne { 0 0 => 1 1 }

DesObj Man:BoatOne { Boat Man }
DesObj Woman:BoatOne { Boat Woman }
DesObj Jailer:BoatOne { Boat Jailer }

Now we need to forbid certain individuals from being together. In our model that means requiring that two variables have different values in certain conditions. We can do this using Req, which stands for Require.

This Req defines the first object cell as temporary variable a and the third object cell as temporary variable b. The middle object cell must either be a or anything except b.

Obj WithoutButWith { with without with }
Req WithoutButWith { a (a,!b) b }

Finally, we specify who is allowed to be with who, i.e. which board cells match up to which object cells.

# woman cannot be with either boy and without man
DesObj WithoutButWith { Man Woman Boy1 }
DesObj WithoutButWith { Man Woman Boy2 }

# man cannot be with either girl and without woman
DesObj WithoutButWith { Woman Man Girl1 }
DesObj WithoutButWith { Woman Man Girl2 }

# convict cannot be with anyone without jailer
DesObj WithoutButWith { Jailer Convict Man }
DesObj WithoutButWith { Jailer Convict Woman }
DesObj WithoutButWith { Jailer Convict Boy1 }
DesObj WithoutButWith { Jailer Convict Boy2 }
DesObj WithoutButWith { Jailer Convict Girl1 }
DesObj WithoutButWith { Jailer Convict Girl2 }

The solution can be resolved with this command indicating we try up to 20 stages.

./sabr 20 < source.tb

The overall program source and the resulting solution can be viewed below.

source | solution