PROLOG-REQUEST@SUSHI.STANFORD.EDU (Chuck Restivo, The Moderator) (05/14/87)
PROLOG Digest Thursday, 14 May 1987 Volume 5 : Issue 37
Today's Topics:
Puzzles - Meta & Xmas
----------------------------------------------------------------------
Date: Mon 11 May 87 13:39:29-CDT
From: Dave Plummer <Atp.Plummer@R20.UTEXAS.EDU>
Subject: A meta puzzle
> Q? If solve(GoalA,GoalB) is true then can one make any comment about
> the relation between the proof-tree, search tree for the two goals.
> with (or without :-)) respect to solve(GoalA) and solve(GoalB).
The only answer I can think of is that the shape of the proof trees
for GoalA and GoalB must be the same. NOTE: it is obviously not true
that the search trees are the same shape. Not a very helpful answer,
I'm afraid, as the programs have to be run for each goal before we can
determine whether the solve/2 case will succeed.
> One statement that I could make is
> solve(GoalA,GoalB) implies (solve(GoalA), solve(GoalB))
Actually this is only true in the simplified world of pure Prolog.
For example, the last thing GoalA might do is retract the first clause
of the proof of GoalB. In the /2 case, this clause would already have
been used, and the retract would not cause problems.
-- Dave
------------------------------
Date: 11 May 87 0:39 +0800
From: Paul Voda <voda%ubc.csnet@RELAY.CS.NET>
Subject: Xmas Puzzle.
This contribution deals with a solution to the Xmas Shoppers puzzle as
presented and solved by Goeran Baage in the issue 29 of Prolog Digest.
The puzzle is a quite complicated one with the raw solution space of
12!**3 * 15**12, i.e. of about 10**42, candidate solutions. Baage's
solution is not a true generate and test approach since he
periodically inserts a constraint checking predicate into the
generation part. Since Prolog is not constraint based, the Baage's
constraint checker has to rely on the extra-logical (meta-logical)
construct "var". I think that the explicit use of var from within a
program
a) jeopardizes the declarative reading
b) makes the statement of the problem more procedural than it should be.
In the last year I was experimenting in the Turbo Prolog with the true
generate and test of much smaller logic problems. These typically call for
the corelation of three sets of five entities (first names, last names,
occupations, etc). Such puzzles have the solution space of 5!**3, cca
1.7M, and run for about 60 minutes.
The large puzzles (more than 10**12 candidates) cannot be probably solved
by a true generate and test unless one severely reorders the clues and
encodes the hand-solution process procedurally. But for that one does not
need Prolog, a Pascal suffices. Passive delaying of constraints of
Mu-Prolog does not help either. The puzzles I have tried routinely overwhelmed
the implementation I have.
It would seem that the active treatment of constraints is required. I enclose
the solution of the Xmas shoppers puzzle in the programming language R-Maple
I was designing and helping to implement for the last two years.
An implementation for PC and compatibles is almost finished now.
R-Maple is a logic programming language with the active treatment of
constraints. It can do smaller puzzles (up to 10**12) without any rearrangment
of clues by a verbatim transcription of the clues into the program. A small
puzzle (1.7M) executes in under one second on an 8Mhz PX-XT and it usually
does not require more the 5 backtracks. Many of them solve without any
backtracks at all.
The truly big puzzles as Xmas shoppers require some planning because
they contain too many unknowns (12*9 = 108 for the Xmas shoppers)
where the constraints form a system of equations and inequalities too
large to be solved directly in a reasonable time. One wants basically
to employ a divide and conquer approach by splitting the problem into
two or more relatively independent subproblems. Thus the unknowns in
one subproblem are not constrainted by the unknowns from the other
subproblems. The approach Baage took in his Prolog solution works very
well in R-Maple. My solution splits the problem into two relatively
unconnected subproblems of:
a) finding as much as possible about the order and the distribution of
the purchases, without caring who bought what, and of
b) corelating the husbands, wives, and surnames to the order of purchases
by using the filled purchase matrix from a).
The R-Maple system found the solution in 17 secs, and ascertained that
there are no additional solutions in the total time of 69 seconds
(8MHz PC-XT) using 110 backtracks altogether. It is interesting to
note that the system generated the 16 possible purchase matrices
(based on my splitting of the problem) in 30 secs using up all the
backtracks. The corelation of names to the purchases did not require
any additional backtracks but it required about 2.5 seconds to check
each candidate matrix (and discard 15 of them). I have to note here
that R-Maple solves the linear diophantine equations in the 32 bit
integers using software routines to perform the arithmetic (and an 8
bit bus to fetch the integers). The solution of linear diophantine
systems is based on the employment of the GCD algorithm and
multiplication over and over. I estimate that the 32 bit arithmetic
and bus width would speed up the 30 seconds spent on finding the
matrices by a factor of 100 at least. Incidentally, the clue that
each couple bought a different combination of items is superfluous but
it speeds up the execution since additional 28 candidate purchase
matrices can be eliminated.
A few words about R-Maple:
It is a programming language integrating three language generations:
3GL Pascal-like language, 4GL database language and a 5GL logic
programming language. Yes, R-Maple has the types of essentially Pascal
but, in contrast to the Turbo Prolog, the domain of R-Maple values is
actually the S-expressions of Lisp. All R-Maple types are just subsets
of the universal type U of S-expressions. Since there is nothing else
but S-expressions, it is possible to convert a value "a" of type "A"
into the value "b" of arbitrary type "B" by the cast "a:B = b". This
succeeds only if the S-expression denoted by "a" is of type B (i.e.
the types overlap). Logically speaking iff "A(a) & B(b) & a = b"
holds. The R-Maple identity is actually the extensional identity of
S-expressions. The conversions from and into the universal type U are
automatically inserted by the compiler (R-Maple generates the native
8086 code) so the people swearing by the typeless Prolog and Lisp can
program their predicates in the typeless style using the type U.
Thusy, of course, they forfeit the compiler introduced optimizations
possible because of the knowledge of types and modes.
The types (T) and modes (m) of arguments and local variables (x) are
specified by declarations of the form "x :m T" where "m" is a mode
specifier. x:<T means that the value of x will be fully known when
the predicate is called (INPUT mode), x:>T means that the value will
be fully generated before the predicate exits (OUTPUT mode), x::T
means that the value x is a symbolic (logic) variable which can have a
value, or a set of constraints, or even no constraints (SYMBOLIC
mode). There is also an input/output mode "x:.T" with reassignable
Pascal-like variables.
Here I hasten to add that R-Maple does not contain a single
extra-logical feature and all of its constructs (including
reassignable variables, and updating of data base files) have precise
semantics given by the first order Theory of Pairs (S-expressions).
A very brief explanation of constructs used in the solution:
Variables start with small letters, constants -being proper names- are
capitalized. People used to the exactly opposite philosophy Prolog
beware! Comments are enclosed in braces {}. The type I is a short
(16 bit), L is a long (32 bit) integer. The type A defined as "A = B |
C | E" is an enumerated type with the values B, C and E.
For the long integer symbolic variables R-Maple simplifies and solves
arbitrary boolean combinations of arbitrarily existentially quantified
systems of linear constraints. In other words, R-Maple has a built-in
decision procedure for Presburger arithmetic (systems of linear
diophantine equations and inequalities). For instance the query
s::L & b::L & 8*s + 6*b = 46 & s > 0 & b > 0
is solved without any backtracks to give the two solutions
s = 2, b = 5 and s = 5, b = 1.
This is the solution of the problem of finding the number of spiders
and beetles in a box containing 46 legs.
The type A -> B where A is a subrange type is the type of finite
mappings from A to B, i.e. the type "array A of B". In the domain of
S-expressions, arrays are just lists. An array "a" is indexed as a(i)
and R-Maple accepts arbitrary constraints involving array indices.
For instance "a(i+1) < 2*a(i)" constraints a possibly unknown element
"i" of the (possibly unknown) array "a" to be less than a half of the
preceding element. The array a:: A->>B is an injection, i.e. a mapping
without the duplication of values. Thus a(x) = a(y) implies x = y.
The type "r :: rel T" is the type of all finite relations over T, i.e.
the type of all finite subsets of T (in the domain of S-expressions,
the values of relations are just lists of T). Relations can be
asserted positively "a in t" or negatively "~ a in t". Thus the
relation "in" is just a list membership relation. Relations are
extensionally lists but, since the order cannot be accessed by the
program, R-Maple can handle them efficiently. Incidentally, lists can
be defined as, say, "t:>list T".
Atomic formulas are joined by the connectives of conjunction (&) and
disjunction (|). A predicate definition such as
pred P(x::T) iff y::V & ..x..y..
is from logical point of view a predicate satisfying the equivalence
P(x) <-> T(x) & exists y ( V(y) & ..x..y.. )
Procedures (proc) are just predicates without backtracking
(deterministic predicates) so the compiler can optimize them.
Procedures with all args but the last INPUT can be invoked both in
relational and functional notations.
proc Fact(x:<L,y:>L) iff
if
x <= 1 -> y = 1
true -> y = x*Fact(x-1) {this is the same as Fact(x-1,z) & y = x*z }
end
As one can see from this and from the predicates below, R-Maple allows
function symbols (like +,*,..) in the terms.
Here is the outline of the solution of Xmas shoppers as given by the
description of the actions taken by the execution of the predicate Xmas.
The query "Xmas(husbands,wives,surnames,purchases)" solves the puzzle:
a) The constraints connecting names to the items purchased are
set in the predicate Purchases. This does not set any choice points.
All the arguments are symbolic (logical, unknowns).
b) The matrix of purchases 'p' is established as a symbolic two-dimensional
array of zeros and ones giving the quantities purchased. The constraints
on purchases are set as equations constraining row sums to exactly 4 items
(Sumpurch) and column sums to 8 items (Sumitems). In the process of this
the waiting on order of Marshall and Martha is determined. This
last requires 8*12 = 96 backtracks (out of the total 110).
c) The matrix of purchases is checked for the uniqueness of purchase
combinations by the cast: "p:Seq->>Purchase = purch". Note that "p"
is just an ordinary array of type Seq -> Purchase. Defining it as as an
injection would flood the system with the additional 12 over 2 = 66
"not equals" and would seriously slow down the solution process.
The reader will note that the argument "purch" is of the OUTPUT mode.
Thus the symbolic-to-output conversion (i.e. the solving of equations)
happens during the cast processing. This gives a total of 16 candidate
matrices "purch".
d) The conversion of the fully known candidate purchase matrix "purch"
into the symbolic array of relations "prel" whis is needed in the predicate
Purchases is done by the predicate Convert. The use of both the purchase
matrix and of the array of relations is necessary because there is no
way in R-Maple to enquire about the cardinalities of relations.
e) After the finalization of the purchase relations "prel" by Convert,
the system is in the position to solve the delayed system of name
constraints set by the predicate Purchases. It rejects all
but one arrays of relations "prel". This happens without any additional
backtracks.
-- Paul J. Voda.
--------------Xmas Shoppers as solved in R-Maple -------------------------
{ The Christmas Shopping Puzzle, text in Prolog Digest 29 vol. 5 or
as a one-to-one permutation named Grocery Shopping in the first book of
Dell Logic Puzzles. }
Item = Gloves | Book | Perfume | Pearls | Sweater | Handbag
Surname = Stanton | Craig | Collins | Smith | Swain | Anthony | Douglas |
Jones | O_Connor | Marshall | Day | Murphy
Female = Elizabeth | Geraldine | Evelyn | Martha | Eleanor | Cheryl |
Susan | Dorothy | Sandra | Cathleen | Rosalyn | Margaret
Male = Bob | Gary | Tom | Jack | Allen | John | Adam | Steve |
George | Joe | Bill | Chuck
Seq = [0..11] {this type encodes the order of waiting on, counting from 0}
No :<L = 0 {No is defined as a long integer constant equal to zero}
Yes :<L = 1
Purchase = Item -> L[No..Yes] {array indexed by enum Item to Long int.}
pred Xmas(h::Male->>Seq, w::Female->>Seq, s::Surname->>Seq,
purch:>Seq->>Purchase) iff
Purchases(h,w,s,prel,martha,marshall) & {just set the name constraints}
Order(p,martha,marshall) & p:Seq->>Purchase = purch &
Convert(0,purch,prel)
pred Purchases(h::Male->>Seq, w::Female->>Seq, s::Surname->>Seq,
p::Item->rel Seq, martha::I, marshall::I) iff
{1} s(Craig) in p(Handbag) & s(Craig) < s(Murphy) & s(Murphy) <> 11 &
{2} s(Collins) in p(Gloves) & s(Collins) in p(Handbag) &
s(Collins) in p(Sweater) & s(Collins) in p(Perfume) &
{4} x::I & s(Smith) = x - 2 & h(Gary) = x - 1 &
x in p(Book) & x in p(Handbag) & s(Swain) = x + 1 & h(Bill) = x + 2 &
{5} ~w(Geraldine) in p(Handbag) & ~w(Geraldine) in p(Sweater) &
{7} h(Tom) in p(Book) &
{8} s(Marshall) = marshall &
{9} w(Evelyn) in p(Gloves) & ~w(Evelyn) in p(Perfume) &
{10} w(Martha) = martha & h(Jack) = martha + 1 & w(Margaret) = martha + 4 &
{12} ~h(Chuck) in p(Gloves) &
{14} ~w(Eleanor) in p(Perfume) &
{15} ~h(Allen) in p(Handbag) & ~h(Allen) in p(Gloves) &
h(Allen) <> s(Anthony) & ~s(Anthony) in p(Gloves) &
{16} w(Cheryl) <> 9 & w(Cheryl) <> 11 & h(John) <> w(Cheryl) &
w(Cheryl) in p(Sweater) & w(Cheryl) in p(Handbag) &
h(John) in p(Sweater) & h(John) in p(Handbag) &
{17} s(Douglas) = 8 &
{18} ~h(Adam) in p(Handbag) & h(Adam) + 1 = s(Day) &
{19} h(Steve) in p(Pearls) & h(Steve) in p(Book) & h(Steve) in p(Sweater) &
{21} ~s(Jones) in p(Sweater) &
{22} w(Susan) in p(Pearls) &
{23} h(George) in p(Sweater) &
{24} ~w(Dorothy) in p(Gloves) & ~s(Craig) in p(Gloves) &
~h(Joe) in p(Gloves) & ~w(Rosalyn) in p(Gloves) &
~w(Rosalyn) in p(Sweater) & w(Dorothy) <> s(Craig) &
w(Dorothy) <> h(Joe) & s(Craig) <> h(Joe) & s(Craig) <> w(Rosalyn) &
h(Joe) <> w(Rosalyn) &
{25} s(O_Connor) in p(Perfume) & s(O_Connor) in p(Sweater) &
{26} ~w(Sandra) in p(Sweater) & w(Sandra) + 1 = w(Cathleen)
pred Order(p::Seq->Purchase, martha:>Seq,marshall:>Seq) iff
{3} p(7,Book) = Yes & p(9,Book) = Yes &
{6} p(11,Pearls) = No &
{11} p(0,Perfume) = Yes & p(1,Perfume) = Yes & p(2,Perfume) = Yes &
p(3,Perfume) = Yes & p(4,Perfume) = Yes &
{13} p(0,Sweater) = No & p(1,Sweater) = No & p(3,Sweater) = No &
{17} p(8,Gloves) = No & p(8,Sweater) = No &
{20} p(9,Gloves) = No & p(10,Gloves) = No & p(11,Gloves) = No &
{10} m:<[0..7] & m = martha & {waiting order of Martha}
p(m+2,Gloves) = Yes & p(m+2,Perfume) = Yes &
p(m+2,Book) = Yes & p(m+2,Handbag) = Yes &
p(m+3,Pearls) = No & p(m+3,Book) = No &
{8} p(marshall,Pearls) = No & p(marshall,Perfume) = No & {order of Marshall}
Sumpurch(0,p) & Sumitems(p,Gloves) {row and column sums are set}
pred Sumpurch(o:<I, p::Seq->Purchase) iff {every couple bought 4 items}
if
o <= 11 ->
p(o,Gloves)+p(o,Book)+p(o,Perfume)+p(o,Pearls)+
p(o,Sweater)+p(o,Handbag) = 4 &
Sumpurch(o + 1,p)
end
pred Sumitems(p::Seq->Purchase, t:<Item) iff {every item was bought 8 times}
p(0,t) + p(1,t) + p(2,t) + p(3,t) + p(4,t) + p(5,t) +
p(6,t) + p(7,t) + p(8,t) + p(9,t) + p(10,t) + p(11,t) = 8 &
if
t < Handbag -> Sumitems(p,t+1)
end
pred Convert(i:<I, p:<Seq->>Purchase, prel::Item->rel Seq) iff
if {convert the matrix of purchases into an array of rels}
i <= 11 -> Convert2(Gloves,i,p(i),prel) & Convert(i+1,p,prel)
end
pred Convert2(t:<Item, i:<Seq, sp:<Purchase, prel::Item->rel Seq) iff
if
sp(t) = Yes -> i in prel(t)
true -> ~i in prel(t)
end &
if
t < Handbag -> Convert2(t+1,i,sp,prel)
end
------------------------------
End of PROLOG Digest
********************