The workshop will bring together researchers from SAT and ASP areas to exchange ideas on the current state-of-the-art in techniques, results and methodologies; to discuss problems which are exhibited in both areas; to formulate challenges and opportunities ahead.
In many applications of Computer Science, especially in combinatorial optimization, hardware design and software correctness checking, complex problems are pervasive. Those problems may be represented in a variety of ways. One technique, which has been used increasingly since the pioneering work of Kautz and Selman on SAT-based planning, is to represent a problem in some logic-based formalism (for instance propositional logic, quantified boolean formulas, or logic programming with the stable semantics) in such a way that intended models correspond to solutions. Subsequently the user applies a solver (dedicated piece of software) to the representation of the problem, computes model(s) and reads off the solutions.
Analogous techniques are used based on a variety of formalisms, such as constraint satisfaction and integer programming, but SAT and ASP are distinguished by being based on logic. While the SAT and ASP research communities apply a similar, logic-based, approach to problem solving, the roots of the two communities are different, and they stress different aspects of the approach. For example, in SAT the emphasis is more toward efficient computation; in ASP more emphasis is placed on knowledge representation. Moreover, there are few researchers who are real experts in both areas.
The effectiveness of the declarative approach has perhaps been demonstrated most clearly by SAT. SAT stems from classical investigations by logicians of propositional satisfiability and has over 90 years of history with contributions of researchers such as Wittgenstein, Tarski, Quine, Davis, Putnam and other great mathematicians, computer scientists, and philosophers. SAT Solver design is facilitated by the fact that the propositional formulas used have very simple syntax and semantics. A great deal of work has gone into engineering very good solvers, and these have now become a standard and widely used tool in the Electronic Design Automation industry, for hardware verification and other related tasks. However, SAT has severe limitations as a modeling language.
ASP is a younger field, with approximately 15 years of history, but shows considerable promise on some problems which are poorly handled by SAT. ASP stems of Logic Programming, but changes the paradigm by computing models rather than unifying substitutions. Due to its Logic Programming roots, ASP input languages invariably include schemata, which together with a built-in way to express recursion provides considerable modeling convenience. The built-in recursion mechanism appears particularly useful when encoding problems involving sequences of events, such as hardware and software verification and planning. In contrast to other approaches ASP is the only area of that appears to have taken modeling methodology seriously from the outset.
SAT and ASP
There are a number of important interactions between these areas. For example, some similar implementation techniques are used in both areas, and SAT solvers are even used as the engines in some ASP solvers. However, in many respects the areas proceed as largely independent disciplines, each one providing its own unique contribution, and with the bulk of attention on rather different particular problems or questions.
Modeling practice plays an important role in both areas, but in rather idiomatic forms. In SAT tractable restrictions are well-studied, but this subject has not yet been developed in ASP. Input/modeling languages which include schemata (a fragment of predicate logic) are standard in ASP, but work of this sort in SAT has been mostly ad-hoc.
The expectation is that the techniques developed in each area can be profitably used in the other. Topics of interest include: