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 NonClausal 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 stateoftheart 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 SATbased planning, is to represent a problem in some logicbased 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, logicbased, 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 builtin way to express recursion provides considerable modeling convenience. The builtin 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 wellstudied, 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 adhoc. Objectives The expectation is that the techniques developed in each area can be profitably used in the other. Topics of interest include:
