In many real-life problems, we search for objects of complex nature &mdash plans, schedules, assignments. Such objects are often represented as (finite) structures, which are implicitly specified by means of theories in some logic. Thus, languages are needed to describe structures, and algorithms to extract them from these implicit descriptions. Propositional Satisfiability (SAT), Constraint Programming (CP), and Answer Set Programming (ASP) are arguably the three most prominent areas that develop such languages and techniques.

Each of these areas has been proposed as a declarative programming approach to solving NP-complete combinatorial problems. Such problems abound in computer science, engineering, operations research computational biology and other fields. In many cases, progress is limited by the difficulty of designing implicit representations of structures (modeling), which hinders common acceptance of the aproach, and the inability to solve sufficiently large instances of the problems in practical time bounds (search algorithms). Therefore, these three areas have as a major goal the development of practical modeling languages and methodologies that support the modeling, and algorithms and tools for efficient problem solving.

SAT

The effectiveness of the above approach to problem solving has perhaps been demonstrated most clearly by SAT. SAT's focus is on efficiency; a great deal of work has gone into engineering very good solvers. SAT solver implementations have become a standard and widely used tool in the Electronic Design Automation industry, for hardware verification and other related tasks. SAT's modeling language is propositional logic, the simplest, oldest, best understood and most standard of all logics. However, as a modeling language it imposes severe limitations; SAT's methodology focusses more on efficient encoding than on specification and knowledge representation. SAT problems are almost always generated from a range of -often dedicated- languages. Whereas ASP and CP aim to support the problem solving process from input (the high level specification) till output, SAT only covers half of this process, and starts with a reduction of the high level specification to a SAT problem.

Constraint Programming

Of the three areas, Constraint Programming has found the broadest application in industry. CP solvers have been successfully used in building solutions to many industrial scheduling and logistical problems. In CP research, a lot of effort has gone into constraint propagation techniques for particular constraints, and into identifying tractable constraint languages or instance families. The domain has its roots in extending logic programming with constraints (CLP). While such early systems computed assignments to constrained variables, many of the current systems compute more complex structures (assignments, functions) that satisfy constraints. In many cases, what these systems do is compute structures from declarative specifications; some systems can handle computation of satisfiability or models for certain subsets of logic in the context of finite domains.

ASP

ASP is the descendant of logic programming, in which problem solving is not done by computation of assignments to variables but by computing (stable) models (or answer sets). Contrary to the other areas, ASP has taken modeling seriously from the outset. ASP is a predicate logic (as opposed to propositional); it has been extended with aggregates, weight constraints and defined predicates, possibly with recursion. The latter appears particularly useful when encoding problems involving sequences of events, such as hardware and software verification and planning. Its methodology is based on studies in knowledge representation and non-monotone reasoning. Recently, the area made considerable progress on the solvers and is developing industrial applications.

Other

Beside SAT, CP and ASP, there are other areas that explore the computation of structures as a problem solving paradigm. Finite model generators for FO have been developed and used for theorem proving (see here ). Model expansion for FO and its extension with inductive definitions and/or aggregates has been presented as a classical logic variant of the ASP paradigm.

Another related paradigm is that of Abductive Logic Programming. The form of abductive inference implemented in this area is very similar to model generation. Abductive systems have been implemented for extensions of logic programming with FO axioms as "constraints", with numerical or finite domain constraints, with aggregates, etc. These systems are implemented as logic programming inference systems interfaced with constraint solvers, and as such, they present interesting examples for integrating techniques from LP and CP.

From the above areas, the computation of structures from specifications emerges as a common theme and is developing into a new declarative problem solving paradigm. This research sheds new light on the role of logic and inference for problem solving and AI. The combined experience within the above areas is breaking an old dogma in certain areas of AI and computational logic, namely that expressive languages such as first order logic (FO) are useless for problem solving because of their undecidability of deduction. Finite model generation or expansion is a simpler form of inference, with widespread applications, in which much richer specification languages are practically useful and even necessary.

There are a number of important interactions between the above areas. For example, SAT solvers are used as the engines in some CSP and ASP solvers, and some similar implementation techniques are used in all three areas. However, in many respects the areas proceed as three largely independent disciplines, each one providing its own unique contribution, and with the bulk of attention on rather different particular problems or questions. There are few, if any, researchers who are real experts in all three areas. To date, we are not aware of any significant meeting which specifically addresses these three areas.

Objectives of the Workshop

LaSh08 aims to offer a discussion forum for research in SAT, ASP and CP that focuses on the computation of structures from declarative descriptions. We invite contributions on modeling languages, methodologies, theoretical analysis, techniques, algorithms and systems. The forum is an occasion to exchange ideas on the state-of-the-art; to discuss specific technical problems; to formulate challenges and opportunities ahead; to analyse differences and simularities between the different areas; to study opportunities for synergy and integration.

The workshop's objective is to create an informal, stimulating atmosphere for exchange of ideas. We invite also reports of work in progress. There will be informal proceedings.