______________________________________________________________________
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'.