Re: incomplete constraint propagation

Raphael Finkel wrote:
> 
>         The problem is that my program is completely constrained, but Eclipse
>         fails to follow through all the constraints.

It is one of the characteristics of constraint programming that
problems are solved by a combination of (smart) constraint
propagation and (stupid) search.

Some properties of the solution can be inferred by constraint
propagation, the rest must be found by (combinatorial) search.
Since search is always available as a fall-back method, the
programmer (or the system) is free to vary the amount of
constraint propagation done.  Doing more propagation results
in less search, but doing too much propagation might be so
costly that it doesn't outweigh the savings in search time.

Most constraint solvers are in fact incomplete. In order to
be efficient, they usually implement some form of local
consistency (e.g. arc-consistency), not global consistency
of the whole constraint network.

Usually this incompleteness does not matter: in real problems
it only increases the amount of search somewhat. In the case
of puzzles (which are probably carefully constructed to be
solvable without search) the shortcoming is of course more
obvious!
 

There are two ways to solve your puzzle all the way:
1. add search (which is anyway needed in most cases)
2. use stronger propagation

Adding search is done by inserting the line

	labeling(Costume),

after the constraint setup and before printing results.
If you follow the execution, you will see that two
backtracks are needed before the solution is found.


If you want to experiment with stronger propagation, a
particularly elegant way is to use Eclipse's Generalized
Propagation library(propia), see Library Manual. This
allows you to compute all inferences from an arbitrary
combination of constraints. To solve your problem, I
collected all the constraints that you mentioned in the
explanation at the bottom of your mail, and subjected
them to the generalized propagation mechanism, writing

	(
	    alldifferent(Costume),
	    ( Scarecrow #= Place1 , Lion #= Place2
	    ; Scarecrow #= Place2 , Lion #= Place3
	    ; Scarecrow #= Place3 , Lion #= Place4
	    )
	) infers most,

This now makes all the inferences that can be made by
looking at that particular group of constraints together,
and as a result you get the solution even without search.


>  Here is my program, based on
>         a logic puzzle from Dell Logic Puzzles, October 1999, page 8, called
>         "Boo!".  I first represent the logic puzzle in my own "Constraint Lingo",
>         from which I then generate Eclipse clauses, retaining Constraint Lingo as
>         comments for documentation purposes.  I have a paper on Constraint Lingo
>         if you are interested; I also can generate smodels clauses, and smodels
>         succeeds in finding the unique solution.
> 
>         --- program starts here
> 
>         :- use_module(library(fd)) .
> 
>         try :-
> 
>         % CLASS place: 1 .. 4
>                 Place = [Place1, Place2, Place3, Place4],
>                 Place :: 1..4,
>                 alldifferent(Place),
>         % CLASS child: bernadette juan keisha sam
>                 Child = [Bernadette, Juan, Keisha, Sam],
>                 Child :: 1..4,
>                 alldifferent(Child),
>         % Break symmetry
>                 Bernadette = 1,
>                 Juan = 2,
>                 Keisha = 3,
>                 Sam = 4,
>         % CLASS costume: crayon lion robot scarecrow
>                 Costume = [Crayon, Lion, Robot, Scarecrow],
>                 Costume :: 1..4,
>                 alldifferent(Costume),
>         %       CONFLICT sam robot
>                 Robot #\= Sam,
>         %       REQUIRED sam 4
>                 Sam #= Place4,
>         %       OFFSET 1 place: scarecrow lion
>                 ( ( Scarecrow #= Place1 #/\ Lion #= Place2 ) #\/
>                 (Scarecrow #= Place2 #/\ Lion #= Place3) #\/
>                 (Scarecrow #= Place3 #/\ Lion #= Place4) ),
>         %       CONFLICT bernadette 2
>                 Bernadette #\= Place2,
>         %       OFFSET 2 place: crayon keisha
>                 ((Crayon #= Place1 #/\ Keisha #= Place3) #\/
>                 (Crayon #= Place2 #/\ Keisha #= Place4)),
>         % print result
>                 write(stdout, '\nPlace1 = '), write(stdout, Place1) ,
>                 write(stdout, '\nPlace2 = '), write(stdout, Place2) ,
>                 write(stdout, '\nPlace3 = '), write(stdout, Place3) ,
>                 write(stdout, '\nPlace4 = '), write(stdout, Place4) ,
>                 write(stdout, '\nBernadette = '), write(stdout, Bernadette) ,
>                 write(stdout, '\nJuan = '), write(stdout, Juan) ,
>                 write(stdout, '\nKeisha = '), write(stdout, Keisha) ,
>                 write(stdout, '\nSam = '), write(stdout, Sam) ,
>                 write(stdout, '\nCrayon = '), write(stdout, Crayon) ,
>                 write(stdout, '\nLion = '), write(stdout, Lion) ,
>                 write(stdout, '\nRobot = '), write(stdout, Robot) ,
>                 write(stdout, '\nScarecrow = '), write(stdout, Scarecrow) .
> 
>         --- program ends here
> 
>         once try/1 is compiled, I run it by the query "try ." .
> 
>         Output:
>                 Place1 = 1
>                 Place2 = 2
>                 Place3 = 3
>                 Place4 = 4
>                 Bernadette = 1
>                 Juan = 2
>                 Keisha = 3
>                 Sam = 4
>                 Crayon = 1
>                 Lion = _622{[2..4]}
>                 Robot = _635{[2, 3]}
>                 Scarecrow = _648{[2, 4]}
> 
>         This output is correct so far as it goes, but it should go farther.  For
>         example, Scarecrow cannot be 4, because the clause for
>         "OFFSET 1 place: scarecrow lion" explicitly restricts it to 1, 2, or 3.
>         Even if I explicitly add a term "Scarecrow #\= 4", Eclipse propagates
>         constraints no further.  But of the three disjuncts in
> 
>                 ( ( Scarecrow #= Place1 #/\ Lion #= Place2 ) #\/
>                 (Scarecrow #= Place2 #/\ Lion #= Place3) #\/
>                 (Scarecrow #= Place3 #/\ Lion #= Place4) ),
> 
>         the first is disallowed because Place1=1 and Scarecrow={[2,4]}, and
>         the second is disallowed because it would prevent Robot from getting a
>         valid value.  After all, Robot is distinct from Scarecrow (putatively
>         Place2=2), Lion (putatively Place3=3), and Crayon (known to be Place1=1),
>         but Robot is known to be in {[2,3]}.  Therefore, only the third disjunct
>         holds, so Scarecrow=Place3=3, Lion=Place4=4, forcing Robot=Place2=2, fully
>         constraining all the variables.
> 
>         If it is any consolation, Gnu Prolog also fails in exactly the same way.
> 
> Raphael Finkel


Since this discussion is of general interest, would you
mind if I copy this to the eclipse-users mailing list?

All the best,
-- 
 Joachim Schimpf              /             phone: +44 20 7594 8187
 IC-Parc, Imperial College   /            mailto:J.Schimpf@ic.ac.uk
 London SW7 2AZ, UK         /    http://www.icparc.ic.ac.uk/eclipse