The jobs puzzle: A challenge for logical expressibility and automated reasoning

The Jobs Puzzle, introduced in a book about automated reasoning, is a logic puzzle solvable by some "intelligent sixth graders," but the formalization of the puzzle by the authors was, according to them, "sometimes difficult and sometimes tedious." The puzzle thus presents a triple challenge: 1) formalize it in a non-difficult, non-tedious way; 2) formalize it in a way that adheres closely to the English statement of the puzzle; 3) have an automated general-purpose commonsense reasoner that can accept that formalization and solve the puzzle quickly. In this paper, I present and discuss three formalizations that are less difficult and less tedious than the original. However, none satisfy all three requirements as well as might be desired, and there are a significant number of automated reasoners that cannot solve the puzzle using any of the formalizations. So the Jobs Puzzle remains an interesting challenge.