Application Center - Maplesoft

# Solving constraint satisfaction problems II: More difficult logic problems

You can switch back to the summary page by clicking here.

MoreLogicProblems.mws

More example logic problems

Carl Devore <devore@math.udel.edu>

31 March 2001

> restart;

This application uses a Maple package called LP , contained in the file "LogicProblem.mpl", which is read by the next line. Make sure that file is in the same directory as this worksheet before executing.

A simple problem showing the use of the "Less" constraint.

This problem is adapted from Varda Reisner, "Logic Problem 1: Delivery Please" in Dell Math Puzzles and Logic Problems (No. 49, November 2000).

For each day, Tuesday to Friday, of last week, Wendy eats dinner at the local diner. Each day, she orders a meat (one was pork), a soup, and a vegetable. Determine the meat, soup, and vegetable for each day.

1. The beef was chosen earlier in the week than the French onion soup, which was chosen earlier than the carrots.

2. The chicken was chosen earlier in the week than the cream of broccoli soup, but later in the week than the spinach.

3. She didn't have fish on Friday.

4. The cream of mushroom soup was not chosen on Tuesday or Friday.

5. The black bean soup was served with the cauliflower.

6. The chicken was not served with the cabbage.

> V:= ['day', 'meat', 'soup', 'veg'];

> day:= [Tue, Wed, Thu, Fri];

> meat:= [pork, beef, chicken, fish];

> soup:= [onion, broc, mush, bean];

> veg:= [carrots, spinach, cauliflower, cabbage];

> st:= time():

> lp2:= LogicProblem(V):

Setting infolevel[TCdisplay] to 6 will print the appropriate submatrix everytime an "equality" is concluded. Setting to 7 will also print it everytime an "inequality" is concluded. Setting it to 8 will also print it everytime an entry is "ruled out" because an equality has been placed in its row or column. All of this is usually way too much information, but it is sometimes useful for debugging.

Setting infolevel[TC] to 5 and infolevel[Constraints] to 4 will show the entry and arguements to each recursive procedure. The "Level" numbers printed are Maple's internal representation of the recursion depth. This can help you track exactly where in the solution process a particular conclusion is reached.

> infolevel['TCdisplay']:= 6: infolevel['TC']:= 5: infolevel['Constraints']:= 4:

> lp2:-CollectStats:= true:

> lp2:-Satisfy([Less([beef,onion,carrots], day) #Clue 1
,Less([spinach,chicken,broc], day) #Clue 2
,Fri<>fish #3
,mush<>Tue, mush<>Fri #4
,bean=cauliflower #5
,chicken<>cabbage #6
]);

`Know:   Processing   [-2, Fri <> fish]`

`ParseAssertionTypes:   false, [-2, Fri <> fish]`

`Know/<>:   Fri, fish`

`&<!=>:   Conclusion   Fri <> fish   Level = 131`

`Elim:   1   2   Fri   fish   Level = 157`

`Elim:   2   1   fish   Fri   Level = 157`

`TransferX:   1   2   Fri   fish   Level = 152`

`TransferX:   2   1   fish   Fri   Level = 152`

`Know:   Processing   [-2, mush <> Tue]`

`ParseAssertionTypes:   false, [-2, mush <> Tue]`

`Know/<>:   mush, Tue`

`&<!=>:   Conclusion   mush <> Tue   Level = 131`

`Elim:   3   1   mush   Tue   Level = 157`

`Elim:   1   3   Tue   mush   Level = 157`

`TransferX:   3   1   mush   Tue   Level = 152`

`TransferX:   1   3   Tue   mush   Level = 152`

`Know:   Processing   [-2, mush <> Fri]`

`ParseAssertionTypes:   false, [-2, mush <> Fri]`

`Know/<>:   mush, Fri`

`&<!=>:   Conclusion   mush <> Fri   Level = 131`

`Elim:   3   1   mush   Fri   Level = 157`

`Elim:   1   3   Fri   mush   Level = 157`

`TransferX:   3   1   mush   Fri   Level = 152`

`TransferX:   1   3   Fri   mush   Level = 152`

`Know:   Processing   [-2, chicken <> cabbage]`

`ParseAssertionTypes:   false, [-2, chicken <> cabbage]`

`Know/<>:   chicken, cabbage`

`&<!=>:   Conclusion   chicken <> cabbage   Level = 131`

`Elim:   2   4   chicken   cabbage   Level = 157`

`Elim:   4   2   cabbage   chicken   Level = 157`

`TransferX:   2   4   chicken   cabbage   Level = 152`

`TransferX:   4   2   cabbage   chicken   Level = 152`

`Know:   Processing   [-3, bean = cauliflower]`

`ParseAssertionTypes:   false, [-3, bean = cauliflower]`

`Know/=:   bean, cauliflower`

`&<=>:   bean = cauliflower   Level = 131`

`TransClosure:   Conclusion   bean = cauliflower`

`RuleOut:   3   4   bean   cauliflower   Level = 178`

`RuleOut:   4   3   cauliflower   bean   Level = 178`

`Elim:   3   4   onion   cauliflower   Level = 183`

`Elim:   3   4   broc   cauliflower   Level = 183`

`Elim:   3   4   mush   cauliflower   Level = 183`

`Elim:   4   3   carrots   bean   Level = 183`

`Elim:   4   3   spinach   bean   Level = 183`

`Elim:   4   3   cabbage   bean   Level = 183`

`TransClosure:`

`Pivot:   3   4   bean   cauliflower   Level = 185`

`Pivot:   4   3   cauliflower   bean   Level = 185`

`Know:   Processing   [-6, Less([beef, onion, carrots],1)]`

`ParseAssertionTypes:   false, [-6, Less([beef, onion, carrots],1)]`

`Know/Less:   [beef, onion, carrots], 1`

`Less/OnePair:   beef, onion, 1`

`&<!=>:   Conclusion   beef <> onion   Level = 160`

`Elim:   2   3   beef   onion   Level = 186`

`Elim:   3   2   onion   beef   Level = 186`

`TransferX:   2   3   beef   onion   Level = 181`

`TransferX:   3   2   onion   beef   Level = 181`

`&<!=>:   Conclusion   onion <> Tue   Level = 160`

`Elim:   3   1   onion   Tue   Level = 186`

`Elim:   1   3   Tue   onion   Level = 186`

`TransferX:   3   1   onion   Tue   Level = 181`

`TransferX:   1   3   Tue   onion   Level = 181`

`&<!=>:   Conclusion   beef <> Fri   Level = 160`

`Elim:   2   1   beef   Fri   Level = 186`

`Elim:   1   2   Fri   beef   Level = 186`

`TransferX:   2   1   beef   Fri   Level = 181`

`TransferX:   1   2   Fri   beef   Level = 181`

`Less/RuleOutImpossible:   1   beef   onion`

`Less/OnePair:   beef, carrots, 1`

`&<!=>:   Conclusion   beef <> carrots   Level = 160`

`Elim:   2   4   beef   carrots   Level = 186`

`Elim:   4   2   carrots   beef   Level = 186`

`TransferX:   2   4   beef   carrots   Level = 181`

`TransferX:   4   2   carrots   beef   Level = 181`

`&<!=>:   Conclusion   carrots <> Tue   Level = 160`

`Elim:   4   1   carrots   Tue   Level = 186`

`Elim:   1   4   Tue   carrots   Level = 186`

`TransferX:   4   1   carrots   Tue   Level = 181`

`TransferX:   1   4   Tue   carrots   Level = 181`

`Less/RuleOutImpossible:   1   beef   carrots`

`Less/OnePair:   onion, carrots, 1`

`&<!=>:   Conclusion   onion <> carrots   Level = 160`

`Elim:   3   4   onion   carrots   Level = 186`

`Elim:   4   3   carrots   onion   Level = 186`

`TransferX:   3   4   onion   carrots   Level = 181`

`TransferX:   4   3   carrots   onion   Level = 181`

`&<!=>:   Conclusion   onion <> Fri   Level = 160`

`Elim:   3   1   onion   Fri   Level = 186`

`Elim:   1   3   Fri   onion   Level = 186`

`TransferX:   3   1   onion   Fri   Level = 181`

`TransferX:   1   3   Fri   onion   Level = 181`

`Less/RuleOutImpossible:   1   onion   carrots`

`&<!=>:   Conclusion   carrots <> Wed   Level = 188`

`Elim:   4   1   carrots   Wed   Level = 214`

`Elim:   1   4   Wed   carrots   Level = 214`

`TransferX:   4   1   carrots   Wed   Level = 209`

`TransferX:   1   4   Wed   carrots   Level = 209`

`Know:   Processing   [-6, Less([spinach, chicken, broc],1)]`

`ParseAssertionTypes:   false, [-6, Less([spinach, chicken, broc],1)]`

`Know/Less:   [spinach, chicken, broc], 1`

`Less/OnePair:   spinach, chicken, 1`

`&<!=>:   Conclusion   spinach <> chicken   Level = 160`

`Elim:   4   2   spinach   chicken   Level = 186`

`Elim:   2   4   chicken   spinach   Level = 186`

`TransferX:   4   2   spinach   chicken   Level = 181`

`TransferX:   2   4   chicken   spinach   Level = 181`

`&<!=>:   Conclusion   chicken <> Tue   Level = 160`

`Elim:   2   1   chicken   Tue   Level = 186`

`Elim:   1   2   Tue   chicken   Level = 186`

`TransferX:   2   1   chicken   Tue   Level = 181`

`TransferX:   1   2   Tue   chicken   Level = 181`

`&<!=>:   Conclusion   spinach <> Fri   Level = 160`

`Elim:   4   1   spinach   Fri   Level = 186`

`Elim:   1   4   Fri   spinach   Level = 186`

`TransferX:   4   1   spinach   Fri   Level = 181`

`TransferX:   1   4   Fri   spinach   Level = 181`

`Less/RuleOutImpossible:   1   spinach   chicken`

`Less/OnePair:   spinach, broc, 1`

`&<!=>:   Conclusion   spinach <> broc   Level = 160`

`Elim:   4   3   spinach   broc   Level = 186`

`Elim:   3   4   broc   spinach   Level = 186`

`TransferX:   4   3   spinach   broc   Level = 181`

`TransferX:   3   4   broc   spinach   Level = 181`

`&<!=>:   Conclusion   broc <> Tue   Level = 160`

`Elim:   3   1   broc   Tue   Level = 186`

`Elim:   1   3   Tue   broc   Level = 186`

`TransClosure:   Conclusion   Tue = bean`

`RuleOut:   1   3   Tue   bean   Level = 207`

`RuleOut:   3   1   bean   Tue   Level = 207`

`Elim:   1   3   Wed   bean   Level = 212`

`Elim:   1   3   Thu   bean   Level = 212`

`Elim:   1   3   Fri   bean   Level = 212`

`TransClosure:   Conclusion   Fri = broc`

`RuleOut:   1   3   Fri   broc   Level = 207`

`RuleOut:   3   1   broc   Fri   Level = 207`

`Elim:   1   3   Wed   broc   Level = 212`

`Elim:   1   3   Thu   broc   Level = 212`

`TransClosure:`

`Pivot:   1   3   Tue   bean   Level = 214`

`&<=>:   Tue = cauliflower   Level = 247`

`TransClosure:   Conclusion   Tue = cauliflower`

`RuleOut:   1   4   Tue   cauliflower   Level = 294`

`RuleOut:   4   1   cauliflower   Tue   Level = 294`

`Elim:   1   4   Wed   cauliflower   Level = 299`

`Elim:   1   4   Thu   cauliflower   Level = 299`

`Elim:   1   4   Fri   cauliflower   Level = 299`

`Elim:   4   1   spinach   Tue   Level = 299`

`Elim:   4   1   cabbage   Tue   Level = 299`

`TransClosure:`

`Pivot:   1   4   Tue   cauliflower   Level = 301`

`Pivot:   4   1   cauliflower   Tue   Level = 301`

`&<!=>:   Conclusion   cauliflower <> chicken   Level = 338`

`Elim:   4   2   cauliflower   chicken   Level = 364`

`Elim:   2   4   chicken   cauliflower   Level = 364`

`TransClosure:   Conclusion   chicken = carrots`

`RuleOut:   2   4   chicken   carrots   Level = 385`

`RuleOut:   4   2   carrots   chicken   Level = 385`

`Elim:   2   4   pork   carrots   Level = 390`

`Elim:   2   4   fish   carrots   Level = 390`

`TransClosure:`

`Pivot:   2   4   chicken   carrots   Level = 392`

`&<!=>:   Conclusion   chicken <> Wed   Level = 429`

`Elim:   2   1   chicken   Wed   Level = 455`

`Elim:   1   2   Wed   chicken   Level = 455`

`TransferX:   2   1   chicken   Wed   Level = 450`

`TransferX:   1   2   Wed   chicken   Level = 450`

`&<!=>:   Conclusion   chicken <> onion   Level = 429`

`Elim:   2   3   chicken   onion   Level = 455`

`Elim:   3   2   onion   chicken   Level = 455`

`TransferX:   2   3   chicken   onion   Level = 450`

`TransferX:   3   2   onion   chicken   Level = 450`

`&<!=>:   Conclusion   chicken <> bean   Level = 429`

`Elim:   2   3   chicken   bean   Level = 455`

`Elim:   3   2   bean   chicken   Level = 455`

`TransferX:   2   3   chicken   bean   Level = 450`

`TransferX:   3   2   bean   chicken   Level = 450`

`Pivot:   4   2   carrots   chicken   Level = 392`

`Pivot:   3   1   bean   Tue   Level = 214`

`Pivot:   1   3   Fri   broc   Level = 214`

`Pivot:   3   1   broc   Fri   Level = 214`

`&<!=>:   Conclusion   broc <> beef   Level = 251`

`Elim:   3   2   broc   beef   Level = 277`

`Elim:   2   3   beef   broc   Level = 277`

`TransferX:   3   2   broc   beef   Level = 272`

`TransferX:   2   3   beef   broc   Level = 272`

`&<!=>:   Conclusion   broc <> fish   Level = 251`

`Elim:   3   2   broc   fish   Level = 277`

`Elim:   2   3   fish   broc   Level = 277`

`TransferX:   3   2   broc   fish   Level = 272`

`TransferX:   2   3   fish   broc   Level = 272`

`Less/CheckForKnownPosition:   1   spinach   broc`

`Less/OnePair:   chicken, broc, 1`

`&<!=>:   Conclusion   chicken <> broc   Level = 160`

`Elim:   2   3   chicken   broc   Level = 186`

`Elim:   3   2   broc   chicken   Level = 186`

`TransClosure:   Conclusion   broc = pork`

`RuleOut:   3   2   broc   pork   Level = 207`

`RuleOut:   2   3   pork   broc   Level = 207`

`Elim:   3   2   onion   pork   Level = 212`

`Elim:   3   2   mush   pork   Level = 212`

`Elim:   3   2   bean   pork   Level = 212`

`TransClosure:   Conclusion   onion = fish`

`RuleOut:   3   2   onion   fish   Level = 207`

`RuleOut:   2   3   fish   onion   Level = 207`

`Elim:   3   2   mush   fish   Level = 212`

`Elim:   3   2   bean   fish   Level = 212`

`TransClosure:   Conclusion   bean = beef`

`RuleOut:   3   2   bean   beef   Level = 207`

`RuleOut:   2   3   beef   bean   Level = 207`

`Elim:   3   2   mush   beef   Level = 212`

`TransClosure:   Conclusion   mush = chicken`

`RuleOut:   3   2   mush   chicken   Level = 207`

`RuleOut:   2   3   chicken   mush   Level = 207`

`TransClosure:   Conclusion   chicken = mush`

`RuleOut:   2   3   chicken   mush   Level = 207`

`RuleOut:   3   2   mush   chicken   Level = 207`

`TransClosure:`

`Pivot:   3   2   broc   pork   Level = 214`

`&<!=>:   Conclusion   broc <> carrots   Level = 251`

`Elim:   3   4   broc   carrots   Level = 277`

`Elim:   4   3   carrots   broc   Level = 277`

`TransClosure:   Conclusion   carrots = mush`

`RuleOut:   4   3   carrots   mush   Level = 298`

`RuleOut:   3   4   mush   carrots   Level = 298`

`Elim:   4   3   spinach   mush   Level = 303`

`Elim:   4   3   cabbage   mush   Level = 303`

`TransClosure:   Conclusion   spinach = onion`

`RuleOut:   4   3   spinach   onion   Level = 298`

`RuleOut:   3   4   onion   spinach   Level = 298`

`Elim:   4   3   cabbage   onion   Level = 303`

`TransClosure:   Conclusion   cabbage = broc`

`RuleOut:   4   3   cabbage   broc   Level = 298`

`RuleOut:   3   4   broc   cabbage   Level = 298`

`TransClosure:   Conclusion   broc = cabbage`

`RuleOut:   3   4   broc   cabbage   Level = 298`

`RuleOut:   4   3   cabbage   broc   Level = 298`

`TransClosure:`

`Pivot:   4   3   carrots   mush   Level = 305`

`&<!=>:   Conclusion   carrots <> Fri   Level = 342`

`Elim:   4   1   carrots   Fri   Level = 368`

`Elim:   1   4   Fri   carrots   Level = 368`

`TransClosure:   Conclusion   Fri = cabbage`

`RuleOut:   1   4   Fri   cabbage   Level = 389`

`RuleOut:   4   1   cabbage   Fri   Level = 389`

`Elim:   1   4   Wed   cabbage   Level = 394`

`Elim:   1   4   Thu   cabbage   Level = 394`

`TransClosure:   Conclusion   Wed = spinach`

`RuleOut:   1   4   Wed   spinach   Level = 389`

`RuleOut:   4   1   spinach   Wed   Level = 389`

`Elim:   1   4   Thu   spinach   Level = 394`

`TransClosure:   Conclusion   Thu = carrots`

`RuleOut:   1   4   Thu   carrots   Level = 389`

`RuleOut:   4   1   carrots   Thu   Level = 389`

`TransClosure:   Conclusion   carrots = Thu`

`RuleOut:   4   1   carrots   Thu   Level = 389`

`RuleOut:   1   4   Thu   carrots   Level = 389`

`TransClosure:`

`Pivot:   1   4   Fri   cabbage   Level = 396`

`&<!=>:   Conclusion   Fri <> chicken   Level = 433`

`Elim:   1   2   Fri   chicken   Level = 459`

`Elim:   2   1   chicken   Fri   Level = 459`

`TransClosure:   Conclusion   chicken = Thu`

`RuleOut:   2   1   chicken   Thu   Level = 480`

`RuleOut:   1   2   Thu   chicken   Level = 480`

`Elim:   2   1   pork   Thu   Level = 485`

`Elim:   2   1   beef   Thu   Level = 485`

`Elim:   2   1   fish   Thu   Level = 485`

`TransClosure:   Conclusion   Fri = pork`

`RuleOut:   1   2   Fri   pork   Level = 480`

`RuleOut:   2   1   pork   Fri   Level = 480`

`Elim:   1   2   Tue   pork   Level = 485`

`Elim:   1   2   Wed   pork   Level = 485`

`TransClosure:`

`Pivot:   2   1   chicken   Thu   Level = 487`

`Pivot:   1   2   Thu   chicken   Level = 487`

`&<=>:   Thu = mush   Level = 520`

`TransClosure:   Conclusion   Thu = mush`

`RuleOut:   1   3   Thu   mush   Level = 567`

`RuleOut:   3   1   mush   Thu   Level = 567`

`Elim:   1   3   Wed   mush   Level = 572`

`Elim:   3   1   onion   Thu   Level = 572`

`TransClosure:   Conclusion   onion = Wed`

`RuleOut:   3   1   onion   Wed   Level = 567`

`RuleOut:   1   3   Wed   onion   Level = 567`

`TransClosure:   Conclusion   Wed = onion`

`RuleOut:   1   3   Wed   onion   Level = 567`

`RuleOut:   3   1   onion   Wed   Level = 567`

`TransClosure:`

`Pivot:   1   3   Thu   mush   Level = 574`

`Pivot:   3   1   mush   Thu   Level = 574`

`Pivot:   3   1   onion   Wed   Level = 574`

`Pivot:   1   3   Wed   onion   Level = 574`

`&<=>:   Wed = fish   Level = 607`

`TransClosure:   Conclusion   Wed = fish`

`RuleOut:   1   2   Wed   fish   Level = 654`

`RuleOut:   2   1   fish   Wed   Level = 654`

`Elim:   1   2   Tue   fish   Level = 659`

`Elim:   2   1   beef   Wed   Level = 659`

`TransClosure:   Conclusion   beef = Tue`

`RuleOut:   2   1   beef   Tue   Level = 654`

`RuleOut:   1   2   Tue   beef   Level = 654`

`TransClosure:   Conclusion   Tue = beef`

`RuleOut:   1   2   Tue   beef   Level = 654`

`RuleOut:   2   1   beef   Tue   Level = 654`

`TransClosure:`

`Pivot:   1   2   Wed   fish   Level = 661`

`Pivot:   2   1   fish   Wed   Level = 661`

`&<=>:   fish = spinach   Level = 694`

`TransClosure:   Conclusion   fish = spinach`

`RuleOut:   2   4   fish   spinach   Level = 741`

`RuleOut:   4   2   spinach   fish   Level = 741`

`Elim:   2   4   pork   spinach   Level = 746`

`Elim:   2   4   beef   spinach   Level = 746`

`Elim:   4   2   cauliflower   fish   Level = 746`

`Elim:   4   2   cabbage   fish   Level = 746`

`TransClosure:`

`Pivot:   2   4   fish   spinach   Level = 748`

`Pivot:   4   2   spinach   fish   Level = 748`

`Pivot:   2   1   beef   Tue   Level = 661`

`&<=>:   beef = cauliflower   Level = 694`

`TransClosure:   Conclusion   beef = cauliflower`

`RuleOut:   2   4   beef   cauliflower   Level = 741`

`RuleOut:   4   2   cauliflower   beef   Level = 741`

`Elim:   2   4   pork   cauliflower   Level = 746`

`Elim:   4   2   cabbage   beef   Level = 746`

`TransClosure:   Conclusion   cabbage = pork`

`RuleOut:   4   2   cabbage   pork   Level = 741`

`RuleOut:   2   4   pork   cabbage   Level = 741`

`TransClosure:   Conclusion   pork = cabbage`

`RuleOut:   2   4   pork   cabbage   Level = 741`

`RuleOut:   4   2   cabbage   pork   Level = 741`

`TransClosure:`

`Pivot:   2   4   beef   cauliflower   Level = 748`

`Pivot:   4   2   cauliflower   beef   Level = 748`

`Pivot:   4   2   cabbage   pork   Level = 748`

`Pivot:   2   4   pork   cabbage   Level = 748`

`Pivot:   2   4   pork   cabbage   Level = 748`

`Pivot:   4   2   cabbage   pork   Level = 748`

`Pivot:   1   2   Tue   beef   Level = 661`

`Pivot:   1   2   Tue   beef   Level = 661`

`Pivot:   2   1   beef   Tue   Level = 661`

`Pivot:   1   3   Wed   onion   Level = 574`

`Pivot:   3   1   onion   Wed   Level = 574`

`Pivot:   1   2   Fri   pork   Level = 487`

`Pivot:   2   1   pork   Fri   Level = 487`

`Pivot:   4   1   cabbage   Fri   Level = 396`

`Pivot:   1   4   Wed   spinach   Level = 396`

`Pivot:   4   1   spinach   Wed   Level = 396`

`Pivot:   1   4   Thu   carrots   Level = 396`

`Pivot:   4   1   carrots   Thu   Level = 396`

`Pivot:   4   1   carrots   Thu   Level = 396`

`Pivot:   1   4   Thu   carrots   Level = 396`

`Pivot:   3   4   mush   carrots   Level = 305`

`Pivot:   4   3   spinach   onion   Level = 305`

`Pivot:   3   4   onion   spinach   Level = 305`

`Pivot:   4   3   cabbage   broc   Level = 305`

`Pivot:   3   4   broc   cabbage   Level = 305`

`Pivot:   3   4   broc   cabbage   Level = 305`

`Pivot:   4   3   cabbage   broc   Level = 305`

`Pivot:   2   3   pork   broc   Level = 214`

`Pivot:   3   2   onion   fish   Level = 214`

`Pivot:   2   3   fish   onion   Level = 214`

`Pivot:   3   2   bean   beef   Level = 214`

`Pivot:   2   3   beef   bean   Level = 214`

`Pivot:   3   2   mush   chicken   Level = 214`

`Pivot:   2   3   chicken   mush   Level = 214`

`Pivot:   2   3   chicken   mush   Level = 214`

`Pivot:   3   2   mush   chicken   Level = 214`

`Less/CheckForKnownPosition:   1   chicken   broc`

`Less/Check:   Constraint   Less(chicken,broc,1)   completely satisfied.`

`Know:   Processing   [-7, Less(onion,carrots,1)]`

`ParseAssertionTypes:   false, [-7, Less(onion,carrots,1)]`

`Less/OnePair:   onion, carrots, 1`

`Less/Check:   Constraint   Less(onion,carrots,1)   completely satisfied.`

`Know:   Processing   [-7, Less(spinach,broc,1)]`

`ParseAssertionTypes:   false, [-7, Less(spinach,broc,1)]`

`Less/OnePair:   spinach, broc, 1`

`Less/Check:   Constraint   Less(spinach,broc,1)   completely satisfied.`

`Know:   Processing   [-7, Less(spinach,chicken,1)]`

`ParseAssertionTypes:   false, [-7, Less(spinach,chicken,1)]`

`Less/OnePair:   spinach, chicken, 1`

`Less/Check:   Constraint   Less(spinach,chicken,1)   completely satisfied.`

`Know:   Processing   [-7, Less(beef,carrots,1)]`

`ParseAssertionTypes:   false, [-7, Less(beef,carrots,1)]`

`Less/OnePair:   beef, carrots, 1`

`Less/Check:   Constraint   Less(beef,carrots,1)   completely satisfied.`

`Know:   Processing   [-7, Less(beef,onion,1)]`

`ParseAssertionTypes:   false, [-7, Less(beef,onion,1)]`

`Less/OnePair:   beef, onion, 1`

`Less/Check:   Constraint   Less(beef,onion,1)   completely satisfied.`

`NormalReturn:   Conclusions:   102`

> time()-st;

> lp2:-`&?`(ShowStats);

> interface(rtablesize= 24);

Note that if you do not use the "with" command, then you must call &? with quotes and parentheses or use a "use" statement. The same is true of any other procedure whose name begins with "&". The "use" statement is more elegant:

> use lp2 in &? ShowStats end;

> use lp2 in &? day end;

An example with a lot of "Less" constraints and a relatively simple procedural constraint.

This problem is adapted from Frank Alward "Logic Problem 3: White-Water Rafting" in Dell Math Puzzles and Logic Problems (No. 49, November 2000).

In a marathon race, prizes were awarded (one was a DVD player) to the first 5 finishers (one was Mr. Young). Each of these 5 wore a different color jersey (one was yellow). Determine the first and last name, placement, jersey color, and prize of each of the 5.

1. The blue jersey was in 1st place.

2. The mountain bike was awarded to 5th place.

3. Mr. Bowker did not win the stereo.

4. The runner who won the VCR, whose jersey was neither red nor white, finished behind both the runner in the green jersey and the winner of the TV.

5. Mr. Sparks, who isn't Al, finished 2 places ahead of Otis.

6. Mr. Nolan and Mr. Sparks finished behind Mark, but all 3 finished before Mr. Stover and the winner of the stereo.

7. The runner in the red jersey finished before Del.

> V:= ['place', 'first', 'last', 'color', 'prize'];

> place:= [\$1..5];

> first:= [Al, Del, Larry, Mark, Otis];

> last:= [Bowker, Nolan, Sparks, Stover, Young];

> color:= [blue, green, red, white, yellow];

> prize:= [bike, dvd, stereo, tv, vcr];

> lp3:= LogicProblem(V):

Clue #5 cannot be completely handled by any of the constraint types that we've discussed so far. One approach is to use the following procedural constraint.

> ClueSparksOtis:= proc(M)
local sparks, otis, internal_place, place_sparks, place_otis;
use `&Soln`= M:-`&Soln`, ConstNum= M:-ConstNum, VarNum= M:-VarNum in
sparks,otis:= ConstNum(Sparks), ConstNum(Otis);
internal_place:= VarNum(place);
place_sparks:= sparks &Soln internal_place;
place_otis:= otis &Soln internal_place
end use;
if place_sparks > 0 and place_otis > 0 then
if place_otis - place_sparks = 2 then false,true #completely satisfied
end
#If we know the place of one of them, we can definitely specify the place of the other
elif place_sparks > 0 then false, false, [Otis = place_sparks+2]
elif place_otis > 0 then false, false, [Sparks = place_otis-2]
else false, false, [] #Consistent (so far), but not satisfied
end
end;

> with(lp3);

> infolevel['Constraints']:= 2: infolevel['TC']:= 1: infolevel['TCdisplay']:= 0: CollectStats:= true:

To specify clue 5, it is useful for the sake of efficiency (though it is not necessary) to say everything that can be said with the predefined constraint types in addition to giving the procedural constraint.

> Clue5:= Al<>Sparks, Less(Sparks, Otis, place), Sparks<>4, Otis<>2, Proc(ClueSparksOtis, []);

> Constraints:=
[blue=1 #Clue 1
,bike=5 #Clue 2
,Bowker<>stereo #Clue 3

#The 5 parts of the next line are required to completely specify Clue 4
,vcr<>red, vcr<>white, Less(green, vcr, place), Less(tv, vcr, place), tv<>green

,_Clue5

#The next 5 items completely specify Clue 6.
,Less([Mark, Nolan, Stover], place), Less([Mark, Sparks, Stover], place)
,Less([Mark, Nolan, stereo], place), Less([Mark, Sparks, stereo], place)
,Stover<>stereo

#Clue 7
,Less(red,Del,place)
];

> st:= time():

> Satisfy(subs(_Clue5= Clue5, Constraints));

`Less/Check:   Constraint   Less(Mark,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(green,vcr,1)   completely satisfied.`

`Less/Check:   Constraint   Less(red,Del,1)   completely satisfied.`

`Less/Check:   Constraint   Less(tv,vcr,1)   completely satisfied.`

`Satisfy:`

`Backup:   Guessing   Larry = 2   Depth=   1`

`Less/Check:   Constraint   Less(Nolan,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Nolan,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Sparks,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Nolan,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,Otis,1)   completely satisfied.`

`Know/Proc:   Proc(ClueSparksOtis,[])   satisfied.`

`Satisfy:`

`GoBack:   Restoring saved state from before guess   Larry = 2   Depth=   0`

`Less/Check:   Constraint   Less(Nolan,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Nolan,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Sparks,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,Otis,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Nolan,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,Stover,1)   completely satisfied.`

`Know/Proc:   Proc(ClueSparksOtis,[])   contradicted.`

> time()-st;

> &? ShowStats;

Note that Clue 5 actually specifies a relationship between two constants and a variable. This is the same situation as with constraint types Succ, Less, and NextTo. In this case, it is simpler and more efficient to specify the constraint via the Relational/Procedure contraint type. We can consider this particular relationship as being "AheadBy2".

> AheadBy2:= (M, a, b) -> `if`(b=0, {a+2}, `if`(a=0, {b-2}, evalb(b-a<>2)));

Note how much simpler it is to specify the constraint in this form.

> Clue5;

> Clue5:= Al<>Sparks, Rel(AheadBy2, Sparks, Otis, place, []);

> Reinitialize();

> st:= time():

> Satisfy(subs(_Clue5= Clue5, Constraints));

`Less/Check:   Constraint   Less(Mark,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(green,vcr,1)   completely satisfied.`

`Less/Check:   Constraint   Less(tv,vcr,1)   completely satisfied.`

`Less/Check:   Constraint   Less(red,Del,1)   completely satisfied.`

`Rel/Check:   Constraint   Rel(AheadBy2,Sparks,Otis,1,[])   satisfied.`

`Less/Check:   Constraint   Less(Nolan,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Sparks,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Nolan,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Nolan,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,stereo,1)   completely satisfied.`

> time()-st;

> &? ShowStats;

Note how much more efficient it is to use the Relational/Procedural constraint type. A Proc/Procedural clue that is hard to satisfy leads to inefficient guessing and backtracking.

The relationship expressed by "AheadBy2" already exists as a predefined constraint type "Equation".

> Clue5;

> Clue5:= Al<>Sparks, Rel(Equation, Sparks, Otis, place, [{_A+2}, {_B-2}]);

The first expression in brackets represents the solution set for the second constant's (in this case Otis) position given that the first constant's (in this case Sparks) position is known; the second expression represents to solutions for the first constant's position given that the second constant's position is known. Note the the symbols _A and _B must be used.

> Reinitialize();

> st:= time():

> Satisfy(subs(_Clue5= Clue5, Constraints));

`Less/Check:   Constraint   Less(Mark,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(green,vcr,1)   completely satisfied.`

`Less/Check:   Constraint   Less(tv,vcr,1)   completely satisfied.`

`Less/Check:   Constraint   Less(red,Del,1)   completely satisfied.`

`Rel/Check:   Constraint   Rel(Equation,Sparks,Otis,1,[{_A+2}, {_B-2}])   satisfied.`

`Less/Check:   Constraint   Less(Nolan,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,Stover,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Sparks,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Nolan,stereo,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Mark,Nolan,1)   completely satisfied.`

`Less/Check:   Constraint   Less(Sparks,stereo,1)   completely satisfied.`

> time()-st;

> &? ShowStats;

An example problem with dummy variables and what to do when some of the variables are not the right size.

This problem is adapted from Diane Yoko "Logic Problem 7: Christmastime Already!?!" in Dell Math Puzzles and Logic Problems (No. 49, November 2000)

Dan and five of his friends each bought distinct types of Christmas trees (one was a spruce) from distinct vendors on not-necessarily-distinct days, Monday to Friday, of last week. Determine each friends' first and last name, type of tree, vendor, and day of purchase.

1. A person's sex can be determined in the natural way from their first name.

2. Anne bought her tree from a private farm.

3. M. Turner and Eva bought trees on Wednesday.

4. M. Turner is married.

5. M. Turner didn't buy the white pine.

6. A single woman bought a tree from Andrews' Nursery.

7. The Douglas fir wasn't the tree Mr. Stevens bought on Monday.

8. Sally and M. Jansen are both married; Irene and M. Hall are both single; four distinct persons are mentioned in this clue.

9. M. Eden didn't buy the white pine or the Douglas fir.

10. Theo wasn't the man who bought the Scotch pine on Thursday.

11. The Christmas store did not sell the Douglas fir.

12. The balsam was bought by a woman on Tuesday.

13. Sally's tree wasn't from Caine's Nursery.

14. Mr. Conner bought his tree from Bank's Nursery.

15. The tree from the department store was bought on Friday.

16. The tree from the department store wasn't the artificial one.

In order to use the Logic Puzzle program, we need to state the problem in terms of equivalence relations. The first problem with that is that we need 6 equivalence classes, but there are only five days Monday to Friday. A quick reading of the clues shows that a tree was purchased on each of those days and two were purchased on Wednesday. Thus, we will put two tokens for Wednesday in the varibable 'day'. The second problem is that sex and marital status are obviously important pieces of information, though they are not explicitly asked for. We can figure out everyone's sex by clue 1. But we can't figure out everyone's marital status. By clue 8, there are at least two married persons and at least two single persons. We create a variable 'status' that assumes the values M1, M2, S1, S2, U1, U2. These stand for "married person 1", "married person 2", "single person 1", "single person 2", "unknown person 1", "unknown person 2". It is possible to completely solve the problem as stated without explicitly determining the marital status of those two unknowns.

> V:= ['first', 'last', 'vendor', 'tree', 'day', 'sex', 'status'];

> first:= [Anne, Dan, Eva, Irene, Sally, Theo];

> last:= [Conner,Eden,Hall,Jansen,Stevens,Turner];

> vendor:= [Andrews, Banks, Caines, Christmas, Dept, farm];

> tree:= [art, balsam, fir, scotch, spruce, white];

> day:= [Mon, Tue, Wed1, Wed2, Thu, Fri];

2 males and 4 females.

> sex:= [m1,m2,f1,f2,f3,f4];

> status:= [M1,M2,U1,U2,S1,S2];

> Constraints:=
[Dan=m1, Theo=m2, Eva=f1, Irene=f2, Sally=f3, Anne=f4 #Clue 1
,Anne=farm #Clue 2
,Turner=Wed1, Eva=Wed2 #Clue 3
,Turner=M1 #Clue 4
,Turner<>white #Clue 5
,Distinct([S1, {m1,m2}]) #Clue 6 "a single woman..."
,S1=Andrews #Clue 6
,Distinct([Stevens, {f||(1..4)}]) #Clue 7: Stevens is male. We can't say whether he is m1 or m2.
#Note that I could have said OR([Stevens=m1, Stevens=m2]), but the Distinct contraint type is far more efficient
,Stevens=Mon, Stevens<>fir #Clue 7

#The next 5 items are required to specify Clue 8
,Distinct([Sally,Jansen,Irene,Hall])
,Distinct([{Sally, Jansen}, {U1,U2,S1,S2}])
,Distinct([{Irene, Hall}, {M1,M2,U1,U2}])

,Distinct([Eden, {white, fir}]) #Clue 9
,scotch=Thu, Distinct([Thu, {Theo, f||(1..4)}]) #Clue 10
,Christmas<>fir #Clue 11
,balsam=Tue, Distinct([balsam, {m1,m2}]) #Clue 12
,Sally<>Caines #Clue 13
,Distinct([Conner, {f||(1..4)}]), Conner=Banks #Clue 14
,Dept=Fri #Clue 15
,Dept<>art #Clue 16
];

> lp4:= LogicProblem(V):

> st:= time():

> infolevel['Constraints']:= 1: infolevel['TC']:= 1:

> lp4:-Satisfy(Constraints);

> time()-st;

> lp4:-`&?`(CountGuesses);

Since there are no undisproved guesses, it is clear that the required solution on the first five variables is complete and unique.

A more complex example with a more complicated uniqueness proof.

This problem is adapted from Jean Hannagan "Logic Problem 10: Letters to the Editor" in Dell Math Puzzles and Logic Problems (No. 49, November 2000).

Last month, each of five freelance food writers (one's first name is Kit) for a magazine received a letter from a reader pointing out a mistake in a recent article they had written. Each writer lives in a different town (one lives in Forest Park). One writer decided to quit, and each of the others mailed a correction. Each article was about a different subject (one was a new restaurant). Determine each writers full name, the subject of their article, the town they live in, and the order in which their complaint letters were received. Also determine which writer decided to quit.

1. The sexes cannot be determined from the first names.

2. Kevin didn't write the article about garlic.

3. Kevin received his letter sometime after the one who wrote about herbs.

4. Kevin mailed his correction along with a new story (i.e., Kevin did not quit).

5. Lee isn't M. Ware.

6. Lee received a letter after the one who wrote about desserts.

7. The one who wrote about roasting vegetables received her letter before the Cedar Grove resident.

8. Lee isn't M. Landis.

9. M. Landis got a letter sometime after the one who wrote an article on desserts.

10. Sal's letter arrived sometime after M. Turner's.

11. The recipient of the first letter did not write about herbs.

12. The recipient of the first letter did not quit.

13. The letter about roasting vegetables came after the one about herbs.

14. The article about herbs wasn't written by the man who lives in Sunrise Acres.

15. Kevin's letter arrived before the one for the resident of Cedar Grove.

16. The writer from Cedar Grove did not write about garlic.

17. Sal's letter arrived before the Spring Ridge resident received his.

18. The Pine Landing resident isn't M. Banks.

19. The Pine Landing resident received a letter before M. Ware.

20. M. Banks received a letter before Lou.

21. Neither M. Banks nor Lou decided to quit.

> V:= ['first','last','subject','city','When','quitter','sex'];

> first:= [Kevin,Kit,Lee,Lou,Sal];

> last:= [Banks,Colson,Landis,Turner,Ware];

> subject:= [dessert,garlic,herbs,New,roast];

> city:= [Cedar,Forest,Pine,Spring,Sunrise];

> When:= [\$1..5];

We need four dummy constants for the four writers who did not quit.

> quitter:= [q,n1,n2,n3,n4];

There are clearly at least two men and at least one woman. The other two are of unknown sex.

> sex:= [m1,m2,u1,u2,f];

> Constraints:=
[Kevin<>garlic #Clue 2
,Less(herbs,Kevin,When) #Clue 3
,Kevin<>q, Distinct([Kevin, {u1,u2,f}]) #Clue 4
,Lee<>Ware #Clue 5
,Less(dessert,Lee,When) #Clue 6
,Less(roast,Cedar,When), roast=f #Clue 7
,Lee<>Landis #Clue 8
,Less(dessert,Landis,When) #Clue 9
,Less(Turner,Sal,When) #Clue 10
,1<>herbs #Clue 11
,1<>q #Clue 12
,Less(herbs,roast,When) #Clue 13
,herbs<>Sunrise, Distinct([Sunrise, {u1,u2,f}]) #Clue 14
,Less(Kevin,Cedar,When) #Clue 15
,Cedar<>garlic #Clue 16
,Less(Sal,Spring,When), Distinct([Spring, {u1,u2,f}]) #Clue 17
,Pine<>Banks #Clue 18
,Less(Pine,Ware,When) #Clue 19
,Less(Banks,Lou,When) #Clue 20
,Banks<>q, Lou<>q #Clue 21
];

> infolevel['TC']:= 1: infolevel['Constraints']:= 2: infolevel['all']:= 0:

> lp5:= LogicProblem(V):

> st:= time():

> lp5:-Satisfy(Constraints);

`Satisfy:`

`Backup:   Guessing   Spring = Kevin   Depth=   1`

`Satisfy:`

`Backup:   Guessing   q = roast   Depth=   2`

`Satisfy:`

`Backup:   Guessing   q = Lee   Depth=   3`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Pine,Ware,5)   completely satisfied.`

`Less/Check:   Cannot satisfy   Less(dessert,Lee,5)`

`NegateLastGuess:   Backing up to last guess.   Level = 95   Depth = 3`

`GoBack:   Restoring saved state from before guess   q = Lee   Depth=   2`

`Less/Check:   Constraint   Less(dessert,Landis,5)   completely satisfied.`

`Less/Check:   Cannot satisfy   Less(dessert,Lee,5)`

`NegateLastGuess:   Backing up to last guess.   Level = 95   Depth = 2`

`GoBack:   Restoring saved state from before guess   q = roast   Depth=   1`

`Satisfy:`

`Backup:   Guessing   q = 5   Depth=   2`

`Satisfy:`

`Backup:   Guessing   q = Cedar   Depth=   3`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Cannot satisfy   Less(dessert,Landis,5)`

`NegateLastGuess:   Backing up to last guess.   Level = 95   Depth = 3`

`GoBack:   Restoring saved state from before guess   q = Cedar   Depth=   2`

`&<=>:   Contradicts   roast <> Spring`

`NegateLastGuess:   Backing up to last guess.   Level = 90   Depth = 2`

`GoBack:   Restoring saved state from before guess   q = 5   Depth=   1`

`Satisfy:`

`Backup:   Guessing   5 = Cedar   Depth=   2`

`Less/Check:   Constraint   Less(dessert,Lee,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,roast,5)   completely satisfied.`

`Less/Check:   Constraint   Less(roast,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Sal,Spring,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Banks,Lou,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,Kevin,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Kevin,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Landis,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Pine,Ware,5)   completely satisfied.`

> time()-st;

> lp5:-`&?`(ActiveGuesses);

We have a complete answer to the stated problem. It is not necessarily unique because of the guesses. Let's see if we can prove uniqueness for a restriction of the above problem. Then I will extend the proof to the whole problem. I will eliminate the quitter variable. Obviously, there is no way to distiguish m1 and m2. Let's be definite and say that the man from Sunrise Acres is m1 and the man from Spring Ridge is m2. Also, we can't distinguish u1 and u2. By clue 7, the known woman is not from Cedar Grove. Let's say the person from Cedar Grove is u1. The rest is cut-and-paste from above.

> V2:= ['first','last','subject','city','When','sex'];

> Constraints:=
[Kevin<>garlic #Clue 2
,Less(herbs,Kevin,When) #Clue 3
# ,Kevin<>q
,Distinct([Kevin, {u1,u2,f}]) #Clue 4
,Lee<>Ware #Clue 5
,Less(dessert,Lee,When) #Clue 6
,Less(roast,Cedar,When), roast=f, Cedar=u1 #Clue 7 #new info added here
,Lee<>Landis #Clue 8
,Less(dessert,Landis,When) #Clue 9
,Less(Turner,Sal,When) #Clue 10
,1<>herbs #Clue 11
# ,1<>q #Clue 12
,Less(herbs,roast,When) #Clue 13
,herbs<>Sunrise, Sunrise=m1 #Clue 14 #new info added here
,Less(Kevin,Cedar,When) #Clue 15
,Cedar<>garlic #Clue 16
,Less(Sal,Spring,When), Spring=m2 #Clue 17 #new info added here
,Pine<>Banks #Clue 18
,Less(Pine,Ware,When) #Clue 19
,Less(Banks,Lou,When) #Clue 20
# ,Banks<>q, Lou<>q #Clue 21
];

This shows why it is useful to use the module structure to have two problems active at the same time.

> lp5_2:= LogicProblem(V2):

> st:= time():

> lp5_2:-Satisfy(Constraints);

`Satisfy:`

`Backup:   Guessing   5 = Cedar   Depth=   1`

`Satisfy:`

`Backup:   Guessing   New = Landis   Depth=   2`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Lee,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Pine,Ware,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Banks,Lou,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,roast,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Sal,Spring,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Landis,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Kevin,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(roast,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,Kevin,5)   completely satisfied.`

`Satisfy:`

`GoBack:   Restoring saved state from before guess   New = Landis   Depth=   1`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Lee,5)   completely satisfied.`

`Less/Check:   Cannot satisfy   Less(Pine,Ware,5)`

`NegateLastGuess:   Backing up to last guess.   Level = 95   Depth = 1`

`GoBack:   Restoring saved state from before guess   5 = Cedar   Depth=   0`

`&<!=>:   Contradicts   4 = Cedar`

> time()-st;

> with(lp5);

```Warning, these names have been rebound: &!!, &-, &<, &>, &?, &G, &Soln, CollectStats, ConstNum, Consts, ConstsInV, DifferentBlock, FreeGuess, GoBack, Guess, InternalRep, IsComplete, IsUnique, NC, NV, PrintConst, Reinitialize, SameBlock, Satisfy, Separated, VarNum, VarNumC
```

> Reinitialize();

Now we go back to the original problem using the dummy variable assignments from the restricted problem and putting the quitter constraints back in:

> Constraints:=
[Kevin<>garlic #Clue 2
,Less(herbs,Kevin,When) #Clue 3
,Kevin<>q
,Distinct([Kevin, {u1,u2,f}]) #Clue 4
,Lee<>Ware #Clue 5
,Less(dessert,Lee,When) #Clue 6
,Less(roast,Cedar,When), roast=f, Cedar=u1 #Clue 7
,Lee<>Landis #Clue 8
,Less(dessert,Landis,When) #Clue 9
,Less(Turner,Sal,When) #Clue 10
,1<>herbs #Clue 11
,1<>q #Clue 12
,Less(herbs,roast,When) #Clue 13
,herbs<>Sunrise, Sunrise=m1 #Clue 14
,Less(Kevin,Cedar,When) #Clue 15
,Cedar<>garlic #Clue 16
,Less(Sal,Spring,When), Spring=m2 #Clue 17
,Pine<>Banks #Clue 18
,Less(Pine,Ware,When) #Clue 19
,Less(Banks,Lou,When) #Clue 20
,Banks<>q, Lou<>q #Clue 21
];

> infolevel['TC']:= 1: infolevel['Constraints']:= 2:

> Satisfy(Constraints);

`Satisfy:`

`Backup:   Guessing   Sunrise = Kit   Depth=   1`

`Satisfy:`

`Backup:   Guessing   New = Landis   Depth=   2`

`Less/Check:   Constraint   Less(Pine,Ware,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Landis,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,roast,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Banks,Lou,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Kevin,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Lee,5)   completely satisfied.`

`Less/Check:   Constraint   Less(roast,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,Kevin,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Sal,Spring,5)   completely satisfied.`

I want to know what was known about the quitter before any guesses were made. Procedure GoBack restores the problem state to what is was before the last guess.

> to &? CountGuesses do GoBack() end;

`GoBack:   Restoring saved state from before guess   New = Landis   Depth=   1`

`GoBack:   Restoring saved state from before guess   Sunrise = Kit   Depth=   0`

The return values of GoBack() are the guesses. I don't care about them for this problem.

Let's see what was known about the quitter:

> &? q;

Kevin, Kit, and Lou are obviously distinct entities (they are all first names). There is no way to distinguish n1, n2, n3, and n4. So we arbitrarily assign Kevin=n1, Kit= n2, Lou= n3.

> st:= time():

> Reinitialize();

> Constraints:=
[Kevin<>garlic #Clue 2
,Less(herbs,Kevin,When) #Clue 3
,Kevin= n1, Kit= n2, Lou= n3
,Distinct([Kevin, {u1,u2,f}]) #Clue 4
,Lee<>Ware #Clue 5
,Less(dessert,Lee,When) #Clue 6
,Less(roast,Cedar,When), roast=f, Cedar=u1 #Clue 7
,Lee<>Landis #Clue 8
,Less(dessert,Landis,When) #Clue 9
,Less(Turner,Sal,When) #Clue 10
,1<>herbs #Clue 11
,1<>q #Clue 12
,Less(herbs,roast,When) #Clue 13
,herbs<>Sunrise, Sunrise=m1 #Clue 14
,Less(Kevin,Cedar,When) #Clue 15
,Cedar<>garlic #Clue 16
,Less(Sal,Spring,When), Spring=m2 #Clue 17
,Pine<>Banks #Clue 18
,Less(Pine,Ware,When) #Clue 19
,Less(Banks,Lou,When) #Clue 20
,Banks<>q, Lou<>q #Clue 21
];

> Satisfy(Constraints);

`Satisfy:`

`Backup:   Guessing   n1 = Spring   Depth=   1`

`Satisfy:`

`Backup:   Guessing   1 = Sunrise   Depth=   2`

`Satisfy:`

`Backup:   Guessing   New = Landis   Depth=   3`

`Less/Check:   Constraint   Less(dessert,Lee,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,roast,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,Kevin,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Kevin,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Pine,Ware,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Landis,5)   completely satisfied.`

`Less/Check:   Constraint   Less(roast,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Sal,Spring,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Banks,Lou,5)   completely satisfied.`

`Satisfy:`

`GoBack:   Restoring saved state from before guess   New = Landis   Depth=   2`

`Less/Check:   Constraint   Less(dessert,Lee,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,roast,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Banks,Lou,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,Kevin,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Kevin,Cedar,5)   completely satisfied.`

`Less/Check:   Cannot satisfy   Less(Pine,Ware,5)`

`NegateLastGuess:   Backing up to last guess.   Level = 95   Depth = 2`

`GoBack:   Restoring saved state from before guess   1 = Sunrise   Depth=   1`

`&<!=>:   Contradicts   herbs = Cedar`

`NegateLastGuess:   Backing up to last guess.   Level = 90   Depth = 1`

`GoBack:   Restoring saved state from before guess   n1 = Spring   Depth=   0`

`&<=>:   Contradicts   2 <> Kevin`

Voila.

> time()-st;

A large portion of the time is often taken by the uniqueness proof. Often a uniqueness proof is unnecessary. For example, you may already know that the solution is unique, or you may not care if the solution is unique. Let's redo the same problem without getting a uniqueness proof.

> UniquenessProof:= false:

> Reinitialize();

> st:= time():

> Satisfy(Constraints);

`Satisfy:`

`Backup:   Guessing   n1 = Spring   Depth=   1`

`Satisfy:`

`Backup:   Guessing   1 = Sunrise   Depth=   2`

`Satisfy:`

`Backup:   Guessing   New = Landis   Depth=   3`

`Less/Check:   Constraint   Less(dessert,Lee,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,roast,5)   completely satisfied.`

`Less/Check:   Constraint   Less(herbs,Kevin,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Kevin,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Pine,Ware,5)   completely satisfied.`

`Less/Check:   Constraint   Less(dessert,Landis,5)   completely satisfied.`

`Less/Check:   Constraint   Less(roast,Cedar,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Turner,Sal,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Sal,Spring,5)   completely satisfied.`

`Less/Check:   Constraint   Less(Banks,Lou,5)   completely satisfied.`

> time()-st;

> &? ShowStats;

>

A puzzle with a two-dimensional spatial relationships and several complex procedural clues.

"Tailgate Party" in Dell Champion: The Best of Logic Puzzles (Feb. 1998).

Ina Rush was caught in a terrific traffic jam last Wednesday around lunch time. Traffic was completely stopped for nearly an hour, but Ina made the best of it by introducing herself to the drivers of the eight cars around hers, and encouraging them to treat the situation as an impromptu picnic. Four of the eight drivers were male (Carl, Joe, Rudy, and Otto), and four were female (Bea, Dee, Elaine, and Emma). From this information and the following clues, match each driver's full name (one last name is Poeler) with the color of his or her car, and locate the car on the chart below.

1 2 3

4 I 5

6 7 8

[The printed chart indicates that Ina is in the middle.]

1. The car just in front of Ina was the same color as the car just to her left, while the car just behind Ina was the same color as the car just to her right.

2. Ms. Kamuter shared some of her lunch with Mr. Blough, who was stopped in the same lane as her, and with Elaine, who was in a different lane.

3. Ms. Stucke passed a can of soda to the driver of a blue car just to her right.

4. Otto shared his potato salad with the two women on his immediate left and right, who were (not necessarily respectively) Ms. Toots and the driver of a gray car.

5. Emma and Ms. Stucke both were driving red cars.

6. Carl (who isn't Mr. Blough) gave his extra slice of apple pie to the driver of a green car that was somewhere ahead of him in the same lane.

7. Ms. Trapt and Dee (neither of whom drove a red car) traded half of their sandwiches with each other.

8. Rudy and Mr. Cruize were driving black cars.

9. Mr. Horne shared a small carton of ice cream with the driver of a white car,

With a careful reading, we see that the colors are 2 red, 1 blue, 2 black, 1 white, 1 gray, and 1 green. This is the type of thing that must be determined by the user before the Logic Problem program can even begin to be used.

> V:= ['first', 'last', 'color', 'place']:

> Men:= {Carl, Joe, Rudy, Otto}: Women:= {Bea, Dee, Elaine, Emma}:

> first:= [op(Men), op(Women)]:

> last:= [Poeler, Kamuter, Blough, Stucke, Toots, Trapt, Cruize, Horne]:

> color:= [red1, red2, blue, black1, black2, white, gray, green]:

> setattribute(black1, black): setattribute(black2, black):

> setattribute(red1, red): setattribute(red2, red):

> place:= [\$1..8]:

> Row1:= {1,2,3}: Row3:= {6,7,8}: Lane1:= {1,4,6}: Lane2:= {2,7}: Lane3:= {3,5,8}:

> Rows:= [Row1, Row3]: Lanes:= [Lane||(1..3)]:

We won't need Row2.

> Cars:= LogicProblem(V):

> with(Cars):

```Warning, these names have been rebound: &!!, &-, &<, &>, &?, &G, &Soln, CPV, ConstNum, Consts, ConstsInV, DifferentBlock, FreeGuess, GoBack, Guess, InternalRep, IsComplete, IsUnique, NC, NV, PrintConst, Reinitialize, SameBlock, Satisfy, Separated, UniquenessProof, VarNum, VarNumC
```

We need this "Proc" type constraint for clue 1.

> SameColor:= proc(M, positions)
local pos1, pos2;
use `&Soln`= M:-`&Soln`, VarNum= M:-VarNum, ConstNum= M:-ConstNum, Consts= M:-Consts in
pos1:= ConstNum(positions[1]) &Soln VarNum(color);
pos2:= ConstNum(positions[2]) &Soln VarNum(color);
if pos1=0 and pos2=0 then
false, false
elif pos1<>0 and pos2<>0 then
if attributes(Consts[pos1]) = attributes(Consts[pos2]) then false,true else true fi
elif pos1<>0 then
if pos1 = ConstNum(black1) then false, false, [positions[2] = black2]
elif pos1 = ConstNum(black2) then false, false, [positions[2] = black1]
elif pos1 = ConstNum(red1) then false, false, [positions[2] = red2]
elif pos1 = ConstNum(red2) then false, false, [positions[2] = red1]
else true
fi
else #pos2<>0
if pos2 = ConstNum(black1) then false, false, [positions[1] = black2]
elif pos2 = ConstNum(black2) then false, false, [positions[1] = black1]
elif pos2 = ConstNum(red1) then false, false, [positions[1] = red2]
elif pos2 = ConstNum(red2) then false, false, [positions[1] = red1]
else true
fi
fi
end use
end:

> Constraints:=
[#Classify by sex:
Distinct([{Kamuter, Stucke, Toots, Trapt}, Men])
,Distinct([{Horne, Poeler, Blough, Cruize}, Women])

#Clue 1:
,Distinct([{2, 4, 5, 7}, {green, gray, white, blue}])
,Proc(SameColor, [2,4]), Proc(SameColor, [5,7])

#Clue 2:
,Kamuter<>Elaine
#Here I introduce the partition/membership constraint types SameBlock and DifferentBlock.
,Rel(SameBlock, Kamuter, Blough, place, Lanes)
,Rel(DifferentBlock, Kamuter, Elaine, place, Lanes)
,Rel(DifferentBlock, Blough, Elaine, place, Lanes)

#Clue 3
,Distinct([Stucke, {4} union Lane3])
,Distinct([blue, {5} union Lane1])
#We can use a "Succ" constraint to specify that the blue car is just to the right of Stucke.
#But note that this only works because of the limitations already placed on their positions by the two Distinct constraints.
,Succ(blue, Stucke, place)

#Clue 4
,Otto<>gray
,Distinct([Otto, Lane1 union Lane3])
,Distinct([Toots, gray, 2,7,4,5])
,Distinct([gray, Men])
,Rel(SameBlock, [Otto, Toots, gray], place, Rows)

#Clue 5
,Emma=red1, Stucke=red2

#Clue 6
,Carl<>Blough, Carl<>green
,Rel(SameBlock, Carl, green, place, Lanes)
,Distinct([Carl, Row1])
,Distinct([green, Row3])

#Clue 7
,Distinct([Trapt,Dee,red1,red2])

#Clue 8
,Rudy=black1, Cruize=black2

#Clue 9
,Horne<>white

#The next constraint illustrates how the Dummy constraint type can be used to print out whatever infomation the user wants.
#It will be called before each pass through the Unsatisfied list.
,Dummy(proc(M) use `&?`= M:-`&?` in print(&? ShowStats) end; false, false end, [])
];

> infolevel['Constraints']:= 0: infolevel['TC']:= 0: infolevel['TCdisplay']:= 0: CollectStats:= true:

> Reinitialize():

> st:= time():

> Satisfy(Constraints);

> time()-st;

In this exmaple, we have seen how the program can handle multi-dimensional relationships. Please proceed to the worksheet ColorASquare.mws for a significantly more complex and more abstract two-dimensional problem.

>