ONT Re: Zeroth Order Theories (ZOT's)
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
I think that it might be a good idea to go back to a simpler example
of a constraint satisfaction problem, and to discuss the elements of
its expression as a ZOT in a less cluttered setting before advancing
onward once again to problems on the order of the Four Houses Puzzle.
| Applications of a Propositional Calculator:
| Constraint Satisfaction Problems.
| Jon Awbrey, April 24, 1995.
Graph Coloring
Based on the discussion in [Wil, page 196].
One is given three colors, say, orange, silver, indigo,
and a graph on four nodes that has the following shape:
| 1
| o
| / \
| / \
| 4 o-----o 2
| \ /
| \ /
| o
| 3
The problem is to color the nodes of the graph
in such a way that no pair of nodes that are
adjacent in the graph, that is, linked by
an edge, get the same color.
The objective situation that is to be achieved can be represented
in a so-called "declarative" fashion, in effect, by employing the
cactus language as a very simple sort of declarative programming
language, and depicting the prospective solution to the problem
as a ZOT.
To do this, begin by declaring the following set of
twelve boolean variables or "zeroth order features":
{1_orange, 1_silver, 1_indigo,
2_orange, 2_silver, 2_indigo,
3_orange, 3_silver, 3_indigo,
4_orange, 4_silver, 4_indigo}
The interpretation to keep in mind will be such that
the feature name of the form "<node i>_<color j>"
says that the node i is assigned the color j.
Logical Input File: Color.Log
o----------------------------------------------------------------------o
| |
| (( 1_orange ),( 1_silver ),( 1_indigo )) |
| (( 2_orange ),( 2_silver ),( 2_indigo )) |
| (( 3_orange ),( 3_silver ),( 3_indigo )) |
| (( 4_orange ),( 4_silver ),( 4_indigo )) |
| |
| ( 1_orange 2_orange )( 1_silver 2_silver )( 1_indigo 2_indigo ) |
| ( 1_orange 4_orange )( 1_silver 4_silver )( 1_indigo 4_indigo ) |
| ( 2_orange 3_orange )( 2_silver 3_silver )( 2_indigo 3_indigo ) |
| ( 2_orange 4_orange )( 2_silver 4_silver )( 2_indigo 4_indigo ) |
| ( 3_orange 4_orange )( 3_silver 4_silver )( 3_indigo 4_indigo ) |
| |
o----------------------------------------------------------------------o
The first stanza of verses declares that
every node is assigned exactly one color.
The second stanza of verses declares that
no adjacent nodes get the very same color.
Each satisfying interpretation of this ZOT
that is also a program corresponds to what
graffitists call a "coloring" of the graph.
Theme One's Model interpreter, when we set
it to work on this ZOT, will array before
our eyes all of the colorings of the graph.
Sense Outline: Color.Sen
o-----------------------------o
| 1_orange |
| 2_silver |
| 3_orange |
| 4_indigo |
| 2_indigo |
| 3_orange |
| 4_silver |
| 1_silver |
| 2_orange |
| 3_silver |
| 4_indigo |
| 2_indigo |
| 3_silver |
| 4_orange |
| 1_indigo |
| 2_orange |
| 3_indigo |
| 4_silver |
| 2_silver |
| 3_indigo |
| 4_orange |
o-----------------------------o
| Reference [Wil]
|
| Wilf, Herbert S.,
|'Algorithms and Complexity,
| Prentice-Hall, Englewood Cliffs, NJ, 1986.
|
| Nota Bene. There is a wrong Figure in some
| printings of the book, that does not match
| the description of the Example that is
| given in the text.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤