SPA 2011: SAT for Practical Applications

Workshop affiliated with SAT 2011

June 23, 2011, Ann Arbor

Workshop

» Home
» Topics
» Organizers/Contact
» Important dates
» Attendance/Submission
» Keynote speakers
» Workshop agenda

Welcome

The satisfiability problem (SAT) is a classical problem in computer science. It is NP-complete and requires time exponential in the size of a problem in the worst-case. Nevertheless, modern SAT solvers are capable to solve large real world instances. Applications of SAT range from artificial intelligence to hardware design and verification. In particular, SAT solvers have been used for software verification, configuration, planning, or scheduling.

Using SAT for practical applications has been driven by remarkable improvements in SAT solver implementations on the one hand, and on the other hand by new approaches to encode real world problems. For example, bounded model checking, which uses a SAT solver as its core engine, is applied frequently by many industries.

The combination of SAT with additional theories such as linear arithmetic, bit-vectors, or uninterpreted functions allows greater flexibility in modeling than plain SAT. Moreover, extensions of SAT like (Weighted/Partial) MAX-SAT, QBF, Pseudo-Boolean Optimization brought new applications into the focus of the SAT community.

Another workshop of interest takes place before the SAT conference: Pragmatics of SAT (PoS'11). While SPA'11 is mainly designed for people interested in applications of SAT, PoS'11 focuses more on people interested in designing and implementing SAT technology.

The aim of this workshop is

  • to give an overview of application areas where SAT solvers are already employed successfully or could be in the future
  • to identify algorithmic problems specific to real-world SAT applications (problem encoding, explanation, etc.)
  • to collect ideas to foster the use of SAT solvers in new application areas (e.g.: a high-level format for combinatorial problems)
We also want to bridge the gap between developers of SAT solver technology and people interested in applying this technology, and therefore especially welcome contributions from industry. The format of the workshop differs from typical workshops that are often thought of as "small conferences". Instead, we want to put an emphasis on discussion and short presentations of new ideas. We therefore especially welcome contributions that:
  • summarize the use of SAT solving techniques in a specific application area
  • describe a particular real-world application of SAT
  • formulate open problems in SAT applications