AI Europe 2016

  Partnership between AISB and AI Europe 2016: Next December 5th and 6th in London, AI Europe will bring together the European AI eco-system by gathering new tools and future technologies appearing in professional fields for th...


Read More...

AISB convention 2017

  In the run up to AISB2017 convention (http://aisb2017.cs.bath.ac.uk/index.html), I've asked Joanna Bryson, from the organising team, to answer few questions about the convention and what comes with it. Mohammad Majid...


Read More...

Harold Cohen

Harold Cohen, tireless computer art pioneer dies at 87   Harold Cohen at the Tate (1983) Aaron image in background   Harold Cohen died at 87 in his studio on 27th April 2016 in Encintias California, USA.The first time I hear...


Read More...

Dancing with Pixies?...

At TEDx Tottenham, London Mark Bishop (the former chair of the Society) demonstrates that if the ongoing EU flagship science project - the 1.6 billion dollar "Human Brain Project” - ultimately succeeds in understanding all as...


Read More...

Computerised Minds. ...

A video sponsored by the society discusses Searle's Chinese Room Argument (CRA) and the heated debates surrounding it. In this video, which is accessible to the general public and those with interest in AI, Olly's Philosophy Tube ...


Read More...

Connection Science

All individual members of The Society for the Study of Artificial Intelligence and Simulation of Behaviour have a personal subscription to the Taylor Francis journal Connection Science as part of their membership. How to Acce...


Read More...
012345

Notice

AISB event Bulletin Item

CALL FOR ABSTRACTS: "SAT for Practical Applications", 23 Jun 2011, USA

http://baldur.ira.uka.de/~olga/Site/SPA2011

(SPA'2011)- Workshop affiliated with SAT 2011 - 14th Intl. Conf. on Theory and Applications of Satisfiability Testing -Ann Arbor MI, USA


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