23 Jun 2011
Ann Arbor MI, U.S.A.
--- Call for Abstracts ---
SAT for Practical Applications (SPA'2011)
Workshop affiliated with SAT 2011 - 14th Intl. Conf. on Theory and
Applications of Satisfiability Testing
Ann Arbor, USA, June 23, 2011
http://baldur.ira.uka.de/~olga/Site/SPA2011
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.
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 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.
Topics of interest include but are not restricted to
----------------------------------------------------
* Applications in verification: hardware, software, hybrid systems, expert
systems, planning, scheduling, configuration (e.g., software package
management, cars, ...), artificial intelligence, computational biology,
cryptanalysis
* Combination of SAT with techniques like BDDs, linear programming, SMT
solving
* Encoding real-world problems in extensions of SAT like MAX-SAT, QBF, etc.
* Optimizing general SAT algorithms for particular applications
Invited Speakers:
-----------------
TBA
Submission
----------
Please, submit a one to two page abstract (preferably in LNCS format; it will
be handed out at the workshop) describing what you would like to present. We
will have talks of approx. 20-30 minutes and time for discussion. Submission
of abstracts is via EasyChair:
http://www.easychair.org/conferences/?conf=spa2011.
Important Dates
---------------
* Abstract submission deadline: April 22, 2011
* Notification of acceptance: April 29, 2011
* Early registration deadline: May 1, 2011
* Workshop: June 23, 2011
Organizers
----------
* Carsten Sinz, Karlsruhe Institute of Technology, carsten.sinz@kit.edu
* Olga Tveretina, Karlsruhe Institute of Technology, olga@ira.uka.de