Search and Logic: Answer Set Programming and SAT

A Workshop affiliated with ICLP, as part of FLoC 2006.

August 16, 2006, Seattle, Washington, USA
Program

Accepted Papers

Invited Talks
Henry Kautz, University of Washington
    Deconstructing Planning as Satisfiability.
Mirek Truszczynski, University of Kentucky
    Knowledge representation languages ---
    a programmer's interface to satisfiability.


Tutorials
John Franco, University of Cincinnati
    Experiences in the Research and Development
    of a Non-Clausal SAT Solver.
Ilka Niemela, Helsinki University of Technology
    Answer Set Programming: Foundations,
    Implementation Techniques, and Applications.

Call For Papers: text.

Important dates
Paper Submission: May 22, 2006
Author Notification: June 27, 2006
Workshop : August 16, 2006

Paper Submission (closed)
Submit PDF or Postscript papers of at most
15 pages, in LNCS format to Easychair

Program Committee
Marco Cadoli,   University of Rome
Thomas Eiter,   Vienna University of Technology
Enrico Giunchiglia,  University of Genova
Nicola Leone,   University of Calabria
Fangzen Lin,   HK University of Science and Technology
Victor Marek,  University of Kentucky
David Mitchell,   Simon Fraser University
Ilka Niemela,   Helsinki University of Technology
John Schlipf,   University of Cincinnati
Eugenia Ternovska,  Simon Fraser University
Toby Walsh,   University of New South Wales

Organizing Committee
Enrico Giunchiglia,  University of Genova
Victor Marek,  University of Kentucky
David Mitchell,   Simon Fraser University
Eugenia Ternovska,  Simon Fraser University
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.

Overview
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.

SAT
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
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.

Objectives
The expectation is that the techniques developed in each area can be profitably used in the other. Topics of interest include:
  • fundamental algorithms,
  • solver implementation techniques,
  • comparison of modeling strategies,
  • criteria for future modeling language choices,
  • generalizing work on tractable cases,
  • methods for taking advantage of tractability results, and
  • new algorithm directions