Note that there are several equally short solutions to this problem, so if you get more than one solution, that’s not necessarily a bug in your specification!

Some of the assumptions in this problem are that the river crossings are instantaneous and that whenever the boat reaches one of the banks, everyone on board gets out (i.e. you don’t need to consider times at which some of the people are in the boat and you can’t save missionaries by having cannibals stay on board, etc). Also, to make the problem work, none of the people can swim, or fly, or teleport, or jump across, or walk on water. The boat cannot move on its own, without someone on board to row it. There are no spare boats, and no, there are no islands in this river!

You may find that you have coded it inefficiently, so that the solver times out before producing a solution. If that happens, things to try are:

• Reduce the number of function values that need to be computed. For instance, a binary function on a domain of 6 objects requires 36 values to be fixed. A unary function is more efficient than a binary relation, and a binary function is more efficient than a ternary relation, even if logically they are equivalent.
• Reduce the length of constraints. The “length” of a constraint is the number of distinct function values that have to be fixed before it can be eveluated. Ten constraints of length 3 are usually more efficient than one of length 4. Sometimes it is possible to split up a long constraint into two or more short ones without introducing too many new function symbols. Remember that the constraints will be rewritten to clause form before being sent to the solver, and what counts is the length of the clauses rather than the formulae you write. Use the “print job” setting to see the clauses.
• Get the function symbols in the right order. The solver generally prefers to fix the values of functions in the order in which they were declared (earliest ones first). So if one function is trivially derivable given some of the others, declare it after them.
• Wherever possible, use names from an enumeration list (given in a sort declaration) rather than those introduced as constants in the “Functions” box. Within clauses, the two kinds of name are syntactically similar, but they are treated very differently inside the solver.
• Don’t over-use the “int” sort. In this problem, for instance, it is better to define a sort “state” than to use integers to enumerate the successive states. The problem with integers is that there are a lot of them! This can cause the solver to run a lot slower than it would if you used a (small) finite domain defined in the “sorts” box.
• If you do use numbers, for instance to count the cannibals, add a constraint saying that the count is always less than 4 (or whatever the known upper bound may be). This can save a lot of time.