CP was co-located with ICAPS, KR, and NMR; see below.
Alain Colmerauer, France
Back to the Complexity of Universal Programs
The talk discusses a framework enabling one to define and determine the
complexity of various universal programs U for various machines.
The approach consists of first defining the complexity as the average
number of instructions to be executed by U, when simulating the
execution of one instruction of a program P with input x.
To obtain a complexity that does not depend on P or x, we
introduce the concept of an introspection coefficient expressing the
average number of instructions executed by U, for simulating the
execution of one of its own instructions. We show how to obtain this
coefficient by computing a square matrix whose elements are numbers of
executed instructions when running selected parts of U on selected
data. The coefficient then becomes the greatest eigenvalue of the matrix.
We illustrate the approach using two examples of particularly efficient
universal programs: one for a three-symbol Turing Machine (blank symbol
not included) with an introspection coefficient of 3672.98, the other for
an indirect addressing arithmetic machine with an introspection
coefficient of 26.27.
University of California, USA
(jointly with KR)
Satisfiability, Knowledge Compilation and the Journey Towards Universal Reasoning Engines
The development of universal reasoning engines has been a main objective
of AI since its very early days. The vision here is to relief system
developers from having to worry about reasoning algorithms, focusing only
on capturing the necessary knowledge, while delegating algorithmic
considerations to these engines. Few decades after this original vision
was first conceived, the field of AI is starting to bear its fruits,
initially through SAT solvers, and more recently through knowledge
compilers (and related model counters).
In this talk, I will discuss some of the progress in realizing this
vision, highlighting both successes and missed opportunities. For
example, on the satisfiability front, I will present a semantics for
modern SAT solvers, which is somewhat distant from how these solvers are
commonly understood. I will argue that the lack of this and similar
semantics could be the reason behind the lack of recent leaps in SAT
solving, which have been saught after since the zchaff solver was
introduced many years ago. On the knowledge compilation front, I will
review some of the key advancements, especially in relation to SAT
solving and model counting, and point to some of the major gaps between
what the theory says is possible and what current practice allows. I will
argue that bridging this gap requires some novelties, especially in how
systematic search is currently practiced. I will also discuss some recent
breakthroughs that seem to have brought us closer to bridging this gap.
John Hooker, Carnegie Mellon University, USA
(jointly with ICAPS)
How to Relax
Relaxation is a theme that occurs in many problem solving methods. It
is often associated with optimization, but relaxation plays an equally
important role in finite-domain constraint programming and other discrete
methods. This talk surveys a wide variety of relaxation methods,
including linear relaxation and cutting planes, Lagrangean relaxation,
the domain store and related relaxations, state space relaxation,
relaxations in decomposition methods, as well as nonserial dynamic
programming, mini buckets, and other relaxations based on simplifying the
primal graph. Recognizing the role of relaxation can suggest
improvements based on strengthening the relaxation. Consistency
maintenance, for example, in effect strengthens relaxations. Other
approaches include the use of such knowledge compilation devices as
and/or trees and multivalued decision diagrams, and the solution of a
relaxation dual problem.
Current issues on Max-SAT
Propositional satifiability (SAT) is a research field strongly related to
CP. SAT solvers have improved dramatically in the last years and are
currently used to solve problems in many industrial applications. The
main reasons for this success are the use of an extremely simple language
(CNF) for which solvers can be highly optimized.
The success story of SAT solvers has led to the study of several
extensions of propositional logic, and Max-SAT is arguably the most
prominent one. In short, Max-SAT is the natural extension of SAT to
model and solve optimization problems (in contrast to decision problems).
It has attracted a lot of interest and, only from the work done in the
last 5 years, current solvers outperform previous ones by several orders
of magnitude. The purpose of the tutorial is to overview this recent
research with special emphasis in the algorithmic aspects and its
potential applications. The tutorial will cover with unified notation the
essential ideas behind modern solvers.
ILOG CP Optimizer:
An Automatic Search and Modeling Framework for Detailed Scheduling
In this software tutorial we present a modeling framework and automatic
search for detailed scheduling problems. We describe a new modeling
framework based on a compact set of algebraic concepts that can be used
to model a wide variety of hard and soft scheduling problems, while
taking advantage of work breakdown structures. Together with a tunable
search engine, models can be simply run and solved with default settings
or with adjusted engine parameters and declarative search phases, to
rapidly produce quality schedules.
See the CP DP page
for detailed information.
Constraint Satisfaction Techniques for Planning and Scheduling Problems
(COPLAS'08) (jointly with ICAPS)
Counting Problems in CSP and SAT, and Other Neighbouring Problems
Local Search Techniques in Constraint Satisfaction (LSCS'08)
Constraint Modelling and Reformulation (ModRef'08)
Preferences and Soft Constraints (SofT'08)
Symmetry and Constraint Satisfaction Problems (SymCon'08)
Quantification in Constraint Programming (QiCP'08)
CP-WS9: CSP Solver Competition
Search in ManyCore)
Delegates attending the CP conference were able to attend the sessions of
which ran alongside it. The single registration fee granted attendance
to research paper presentations, tutorials and workshops of these co-located events.
Some sessions were shared.
Not co-located but taking place temporally and geographically close were the following
International Joint Conference on Automated Reasoning (IJCAR)
took place in Sydney during 10–15 August, and the
International Workshop on Principles of Diagnosis (DX)
took place near Sydney in the week following CP.
The joint Conference Dinner took
place on board MV Sydney 2000 on Wednesday night.
(Please see the program
or local information for details.)