______________________________________________________________________

Date:  Wednesday 23 May 2001
Time:  13:00 to 14:00  (we will start on the hour!)
Venue: Room A114, Ekonomikum, Kyrkogårdsgatan 10, Uppsala

	   Permutation Problems and Channelling Constraints

			      Toby Walsh
		    Department of Computer Science
			  University of York
			    United Kingdom
			   tw@cs.york.ac.uk
		    http://www.cs.york.ac.uk/~tw/

Many  assignment,  scheduling  and routing  problems  are  permutation
problems.  For example, sports tournament scheduling can be modeled as
finding a permutation  of the games to fit into the  available  slots,
whilst the traveling  salesperson  problem can be modeled as finding a
permutation of the cities which gives a tour of minimal length.  There
are a number of different ways of modelling  permutation problems (for
example, do we assign  teams to time slots, or do we assign time slots
to  teams?).  I  describe  a  methodology,  as well  as a  measure  of
constraint  tightness,  that can be used to  compare  these  different
models.  My  results  will  help  users  of  constraints  satisfaction
toolkits  to choose a model  for a  permutation  problem,  and a local
consistency.
______________________________________________________________________

Date:  Wednesday 23 May 2001
Time:  14:30 to 15:30
Venue: Room A114, Ekonomikum, Kyrkogårdsgatan 10, Uppsala

   Extensions to Proof Planning for Generating Implied Constraints

			      Ian Miguel
		    Department of Computer Science
			  University of York
			    United Kingdom
			  ianm@cs.york.ac.uk
		   http://www.cs.york.ac.uk/~ianm/

Implied  constraints are those that logically  follow from the initial
model of a constraint  satisfaction  problem.  The addition of implied
constraints can greatly improve efficiency and is an important step in
solving  difficult  problems.  Unfortunately,  the addition of implied
constraints  is  currently  done by hand in an ad-hoc  manner.  We are
developing  a  system  based  on  proof   planning   which   generates
automatically  those  implied  constraints  which  will help to reduce
search.

Proof planning is a technique  used for guiding the search for a proof
in  automated   theorem   proving.  Common   patterns  in  proofs  are
identified and  encapsulated  in methods which are made available to a
planner.  This talk describes how proof planning is being  extended to
generate  implied  algebraic   constraints.  This  inference   problem
introduces  a  number  of   challenging   problems  like   deciding  a
termination  condition  and  evaluating  constraint  utility.  We have
implemented  a  number  of  methods  for  reasoning  about   algebraic
constraints.   For   example,   the   "eliminate"    method   performs
Gaussian-like   elimination  of  variables  and  terms.  We  are  also
re-using  proof methods from the PRESS  equation  solving  system like
(variable) isolation.
______________________________________________________________________

Date:  Tuesday 29 May 2001
Time:  14:15 to 15:15
Venue: Room A114, Ekonomikum, Kyrkogårdsgatan 10, Uppsala

	     Solving Non-Boolean Satisfiability Problems

			    Alan M. Frisch
		    Artificial Intelligence Group
		    Department of Computer Science
			  University of York
			    United Kingdom
			 frisch@cs.york.ac.uk
		  http://www.cs.york.ac.uk/~frisch/

State-of-the-art  procedures for  determining  the  satisfiability  of
formulas of Boolean  logic have  developed to the point where they can
solve  problem  instances  that are large  enough  to be of  practical
importance.  Many of the problems on which  satisfiability  procedures
have been effective are  non-Boolean  in that they are most  naturally
formulated in terms of variables  with domain sizes  greater than two.
Boolean   satisfiability   procedures   have  been  applied  to  these
non-Boolean   problems  by  reformulating  the  problem  with  Boolean
variables.  An  alternative,  previously  unexplored  approach,  is to
generalise  satisfiability  procedures to handle non-Boolean  formulas
directly.  This  talk  compares  these  two  approaches.  We  begin by
presenting  two  procedures   that  we  have   developed  for  solving
non-Boolean  formulas  directly.  We also  present  three  methods for
systematically  transforming non-Boolean formulas to Boolean formulas.
Finally,  experimental results are reported on using all these methods
to solve  random  formulas,  graph  colouring  problems  and  planning
problems.
______________________________________________________________________

For directions, make a detailed search on "Kyrkogårdsgatan 10" at
http://www.gulasidorna.se/, where the `Ekonomikum' is still known
as the `Humanist Centrum'.