Re: [xml-dev] The Einstein Puzzle

[Rick Jelliffe <rjelliffe@allette.com.au>]

Nice to see this!

One angle I would say is that the SAT terminology "constraint" is somewhat different from the schema terminology of "constraint".  Schemas don't say that the Englishman lives in the red house, they say that all Englishmen we are interested in live in red houses.  

For example, take this asertion:

 <sch:rule context="house[owner='Australian']">

    <sch:assert test="pet='quoll'">Every Australian has a quoll for a pet</sch:assert>

  </sch:rule>

We might say this is semantically equivalent to

 <unchangeableLawOfTheUniverse  nationality="Australian" pet="quoll"/>

but not

 <lastPersonISaw nationality="Australian" pet="quoll"/>

So Schematron lets us use attribute values and element data content in assertions, but only to express the invariant qualities of all possible documents.  When you start to have assertions on data, you from schema languages to unit test languages.

So I would say that when "it is not obvious what instances satisfy the constraints" it is a sign that you are not working in the schema domain, but in the data domain.   For Schematron, you notionally *start* with a natural language description of the constraint. If you cannot formulate a natural language description, you are hamstrung from the start: you are hacking (in the bad sense).  So model-checking (for Schematron) should be an exercise in debugging not search  (though coverage-checking may not fit this sweeping statement).  In Schematron, the assertion is the natural language statement, not just the assertion test (in XPath or whatever): the entire design of Schematron is to encourage explicit statements of intent, not just to have formula in isolation.

Regards

Rick

On Tue, Jan 16, 2018 at 12:59 AM, Costello, Roger L. <costello@mitre.org> wrote:

Hi Folks,

 

Scenario: You create an XML Schema that specifies the structure of XML instances. You create a Schematron schema that specifies constraints.

 

Sometimes constraints are complex. In such cases it may not be immediately obvious what instances satisfy the constraints. The Einstein puzzle is a neat example of this.

 

Below I show the Einstein puzzle. Then I show how to automatically generate—from the constraints—the set of instances.

 

The Einstein Puzzle

There are five houses of different colors next to each other on the same road. In each house lives a man of a different nationality. Every man has his favorite drink, his favorite brand of cigarettes, and keeps pets of a particular kind.

1. The Englishman lives in the red house.
2. The Swede keeps dogs.
3. The Dane drinks tea.
4. The green house is just to the left of the white one.
5. The owner of the green house drinks coffee.
6. The Pall Mall smoker keeps birds.
7. The owner of the yellow house smokes Dunhills.
8. The man in the center house drinks milk.
9. The Norwegian lives in the first house.
10. The Blend smoker has a neighbor who keeps cats.
11. The man who smokes Blue Masters drinks beer.
12. The man who keeps horses lives next to the Dunhill smoker.
13. The German smokes Prince.
14. The Norwegian lives next to the blue house.
15. The Blend smoker has a neighbor who drinks water.

Create an XML Schema. Create a Schematron schema. What are the valid instances? In other words, what is the color of house1? What is the nationality of the person living in house1? What is his favorite drink? What brand of cigarette does he smoke? What is his pet? Ditto for the other houses.

Perhaps you created an XML Schema that specifies XML instances be structured like this:

<Neighborhood>
    <House number="1">
        <color>...</color>
        <nationality>...</nationality>
        <drink>...</drink>
        <cigarette>...</cigarette>
        <pet>...</pet>
    </House>
    ...
</Neighborhood>

Your Schematron schema specifies the 15 constraints listed above.

Good.

Now, what is a valid instance?

………. I’m waiting ………. still waiting ………. give up?

The constraints in the Einstein puzzle are pretty complex. It’s not immediately obvious the instances that satisfy the constraints. And there’s no tool support to help you find the instances.

That’s a problem.

Here’s the state of technology as I see it: We have languages and tools (e.g., XML Schema/Saxon, Schematron/XSLT Processor) for expressing structure and constraints. But we do not have languages and tools which auto-generate the instances that satisfy the structure and constraints:

The Einstein puzzle is an example of a constraint satisfaction problem – given a bunch of constraints, what are the instances that satisfy the constraints. There are tools called SAT (satisfiability) tools which can evaluate a bunch of constraints and tell you the instances that satisfy the constraints. In the last 20 years there has been a revolution in SAT technology. Today, SAT tools, such as SAT4j (SAT for Java), can solve enormous constraint expressions. 20 years ago it would have taken a supercomputer days to solve expressions that can today be solved in a few seconds, using an ordinary laptop.

Here's what Donald Knuth says:

Enormous technical breakthroughs in recent years have led to amazingly good ways to approach the satisfiability problem. We now have algorithms that are much more efficient than anyone had dared believe possible before the year 2000. These so-called “SAT solvers” are able to handle industrial-strength problems, involving millions of variables. [Donald Knuth, Satisfiability and the Art of Computer Programming]

Professor Daniel Jackson and his team at MIT have created a language and tool (the tool wraps SAT4J) called Alloy. Alloy can show you all the instances satisfying a set of constraints.

Want to see the solution to the Einstein Puzzle? Want to extend your XML skills to express more complex constraints and have a tool automatically generate the instances satisfying the constraints? See here: http://xfront.com/Alloy/Einstein-Puzzle.docx

/Roger