Developing configurations and solutions for logical puzzles with UML and OCL

A typical logical puzzle, namely a problem that can be solved through deductive reasoning, is shown in Fig. 1. The left upper part visualizes the possible puzzle solutions, and in the left lower part four clues are stated that determine the solution. The right part represents the puzzle in the form of a UML and OCL class model along with OCL invariants that determine exactly one allowed object diagram. The UML and OCL representation is only shown to make the puzzle precise and to show a possible puzzle implementation. One does not need OCL to understand the puzzle task. Often, for better motivation, the puzzle is embedded into a real-life context. In this example, the puzzle could be stated as follows:

Bild vergrößern

Here, observations are stated in the form of conditional statements, as shown in Fig. 1. Statements could also be non-conditional (like \(\mathtt{{top<>blue}}\), i.e., the top of the car was not blue). In this case, the task for the person solving the puzzle, say the police inspector, is to identify on the basis of the observations the top and body color of the car. Here, this is possible and leads to a unique solution, if done properly. Not all sets of clues do have a solution or do have a single solution. This depends on the stated clues.

To model this puzzle, we use the USE tool [8, 9]) which provides us with facilities to construct UML class models with OCL constraints. USE supports both textual and visual representation of models, enabling the analysis and inspection of model properties through derivation and deduction. The goal in the tool USE is the prediction of system properties from the model before actually building an implementation. USE offers to the developer a graphical user interface (GUI) and a command line interface (CLI). Models that are class-oriented (class and protocol state-machine models) and that are instance-oriented (object models as well as sequence and communication models) can be studied in USE. A model finder for class models including OCL invariants supports object model finding and partial object model completion. Thus, the tool comprises (1) an OCL evaluator that determines the value of an OCL expression in an object model (object diagram), and (2) a model finder, that automatically constructs object models for a given class model and a set of OCL invariants or reports unsatisfiable, if contradicting constraints are stated, for example.

The elements from Fig. 1 are formally represented as automatically generated (details will follow later in Sect.  3) USE objects as shown in Fig. 2. The UML and OCL parts from the right of Fig. 1 possess a formal counterpart in Fig. 2. For example, a color is represented as a possible value entry of a Property object. Each of the nine possible solutions is shown as a Thing object and each of the four clues as a Clue object. Property objects with attributes name and value describe Thing objects, e.g., thing3 is linked to two Property objects, the first one property3 with name= ’top’ and value=’red’ and the second one property5 with name=’body’ and value=’red’. In order to simplify the diagram, four property objects are hidden. The puzzle solution is represented by the yellow marked Thing object thing3 that is the only Thing object satisfying all clues. The remaining Thing objects are not solutions to the puzzle and this is indicated by a list of banning clues in the northeast object rectangle corner (details on how to achieve the solution will follow later in Fig. 3).

Bild vergrößern

Bild vergrößern

In the lower part of Fig. 2, four OCL queries and their results are shown. The queries discover central aspects of our approach.

A systematic method for solving the puzzle is shown in Fig. 3. To illustrate the method, the possible puzzle solutions already shown in Fig. 1 are presented four times but complemented by additional features to indicate each step in the process. In each of the steps, one clue is applied and the result is captured by the black and gray tokens inside one of the nine possible solutions: All elements in Fig. 3 taken together give a systematic, substantial overview on the development of the solution. Colors of the tokens indicate the impact of applying the current clue and the previous clues. The fact that the second clue does not ban any possible solution is reflected in Fig. 2 by the circumstance that the fourth OCL query gives for clue2 as the result the empty set Set . The fact that some clues are banning more than one possible solution is reflected by the circumstance that two clues are occuring in the northeast corners of the Thing rectangles. Finally, the property of being definitively a solution is reflected in the figure by the circumstance that the Thing object thing3 does not have any banning Clue list in its northeast corner; the property of being a unique solution is reflected by the circumstance that object thing3 is the only Thing object without a banning Clue list in its northeast corner. Here, we have applied the clues in the order of their object identity (clue1, clue2,...). However, one could apply the clues in any order, leading to a different order and color for the marks, but leading to the same solution thing3 and banning the same possible solutions.

Bild vergrößern

Our approach relies on a UML class model (metamodel), and a puzzle is modeled explicitly with an accompanying object model. In Fig. 4, the USE class model and informal explanations for model elements are presented. These elements have already appeared in the object model in Fig. 2 in the form of examples. Now, we discuss the classes Thing, Property and Clue in a systematic way, mostly independent from an example.

A Thing object (e.g., a car with particular top and body color) represents a possible solution for a modeled logical puzzle. A thing can be linked through the association ThingProperty to Property objects which describe with name-value pairs relevant, puzzle domain-specific aspects of a thing (e.g., a car with top-red and body-blue). A Property can state that a linked thing has for the property name the shape value and can be a universal attribute in the considered domain. In order to give a fresh example different from the used car domain, in a puzzle about potentially poisoned dinner courses there could be course properties like name = ’Starter’ with value=’Soup’ representing the course Starter=Soup or properties like name=’Dessert’ with value=’Fruit’ representing the course Dessert=Fruit. A set of Clue objects give hints in order to identify a unique solution among the possible solutions, i.e., the set of things constituting the puzzle (e.g., (1) clue: if the car top is not blue, then the car body is green; (2) clue: the car body is not red). Clues refer to properties and can be (1) conditional with a premise prem and a conclusion conc (e.g., \(\mathtt{{top='red' => body='green'}}\)) or (2) unconditional (e.g., body = ’red’) in which case premise and conclusion are required to coincide in the formal object representation. Both premise and conclusion can be indicated as being negated with Boolean flags.

Bild vergrößern

In Fig. 4, the model operations and the needed model invariants are sketched. The model operations allow to express central model functionalities in a compact way:The invariants are listed in the order of their context class and their name, additionally classifying them as belonging to (1) syntax, (2) semantics or (3) the loaded invariants (e.g., user defined). Although all invariants have formally the same shape as universally quantified formulas over the context class, we are distinguishing between syntax and semantics because the invariants serve different roles: Invariants about syntax make restrictions about the formal representation of entities from the puzzle and clue domain (e.g., all properties are syntactically different in the sense that no two different properties have the same attribute values for name and value); invariants about semantics restrict evaluations and properties of entities from the problem domain (e.g., how clues are evaluated in the possible solutions and how that evaluation is related to the Thing attribute banned; a central semantic invariant requires that there is only one valid solution, i.e., one Thing in which all Clue objects evaluate to true). The seven syntax invariants handle: (1) clue representation, (2) uniqueness of clues, (3) linking properties to things, (4) unique name-value pairs for properties, (5) linking things to properties, (6) things having unique properties and (7) thing properties referring to properties with different names. The two semantic invariants handle: (1) things where all clues are valid being not banned, and (2) existence of a unique solution in which all clues are valid. Finally, loaded invariants allow the user to add puzzle-specific constraints. In this case, the single loaded invariant requires that one particular solution among the nine possible solutions is chosen: Top and body of the car must be red. If this invariant is not given, the system will just pick one solution arbitrarily.

One central model functionality is realized by the operation Thing::valid(c:Clue):Boolean. In the context of a potential puzzle solution, in formal terms a Thing object, the operation checks whether a parameter Clue, which is basically a primitive formula over a potential solution, is valid in the potential solution or is not valid, where the operation result is determined by the Boolean return type. The operation must consider the different syntactical options for building a Clue, where the syntactical options are determined by choices between (a) conditional or non-conditional clue, (b) premise negation or premise affirmation and (c) conclusion negation or conclusion affirmation.

Bild vergrößern

In Fig. 5, all six options for building and representing puzzle clues are shown. In the left column, the two options for expressing unconditional clues are pictured, and in the right column, the four options for conditional clues are displayed. In each of the two columns, the clues are first shown in textual form and then in the form of the corresponding object model representation. Basically, the left textual representation coincides with the value of the derived attribute toStr in a Clue object. The different options in both columns arise due to choices for negation or affirmation of the Clue condition with respect to the Clue premise and conclusion.

Bild vergrößern

In Fig. 6, the implementation of the operation Thing::valid(...) is shown. As indicated within comments, the implementation distinguishes the six cases for clues as presented in Fig. 5. Let us consider in more detail one prototypical example case, a conditional clue with equality in the premise and in the conclusion: \(\mathtt{{nameP=valueP =>}}\) \({nameC=valueC}\). This case is implemented lines 10–14. (1) In line 12, the premise property name c.prem.name is used to obtain the value of the property in the current thing (nameP). Then, it is checked whether the premise property is equal to the premise value obtained with c.prem.value (valueP). (2) For the conclusion, a similar procedure is followed (line 14). The conclusion property nameC and the conclusion value valueC are determined (using the expressions t.value(c.conc.name and c.conc.value, respectively). Then, it is checked whether the conclusion property is in the current Thing equal to the conclusion value. (3) Last, the implication expressed in the clue is checked by evaluating the left and right hand side (i.e., implies in OCL). The other five cases work in an analogous way with negation or affirmation of clue conditions respected by applying equality or inequality checks at appropriate spots.

As is detailed in Fig. 6, the operation Thing:: cluesValid():Set(Thing) returns the set of all Thing objects in which all clues are valid. The operation does not use or rely on a self-object and is thus independent from the Thing object on which it is called. It can be applied for characterizing solutions, because all clues are assumed to be valid in a solution. If the puzzle is required to have a unique solution, this unique solution must be included in the operation result because it must be valid for all clues. Two further, central invariants, which apply cluesValid() in an essential way, contribute to the core of the model, namely the two invariants that we have called semantic invariants before, because they restrict the way attribute values and links have to be evaluated. Both invariants use the Boolean-valued Thing attribute banned: The purpose of this attribute is to mark a Thing object, i.e., to mark a possible solution, as being banned or, in other words, as being unusable as a solution. (1) The invariant Thing::thingsWithCluesValid_EQ_thingsNot Banned asserts that the set of valid Thing objects is exactly the set of Thing objects that are not banned, i.e., things t with t.banned=false. (2) The invariant Thing::oneThingWithCluesValidNotBanned guarantees the existence of a unique solution by requiring that among all Thing objects, in which all clues are valid, there is exactly one Thing object that is not banned, namely the unique solution.

Our puzzle model is a general model to build logical puzzles and we use an OCL solver, the USE model finder, to construct puzzle instances automatically. The solver requires information about which values are permitted in the solution, the number of possible solutions and optional additional constraints about the puzzle not captured by the puzzle by the puzzle model.

In our approach, a puzzle can be configured in a number of ways: One can use (1) the properties file in order to specify the basic underlying puzzle terminology and the number of possible solutions, and (2) additional invariants to restrict possible solutions regarding the puzzle terminology or regarding the form or the extent of puzzle clues.

In the properties file, one can determine for the class Property the items that are used for the attributes name and value. In our running example, we have used top and body for the attribute name, and red, blue and green for the attribute value. One can also specify bounds for the number of objects in a class and the number of links in an association. In the example, we have restricted the number of Thing objects to 9, the number of Property objects to 6 and the number of ThingProperty links to 18, resulting in 2 links per Thing object and 3 links per Property object. Additionally, in order to restrict the puzzle options, one can use particular invariants to be loaded that regulate name-value dependencies, similar to introducing value types for properties. For example, one could have an invariant that restricts the body color to black and white and the top color to gold and silver, if desired.

Bild vergrößern

Puzzle configuration with additional invariants might also handle puzzle features which are independent from the puzzle domain at hand. Invariants can restrict the features of the puzzle solution by considering the form and number of used clues: As clues can be conditional or unconditional, invariants might require a certain number of clues in each category. For example, it is possible to demand that all clues are conditional. We have seen in examples, clues do not necessarily ban things, i.e., a clue might not exclude any possible solution at all. For instance, the clue \(\mathtt{{body=green => body<>red}}\) in the running example was such a clue. Such clues can make the puzzle purposefully more complicated, if this is desired, and the identification of such clues is part of the teaching concept. Additional invariants might require to exclude or to include such clues. Lastly, our invariant that insists on a unique solution is debatable: Instead of requiring exactly one solution, a replacing invariant could require that two or three solutions are allowed.

Our model is a not only a model, but we classify it as a metamodel. The assessment that we are working with a metamodel is already present in Figs. 1 and 2: the UML and OCL class model from the right of Fig. 1 is represented in Fig. 2 as an object model that instantiates the meta class model from Fig. 4. Basically, the object model in Fig. 2 and the class model in Fig. 1 are different views on the same matter, on the same circumstances.

Our model can be regarded as a multi-level model, but it is implemented in a two-level framework (with class and object model) as it is available in USE. Some background on multi-level and two-level approaches can be found in [15]. In this setting, the Property class behaves as an ontological element (i.e., it describes elements from the application domain), and invariants optionally added by the user allow to restrict allowed values in the application domain for each property. As an example, if one would extend our car example with a property engine allowing values like petrol and electric, one could guarantee by restriction through an OCL invariant, the top property takes only values like red and the engine property values like electric, but the engine property will never take a value like green; an invariant realizes the restriction of values per property type. Please note adding OCL invariants is optional, and many puzzles can be built without the need for OCL. The Clue class behaves like a linguistic element which allows our system to impose ‘universal puzzle constraints’ over the application objects. For the distinction between ontological and linguistic elements, see [1].

As an example for the nature of our metamodel, when the class Clue is instantiated, one does not obtain directly a clue in the shape of a formula like \(\mathtt{{forAll c:Car c.body<>}}\) \(\mathtt{{(red}}\). But, in a well-formed puzzle model, one obtains two objects c:Clue and p:Property with c.prem=p, c.negatedP=true, c.conc=p, c.negatedC=true, p.name=’body’, and p.value=’red’. The object p:Property belongs to the application domain (describes a car), whereas c:Clue models actually a constraint over the properties which has been automatically derived according to the puzzle rules encoded in our model invariants and especially in the operation Thing::valid(Clue).

In Fig. 7, you see an overview on our approach showing the central parts and their connections. Basically, there is a class model, namely our metamodel, including metamodel invariants, and an object model that instantiates the metamodel. This object model is generated by the USE model finder based on a puzzle configuration designed by the puzzle developer. Optionally, domain invariants can added. The object model may be viewed also as a class model in which invariants correspond to the clues generated.

Figure 8 shows the architecture of the approach, showcasing the different elements involved. The metamodel that supports our approach and has been presented in Sect. 2 is made available to the USE tool and becomes the basis around which the rest of the elements are built (label 1). If a modeler wants to use the metamodel to make experiments or play within the USE tool, he or she must write a properties file and additional constraints (label 2). This can be loaded into the USE model finder to generate puzzle instances and can be inspected and manipulated using the regular USE interface. This is the approach used in the previous sections to illustrate the internals of the approach.

To make the puzzles playable through a user interface that hides the complexity of manipulating USE, we have built two components (label 3). A game generator which takes a property specification and OCL constraints and interacts with the USE model finder to generate the corresponding object diagram. Then, a game engine component interprets the object diagram to make it interactive (e.g., check if a selected ‘thing’ violates some clue). On top of this, a user interface (label 4) has been built, which provides a way for the user to write the property specification and the constraints, and then a game zone where the puzzle is shown and can be played.

Bild vergrößern

To specify puzzles, our system requires two main elements. First, the puzzle design has to declare the allowed properties of the puzzle in the form of property names and property values. This is currently done by using property files in the format expected by the USE model finder in order to declare the bounds of the constraint solver. In the example, this will be specified with the following syntax:

Bild vergrößern

In addition, we need to set the bounds for the number of objects of each type in our puzzle model. The computation of these bounds needs to be done currently manually as explained in the previous section.

Bild vergrößern

Using this configuration, the USE model finder will construct an instance of the puzzle which will consist of a valid combination of the property values. To enable the construction of more interesting puzzles, we support the specification of additional OCL invariants which guarantee that the puzzle has the required shape (i.e., loaded invariant in Fig. 4). In general, a puzzle may have several solutions. The USE model finder is able to find them (using its scrolling feature). However, a user might be interested on specifying exactly one, target solution. We can use OCL invariants to specify it. For instance, let us assume that we want to make sure that the solution is a car that is fully red.

Bild vergrößern

A puzzle description is loaded into the USE model finder to generate a concrete puzzle which involves things, clues and a particular solution. This process may take from a few seconds to a few minutes depending on the complexity of puzzle. Therefore, we allow the user to store (and later load) the puzzle so that it can be played repeatedly without the burden of recomputing it.

Our tool generates puzzles using the following YAML format,¹ which is also human readable so that she or he can easily tweak the puzzle (e.g., typically slightly modify the clue description).

Bild vergrößern

To play a game, we have built a user interface (UI) which shows the different elements of the game and allows the user to interactively try to solve the puzzle. Figure 9 shows the user interface for playing the running example puzzle about robbery. The UI shows the list of clues that the user must take into consideration to figure out the solution. At any time in the game, there is an active clue which is the one that the player is using to reason about which solutions must be discarded according to the clue. The possible solutions are shown in the form of cards ( and ). A card has a state which can be Unknown if it has not been banned as a solution ( ), Banned when it has been marked as an invalid solution to the puzzle according to the current clue, or Solution which is given to the card that the player thinks is the solution to the puzzle (i.e., typically because it is the only one not banned).

Bild vergrößern

The behavior of the UI follows the resolution strategy described in Sect. 2.2. We consider three modes or difficulty levels for playing the game.

Bild vergrößern

To implement the system, we have integrated the USE model presented in Sect. 3 into a Java web application. The application invokes the USE model finder programmatically to compute the actual puzzle. To facilitate the integration, we use the options offered by EFinder [5] since it provides a simple API for invoking the USE model finder.

When the puzzle instance is computed, our application processes the generated USE objects and present them in the user interface and make the puzzle playable using the UI shown before.

The prototype is available at https://github.com/jesusc/puzzle-builder.

We propose a puzzle similar to the running example but focused on researchers. The puzzle goal is stated as follows:

Bild vergrößern

To design this puzzle, we have three properties: author, topic and origin (city of birth), and we use as property values the data of Antonio Vallecillo and the authors of this paper. This is specified as follows:

Bild vergrößern

The goal is to have thing elements like Martin, Validation, Dortmund and Jesus, Tooling, Murcia, but also Antonio, Uncertainty, Malaga as the actual solution for the puzzle.

Using this configuration, the solver may select as a solution an unintended combination of property names and values like Author = Antonio, Topic = Martin, Origin = Validation. Moreover, we are interested in forcing a particular solution, in this case the one involving Antonio. To this end, we must specify additional OCL invariants which guarantee that the puzzle has the required shape. In this case, they will be as follows:

Bild vergrößern

The context of the puzzle as shown in Fig. 11 comes from a well-known fantasy novel.

Bild vergrößern

Although one might know the solution (or parts of the solution) by inspecting the offered choices (‘who’: Aragorn, Frodo, Gandalf; ‘what’: IsildursBane, MallornSeed, Palantir; ‘where’: Caradhras, Erebor, Orodruin), the solution, namely the right choice for ‘who,’ ‘where’ and ‘what,’ can be formally derived from the clues in Fig. 11.

In the figure, basically a sequence of USE object diagrams shows (1) the formal representation of puzzle choices with Property objects, possible solutions with Thing objects, and used clues with Clue objects and (2) one derivation of the solution. The upper left quarter shows the application of clue1, the upper right of clue2, the lower left of clue3, and the lower right of clue4. In each of the four quarters, the Thing objects banned by the respective clue are indicated as dark objects, whereas the light Thing objects are not reached by the clue. The respective OCL query and its result are shown as well. In the first quarter for the first clue, the essential results for the last three clues are indicated in short form, as well. Here, dark objects are those banned by clue1, the Thing objects that have on its right border a rectangle with 2 are those newly banned by clue2, Thing objects with a 3 rectangle are newly banned by clue3, and Thing objects with a 4 rectangle are newly banned by clue4. The only light Thing object being not marked is the only object with banned=false, and this object represents the puzzle solution.

The puzzle configuration defines in the properties file the items for the name and value of Property objects as well as appropriate sizes for the number of objects and links for the classes and the association. The configuration includes one invariant that determines the solution:

Bild vergrößern

In the book [10], a large collection of puzzles is modeled in first-order logic. In order to show that our approach for puzzle modeling is capable of expressing puzzles like the ones in [10] and to further validate our approach, we have chosen three typical puzzle examples and explain how they can be formulated in our approach. The examples come from three different book chapters (Micro-arithmetic Puzzles, Love and Marriage, Grid Puzzles). These examples illustrate how analogous puzzles could be effectively modeled using our methodology.

The first puzzle from the book is displayed basically in the form of an object diagram in Fig. 12. It uses four integer variables and requires to find substitutions for them such that particular relationships between the variables values are satisfied. All substituted values have to be distinct, have to come from the interval 1..4, and the two equations shown in the lower right of Fig. 12 have to hold. In order to handle this puzzle, we had to slightly extend our class model to be able to express numerical conditions, since values are expressed in the original model as strings: we extended the class model with the operation toInt that converts a string to an integer, provided the string represents an integer. The four variables are expressed as four properties, the integer interval as attribute restrictions in the properties file, and the distinctness requirement and the two equations are stated as invariants. As can be seen from the found solution, the book puzzle parts could be successfully stated, and the proper solution was found.

In this model and in the following two, there is only one Thing object, i.e., only one possible solution, that must be found. Formally, there are no Clue objects, since the clues are given in the puzzle formulation and are not expected to be constructed. The already formulated puzzle clues are expressed as invariants that the Thing object, which is to be constructed and that possesses attribute values and links, has to satisfy. We emphasize that the puzzle formulations that we have developed for the book puzzles are instantiations of our puzzle metamodel, whereas in the book each puzzle is newly formulated with an ad-hoc model, not as a metamodel instantiation as done in our approach.

The second puzzle from the book is displayed basically in the form of an object diagram in Fig. 13. It shows a 3x3 matrix of Integer variables, requires the value 5 to occur in the center, and each of the rows, columns and diagonals to have the sum 15. As before, the variables from the matrix are expressed as properties, integer ranges as attribute restrictions in the properties file, and the eight equations for rows, columns and diagonals are stated as invariants, where in Fig. 13 from the eight equations only one equation is shown in an exemplary way. From the found solution, one learns that the book puzzle parts could be properly expressed, and again the right solution was achieved.

The third puzzle from the book is pictured basically in the form of an object diagram in Fig. 14. It is about guessing the name of a particular person at a dinner meeting where hints are given regarding the order that persons sit at a round table. Opposed to the previous two models with focus on numbers, properties express characteristics of persons, namely the gender of the person and the person sitting left to the respective person. In the properties file, the person names and values for gender as well as the number of Property objects and links are stated. In order to capture the cyclic nature of the underlying information, i.e., every person has a left neighbor, some Property objects show the same domain (namely, the names of the persons) for the name and value attributes. Invariants formulate the puzzle conditions as (1) proper specification for the gender characteristic, (2) the requirement that women and men alternate, and (3) particular neighbor requirements for two persons (namely Anna and Roger). The puzzle answer is here formulated as an OCL query which yields a particular result. From the found formulation, we see that the puzzle parts from the book could be expressed, and also the solution from the book was reached.

In Fig. 15, we show how the cyclic information structure for the example could be represented in a USE model as an extension of our puzzle metamodel. As the persons are expressed with Property objects, one could introduce a derived, reflexive association on the class Property for the person sitting left to another person. The object model displays the achieved solution using this additional association.

In this section, we show that our approach can also be used to model puzzles available in the web and consumed by actual users. In particular, we focus on the type of puzzles of https://www.zebrapuzzles.com (puzzles in the style of the Einstein Riddle ²).

Bild vergrößern

By using an example, Fig. 16 gives an impression how puzzles of the zebrapuzzles website look like and how they would be modeled in our approach. Four parts are shown: The website puzzle structure in the form of a table to be filled by the user, the representation of the solution table as a UML object diagram in our model, the verbal clues given to the user and the representation of the clues in the form of a complex OCL invariant with each of the 13 clues formalized as a conjunctional part in an existentially (one) quantified OCL formula.

The puzzle involves four different men characterized by four properties: a shirt with a unique color, a unique first name and a food order for a unique soup and a unique meat dish. The men are arranged from left to right, and, accordingly, one can think of the properties being arranged in line, e.g., there is the soup in the third position. The property values are available through drop-down menus. The table already shows the puzzle solution except the second soup. However, this soup is already determined as the other three soups have already been selected. This second soup is represented in the object diagram in the second part of the figure through the property object property37 with name value Soup2. The object diagram layout follows the table.

The UML object diagram shows how the puzzle solution is represented as a Thing object with links to sixteen property objects. Thus, for example, there are four Shirt Property objects, namely for Shirt1, Shirt2, Shirt3 and Shirt4 holding appropriate values. In our model, there are 64 Property objects, as there are 16 properties (Shirt 1..4, Name 1..4, Soup 1..4, Meat 1..4) each capable of holding 4 values: \(16*4=64\). In our first puzzle example for a car with three different top and body colors, we have explicitly shown all possible nine solutions in Fig. 1. In this example, we would roughly obtain \(4!*4!*4!*4! = 331.776\) different solutions, a number unmanageable to display and to construct in our approach.

The third part of Fig. 16 displays the verbal clues presented to the user. The clues directly constrain (1) single fields in the table (e.g., using formulations as ‘in the last position’), (2) lines by particular restrictions (e.g., ‘at one of the ends’), (3) the table by requiring particular patterns to occur (e.g., ‘immediately after’) or (4) neighbor or successor properties and values (e.g., ‘somewhere after’). These verbal formulations are made precise by stating them in OCL.

The fourth part shows the clues as parts of a complex OCL invariant. The clues partly directly refer to single properties, e.g., ‘The man who ordered beef is in the last position’ roughly corresponds to ‘Meat4=beef.’ The clues partly refer to property combinations, e.g., ‘The person who ordered corn soup is immediately after Charles’ roughly corresponds to ‘(Name1 = Charles and Soup2 = CornS) or (Name2 = Charles and Soup3 = CornS) or (Name3 = Charles and Soup4 = CornS).’ We have marked three of the 13 clues in the verbal part and correspondingly marked them in the formal representation as an OCL invariant for easy identification. The OCL formulation nicely points out that there are six used clue patterns. Note that some of the clues cannot be expressed in our clue metamodel as there we only consider simple implications, but not general first-order formulas (e.g., a series of disjunctions of conjunctions as in the above ‘Charles’ and ‘CornS’ example).

In conclusion, we can say that we are able to model puzzles like the ones from zebrapuzzles and express the clues as constraints. Proceeding this way, we can check whether among a number of existing Thing objects a solution exists, but we currently cannot generate clues like the ones occuring in the example as this would require an extension of our current (clue) metamodel. We emphasize, however, that the basic logic behind zebrapuzzles can be formulated in our approach, but some approach limits become apparent. However on zebrapuzzles, manually constructed puzzles and solutions are presented whereas we automatically can construct puzzles, solutions and clues all restricted with constraints (e.g., single solution or multiple solution).

In order to obtain feedback on our puzzle approach, we performed a survey among students participating in a UML and OCL course. The survey was performed after the end of the course and before the oral examinations. The survey with nine questions presented two puzzles and was asking about (1) the solutions and derivations of solutions [4 questions for puzzle A and 2 questions for puzzle B], (2) the applied logical laws in the solution finding process [1 question] and (3) the difficulty and the usefulness of logical puzzles [2 questions].

Both puzzles were about a scenario where a murder crime had to be solved. The murderer was either the Butler, the Duke or the Countess. The murder happened either in the Library, the Parlour or the Garden. The murder either used a Rope, a Gun or a Knife. Two different sets of clues both possessing a unique solution and presented in the form of object diagrams with Clue objects from our metamodel were given. Both puzzles are displayed in Fig. 17 with the derived attribute /toStr showing the clue in compact form. In the figure, the first puzzle also presents on the right side three derivations for a potential solution that is shown in the bottom line. Two of the three derivations are erroneous and make unacceptable conclusions. The second derivation is the correct one. Results and intermediate steps of the derivations are pictured in comment notes on the right side.

Bild vergrößern

Bild vergrößern

Bild vergrößern

All questions were presented along with multiple-choice questions and answers. The questions asked were: For questions 2–4, the multiple-choice answers included an option ‘no incorrect step.’ For question 7, a choice between three important logical laws was offered. Although the survey is based on multiple-choice questions, we believe that the questions are formulated on a high technical level, and it seems unlikely that by chance only correct answers are picked.

Bild vergrößern

Bild vergrößern

The student responses are shown in overview form in Figs. 18, 19 and 20. For the first seven questions, there is one correct answer, the other answers are wrong. Basically, and as expected, there is a relative majority in the student answers for the right answers. However, there is one exception: in question (7) about which logical law has to be applied in the puzzle solution process there is a majority for the De Morgan law, not for the law stating implication equivalence. Of course, this question is not directly about a concrete puzzle, but it is about abstract principles standing behind formal reasoning. As we know, a large number of students in media informatics being not trained in formal matters attended the course, we suspect that this is the reason for this fact. Otherwise the student answers are basically as expected and do not present serious surprises. The two ranking questions reveal that the students found the puzzles relatively hard to solve. And there is a majority in regarding such logical puzzles as important or at least as useful for Computer Science education. In the respective course, which covers a wide range of topics from basic UML to operation details of OCL, we did not put a high emphasis on using puzzles. Probably a better approval of puzzles would result, if teaching with puzzles would be better emphasized.

Survey summary: Fifteen students participated in the survey. For the single questions and stated percentages, one can derive the concrete numbers. The educational context for the survey was that the survey took place on a voluntary basis for the students after the lectures and before the oral examination. Twenty-five students were enrolled in the course, which means that ten enrolled students did not participate in the survey. The participating ones probably expected further hints for the oral examination that was already scheduled.

The examples from this section on validation show that the approach is capable of formulating a large spectrum of puzzle situations, from numerical problems to discrete graph-like structures with cyclic information reference. In particular, nontrivial puzzles that come from the literature or from the web could be realized or at least be modeled with the approach.

The student survey indicates that students with background on UML/OCL are, in general, able to interpret our puzzle models. Moreover, the survey indicates that teaching with puzzles is accepted well by students.

The use of puzzles is a well-known approach to the teaching of problem-solving skills and athematical thinking [7, 17]. The nature and difficulty of the puzzles vary depending on the target players: from school grade students to engineering students.

For instance, Parsons puzzles are targeted to computer science students since the task is to reorder a set of statements to form a target programming assignment. For this kind of puzzles, both solvers [14] and builder [6] tools have been proposed.

Puzzles can also be used to introduce complex topics to students. For instance, quantum gates are introduced to middle-school and high-school students through a dedicated puzzle game [16].

Puzzles have been used to teach first-order logic. For instance, the ‘Introduction to logic’ course at Stanford uses a variant of the MineField game .³ In [11], a variant of this approach in which the system also generates new instances of the game automatically is put forward.

In our case, our goal is to automatically build logic-based puzzles which could be played by students (e.g., high-school students). These puzzles can also be targeted to children if the complexity of the solution and clues is small and the appropriate gaming experience (e.g., physical cards) is provided.

The topic of solving puzzles has traditionally been addressed by using solvers of different types (e.g., SAT or SMT solvers). In this case, given a puzzle the complexity lies on properly encoding the puzzle using the underlying formalism. For instance, in [10] several puzzles along with their encoding in a logic formalism are discussed. In this work, we use some of these puzzles to show the applicability of our approach.

The topic of solving puzzles has recently gained interest due to the new AI models, since puzzles along with solutions can be used to test the reasoning capabilities of large language models (LLMs). Also, LLMs can be used as an interface to interact with the puzzle [12]. In our case, our system could be used as a test generator (by generating different puzzle instances) to analyze the capabilities of LLMs for solving logic puzzles.

The design and development of new puzzles is a concern complementary to solving them. In this respect, some DSLs have been proposed to specify puzzles and their gaming context. For instance, EGGG [19] is DSL which allows the user to encode games, and it generates an interface to play with them (e.g., the rock–paper–scissors). However, the system is primarily a code generator, and it does not really ‘understand’ the games.

In [3], a DSL is proposed to encode human strategies for solving logical puzzles like Sudoku or Nonograms. The goal in this case is to understand how players address complex games. This is done through program synthesis techniques. In our case, our generation of Clue objects can also be seen as program synthesis procedure.

Ortiz et al. [18] proposed a system to generate Nonograms puzzles based on color images.

To the best of our knowledge, our approach is the first approach based on software modeling foundations to build logical puzzles, which incorporates the automatic generation of puzzle instances via constraint solving.

Although logical puzzles have a tradition dating back many centuries [20] and many well-known logical puzzles have been created (e.g., the zebra puzzle also known as Einstein’s Riddle), there is still an active industry which produces new puzzles and publishes them in magazines, books and dedicated websites.

As a concrete example, the website https://www.brainzilla.com/ offers a large number of puzzles of different kinds. Several of them can be classified within the category of logical puzzles since they are built on top of clues and logical relationships. It has the so-called ‘zebra puzzles’ (the type of puzzles shown in Sect. 5.4), logic grid puzzles, Suduku-like puzzles and logical equations.

Our approach is particularly relevant for logic grid puzzles which we can model and generate automatically with our tool. According to personal communication with the owner of the website, the logic grid puzzles are constructed manually by skilled game player. This means that our approach could be an alternative to build this type of puzzles. On the other hand, we have shown that our approach is expressive enough to model Zebra Puzzles and the question of how to tune an OCL solver to automatically construct a concrete instance could be become a relevant benchmark to move this type of tools forward.