SAT Live!

keep up to date with research on the satisfiability problem

Our scientific association

The SAT association

Upcoming deadlines

SAT related books

SAT Live! is currently being redesigned. Features are added incrementally to the site. Do not hesitate to come back later to see how it evolves.

What is the Satisfiability problem?

If you are a newcomer to the SATisfiability problem, you might want to take a look at wikipedia's page on the boolean satisfiability problem first. You might also find those surveys of interest. For a deeper insight of the current interest on SAT solvers for software and hardware verification, Armin Biere's course on formal systems is a good start. Eugene Goldberg has also a nice and somehow non standard way of introducing modern SAT solvers in his three part course on SAT. Finally, Joao Marques-Silva wrote a nice article on practical applications of boolean satisfiability.

The SAT association also makes available some chapters from the Handbook of satisfiability to allow newcomers to understand key principles in satisfiability, namely History of Satisfiability, the Conflict Driven Clause Learning architecture in SAT solvers and the principles behind Bounded Model Checking. More material is available on the association's tutorials web page.

Looking for a SAT solver to play with?

The following open source SAT solvers might be a good start: Minisat (C++), Picosat (C), SAT4J (Java). If you are looking for a stochastic local search framework for SAT, you should take a look at UBCSAT.
----------------------------------------------------------------------

                         CALL FOR PAPERS

              Eighteenth International Conference on
        THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
                         --- SAT 2015 ---

                Austin, Texas, September 24-27, 2015
               http://www.cs.utexas.edu/~marijn/sat15/

         Abstract submission deadline: April 22, 2015
            Paper submission deadline: April 29, 2015

-----------------------------------------------------------------------

The International Conference on Theory and Applications of
Satisfiability Testing (SAT) is the premier annual meeting for
researchers focusing on the theory and applications of the
propositional satisfiability problem, broadly construed. In addition
to plain propositional satisfiability, it also includes Boolean
optimization (such as MaxSAT and Pseudo-Boolean (PB) constraints),
Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories
(SMT), and Constraint Programming (CP) for problems with clear
connections to Boolean-level reasoning.

Many hard combinatorial problems can be tackled using SAT-based
techniques including problems that arise in Formal Verification,
Artificial Intelligence, Operations Research, Computational Biology,
Cryptography, Data Mining, Machine Learning, Mathematics, et
cetera. Indeed, the theoretical and practical advances in SAT research
over the past twenty years have contributed to making SAT technology
an indispensable tool in a variety of domains.

SAT 2015 aims to further advance the field by soliciting original
theoretical and practical contributions in these areas with a clear
connection to Satisfiability. Specifically, SAT 2015 invites
scientific contributions addressing different aspects of SAT
interpreted in a broad sense, including (but not restricted to)
theoretical advances (such as exact algorithms, proof complexity, and
other complexity issues), practical search algorithms, knowledge
compilation, implementation-level details of SAT solvers and SAT-based
systems, problem encodings and reformulations, applications (including
both novel application domains and improvements to existing
approaches), as well as case studies and reports on findings based on
rigorous experimentation.

SAT 2015 takes place in Austin, Texas, and is co-locating with the
fifteenth Formal Methods in Computer-Aided Design (FMCAD) conference.
Austin, the capital of Texas, is a college town and a center of
alternative culture away from the major cities on the American coasts,
although the city is rapidly gentrifying with its rising
popularity. Austin's attitude is commonly emblazoned about town on
T-Shirts and bumper stickers that read: "Keep Austin Weird."  Austin
is considered a major high tech center due in part to UT Austin and
the many Fortune 500 companies in the area such as AMD, Apple, eBay,
Google, IBM, and Intel, among others. Austin is also marketed as the
"Live Music Capital of the World" due to the large number of live
music venues.


IMPORTANT DATES
===============

April   22, 2015: Abstract submission deadline
April   29, 2015: Paper submission deadline
June 10-12, 2015: Author response period
June    28, 2015: Author notification
July    26, 2015: Camera-ready versions of papers due

September    23, 2015: Pre-conference workshops
September 24-27, 2015: Main conference

Follow http://www.cs.utexas.edu/~marijn/sat15/ for updates.


SCOPE
=====

SAT 2015 welcomes scientific contributions addressing different
aspects of the satisfiability problem, interpreted in a broad
sense. Domains include MaxSAT and Pseudo-Boolean (PB) constraints,
Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories
(SMT), as well as Constraint Satisfaction Problems (CSP). Topics
include, but are not restricted to:

  Theoretical advances (including exact algorithms, proof complexity,
  and other complexity issues);

  Practical search algorithms;

  Knowledge compilation;

  Implementation-level details of SAT solving tools and SAT-based
  systems;

  Problem encodings and reformulations;

  Applications (including both novel applications domains and
  improvements to existing approaches);

  Case studies and reports on insightful findings based on rigorous
  experimentation.


Out of Scope
============

Papers claiming to resolve a major long-standing open theoretical
question in Mathematics or Computer Science (such as those for which a
Millennium Prize is offered, see
http://www.claymath.org/millennium-problems), are outside the scope of
the conference because there is insufficient time in the schedule to
referee such papers; instead, such papers should be submitted to an
appropriate technical journal.


Paper Categories
================

Submissions to SAT 2015 are solicited in three paper categories,
describing original contributions:

  REGULAR PAPERS (9 to 15 pages, excluding references)
    Regular papers should contain original research, with sufficient
    detail to assess the merits and relevance of the contribution. For
    papers reporting experimental results, authors are strongly
    encouraged to make their data and implementations available with
    their submission. Submissions reporting on case studies are also
    encouraged, and should describe details, weaknesses, and strengths
    in sufficient depth.

  SHORT PAPERS (up to 8 pages, excluding references)
    The same evaluation criteria apply to short papers as to regular
    papers. They will be reviewed to the same standards of quality as
    regular papers, but will naturally contain less quantity of new
    material. Short papers will have the same status as regular papers
    and be eligible for the same awards (to be announced later).

  TOOL PAPERS (up to 6 pages, excluding references)
    A tool paper should describe the implemented tool and its novel
    features. Here "tools" are interpreted in a broad sense, including
    descriptions of implemented solvers, preprocessors, etc., as well
    as systems that exploit SAT solvers or their extensions to solve
    interesting problem domains. A demonstration is expected to
    accompany a tool presentation. Papers describing tools that have
    already been presented previously are expected to contain
    significant and clear enhancements to the tool.

Submissions should not be under review elsewhere nor be submitted
elsewhere while under review for SAT 2015, and should not consist of
previously published material.

Submissions not consistent with the above guidelines may be returned
without review.

Besides the paper itself, authors may submit a supplement consisting
of one file in the format of a gzipped tarball (.tar.gz or .tgz) or a
gzipped file (.gz) or a zip archive (.zip). Authors are encouraged to
submit a supplement when it will help reviewers evaluate the
paper. Supplements will be treated with the same degree of
confidentiality as the paper itself. For example, the supplement might
contain detailed proofs, examples, software, detailed experimental
data, or other material related to the submission. Individual
reviewers may or may not consult the supplementary material; the paper
itself should be self-contained.

Regular papers and short papers may be considered for a best paper
award. If the main author is a student, both in terms of work and
writing, the paper may be considered for a best student-paper
award. Use the supplement to your submission to state (in a brief
cover letter) if the paper qualifies as a student paper.

Links to information on the Springer LNCS style are available through
the SAT 2015 website at http://www.cs.utexas.edu/~marijn/sat15/.

All papers submissions are done exclusively via EasyChair at
http://www.easychair.org/conferences/?conf=sat2015.

One author of each accepted paper is expected to present it at the
conference.


PROCEEDINGS
===========

All accepted papers are expected to be published in the proceedings of
the conference, which will be published within the Springer LNCS
series.


PROGRAM CHAIRS
==============

Marijn Heule    The University of Texas at Austin, United States
Sean Weaver     Trusted Systems Research Group, Department of Defense, United States


PROGRAM COMMITTEE
=================

To be announced


CONTACT
=======

sat2015@easychair.org
                                    
*** VCLA International Student Awards ***

The Vienna Center for Logic and Algorithms calls for the nomination of
authors of outstanding scientific works in the field of Logic and
Computer Science, for the following awards:

- Outstanding Master Thesis Award (thesis for obtaining a Masters
degree or equivalent)

- Outstanding Undergraduate Research Award (thesis or final project
for obtaining a Bachelors degree or equivalent)

In both categories, the work must make an original contribution to a
research field that can be classified as part of Logic in Computer
Science, with focus on databases and artificial intelligence,
verification, and computational logic.

The  degree must have been awarded no earlier than November 1st, 2012.
Students that obtained the degree at the Vienna University of
Technology are excluded from nomination.

The committee will select a winner for each category. The winners will
be invited to Vienna to present their project and participate in a
festive award ceremony. Additionally, the Outstanding Master Thesis
Award category is accompanied by a prize of 1,200 Eur, and the
Outstanding Undergraduate Research Award by a prize of 800 Eur. The
decisions of the committee are not appealable.

For more information, please see http://logic-cs.at/award/


IMPORTANT DATES
------------------

Nomination deadline: November 15, 2014 (AoE)
Notification of decision: Mid January 2015
Award ceremony: Spring 2015 (precise date to be announced)


TOPICS OF INTEREST
------------------

Both awards recognize the author of an original contribution to a
research field that can be classified as part of *Logic in Computer
Science*, understood broadly as the use of logic as a tool that
enables computer programs to reason about the world.

The main areas of interest are:

- Databases and artificial intelligence, including subjects like
answer-set programming and Datalog, query languages based on logical
concepts (such as SQL, current XML-based languages), optimization of
queries, novel database-theoretical methods (like schema mappings,
information integration, querying ontologies), logic programming,
description logics, knowledge representation and reasoning (belief
change, abductive reasoning, multi-context systems, inconsistency
handling, incomplete knowledge, diagnosis), and AI formalisms
(argumentation, planning, preferential reasoning, decision support
systems).


- Verification, concerned with logical methods and automated tools for
reasoning about the behavior and correctness of complex state-based
systems such as software and hardware designs as well as hybrid
systems. It ranges from model checking, program analysis and
abstraction to new interdisciplinary areas such as fault localization,
program repair, program synthesis, and the analysis of biological
systems.


- Computational logic, covering theoretical and mathematical
foundations such as proof theory (cut elimination, proof mining,
interpolants), automated deduction (resolution, refutation, theorem
proving), non-classical logics (multi-valued logics, juridical
reasoning, deontic logics, modal and temporal logics), computational
complexity (complexity analysis, parameterized complexity,
decomposition methods) and constraint satisfaction (SAT, QSAT, CSP).


NOMINATION INSTRUCTIONS
------------------

Nominations must include:

* A cover page with the name and contact details of the nominated
person, the title of the work for which the person is being nominated,
category, date on which the degree was awarded (or if not applicable,
the date on which the work was submitted), and name of the university.

* An English summary of the thesis or project of maximum 3 pages,
excluding references (A4 or letter page size, 11pt font min.). The
summary must clearly state the main contribution of the work, its
novelty, and its relevance to some of the aforementioned areas of
interest.

* CV of the nominated person, including publication list (if applicable)

* An endorsement letter from a supervisor or another endorsing person,
preferably affiliated to the university to which the work was
submitted. The letter must clearly state what was the independent and
novel contribution done by the student and why the endorser believes
the student deserves the award.

* The full thesis/project

All documents should be in English, with the exception of the thesis
or project. In case the thesis or project is in a different language,
it must be accompanied by a research report in English with a maximum
length of 12 pages
excluding references (A4 or letter page size, 11pt font min.). This
report should be sufficient for the committee to evaluate the merit
and quality of the submitted work. In case such a report is provided,
the 3-page summary is
optional.

Nominations should be submitted electronically via EasyChair:

https://easychair.org/conferences/?conf=vcla2014

All documents except the full thesis should be combined (in the order
they are listed) into a single pdf file, to be submitted as "paper" in
Easychair. The full thesis should be submitted as attachment.

The submission must be accompanied by a plain text electronic abstract
of the thesis or project of at most 400 words, and three keywords.


The nominated student must always be listed as first and corresponding
author in the Easychair form. The supervisor or endorser may
optionally be included as second author (for example, in case (s)he
does the electronic submission).


AWARD COMMITTEE
------------------
Ezio Bartocci
Simone Bova
Michael Fink
Robert Ganian
Igor Konnov
Tomer Kotek
Roman Kuznets
Magdalena Ortiz (chair)
Revantha Ramanayake
Mantas Simkus
Daniel Weller
Florian Zuleger
                                    
---------------------------------------------------------------------------

                       13th International Conference on
                Logic Programming and Non-monotonic Reasoning
                                 LPNMR 2015

                       http://lpnmr2015.mat.unical.it/

                              Lexington, KY, USA
                            September 27-30, 2015

   (Collocated with the 4th Conference on Algorithmic Decision Theory 2015)
---------------------------------------------------------------------------

AIMS AND SCOPE

 LPNMR 2015 is the thirteenth in the series of international meetings on
 logic programming and non-monotonic reasoning. LPNMR is a forum for
 exchanging ideas on declarative logic programming, non-monotonic reasoning,
 and  knowledge representation. The aim of the conference is to facilitate
 interactions between researchers and practitioners interested in the
 design and implementation of logic-based programming languages and
 database systems, and those working in knowledge representation and
 nonmonotonic reasoning. LPNMR strives to encompass theoretical and
 experimental studies that have led or will lead to the construction of
 systems for declarative programming and knowledge representation, as well
 as their use in practical applications. This edition of LPNMR will feature
 several workshops, a special session dedicated to the 6th ASP Systems
 Competition, and will be collocated with the 4th Algorithmic Decision
 Theory Conference, ADT 2015. Joint LPNMR-ADT Doctoral Consortium will be
 a part of the program.

 Authors are invited to submit papers presenting original and unpublished
 research on all aspects of non-monotonic approaches in logic programming
 and knowledge representation. We invite submissions of both long and
 short papers.

TOPICS

 Conference topics include, but are not limited to:

 1. Foundations of LPNMR Systems:
   * Semantics of new and existing languages;
   * Action languages, causality;
   * Relationships among formalisms;
   * Complexity and expressive power;
   * Inference algorithms and heuristics for LPNMR systems;
   * Extensions of traditional LPNMR languages such as new logical
     connectives or new inference capabilities;
   * Updates, revision, and other operations on LPNMR systems;
   * Uncertainty in LPNMR systems.

 2. Implementation of LPNMR systems:
   * System descriptions, comparisons, evaluations;
   * Algorithms and novel techniques for efficient evaluation;
   * LPNMR benchmarks.

 3. Applications of LPNMR:
   * Use of LPNMR in formalization of Commonsense Reasoning and other
     areas of KR;
   * LPNMR languages and algorithms in planning, diagnosis, argumentation,
     reasoning with preferences, decision making and policies;
   * Applications of LPNMR languages in data integration and exchange
     systems, software engineering and model checking;
   * Applications of LPNMR to linguistics, psychology, and other sciences
   * Integration of LPNMR systems with other computational paradigms;
   * Embedded LPNMR: Systems using LPNMR subsystems.

SUBMISSION

 LPNMR 2015 welcomes submissions of long papers (13 pages) or short papers
 (6 pages) in the following categories:

   * Technical papers
   * System descriptions
   * Application descriptions

 The indicated number of pages includes title page, references and
 figures. All submissions will be peer-reviewed and accepted papers will
 appear in the conference proceedings published in the Springer-Verlag
 Lecture Notes in Artificial Intelligence (LNAI/LNCS) series. At least one
 author of each accepted paper is expected to register for the conference
 to present the work. Submissions must be formatted according to the
 Springer LNCS author instructions,

             http://www.springer.com/comp/lncs/Authors.html

 must be written in English, and present original research. Paper
 submission will be electronic through the LPNMR-15 Easychair site:

          https://www.easychair.org/conferences/?conf=lpnmr2015

 The Program Committee chairs are planning to arrange for the best papers to
 be published in a special issue of a premiere journal in the field.

MULTIPLE SUBMISSION POLICY

 LPNMR 2015 will not accept any paper which, at the time of submission, is
 under review or has already been published or accepted for publication in
 a journal or another conference. Authors are also required not to submit
 their papers elsewhere during LPNMR's review period. However, these
 restrictions do not apply to previous workshops with a limited audience
 and without archival proceedings.

ASSOCIATED EVENTS

  WORKSHOPS - LPNMR 2015 will include specialized workshops to be held on September 27
  prior to the main conference. Currently planned workshops include:

  - Grounding, Transforming, and Modularizing Theories with Variables
    Organizers: Marc Denecker, Tomi Janhunen

  - Action Languages, Process Modeling, and Policy Reasoning
    Organizer: Joohyung Lee

  - Natural Language Processing and Automated Reasoning
    Organizers: Marcello Balduccini, Ekaterina Ovchinnikova, Peter Schueller

  - Learning and Nonmonotonic Reasoning
    Organizers: Alessandra Russo and Alessandra Mileo

  ASP COMPETITION - A special session dedicated to a discussion of the
  6th ASP System Competition, including the methodology of the competition,
  benchmarks used, lessons learned and, most importantly, the results and
  the announcement of the winners.

  ALGORITHMIC DECISION THEORY (ADT) 2015 (collocated - same time and place)
  Algorithmic Decision Theory is a vibrant and growing area of research
  concerned with algorithmic aspects of problems arising in social choice
  and economics that involve optimal ways to aggregate preferences. The
  area abounds in hard computational problems and may be an axciting area
  of applications for ASP. The two conferences will seek ways to identify
  and promote synergies between their respective areas of focus.

JOINT LPNMR-ADT DOCTORAL CONSORTIUM:

  Details to be announced

  co-Chairs:
  - Esra Erdem (LPNMR), Sabanci University, Turkey
  - Nick Mattei (ADT), NICTA, Australia

IMPORTANT DATES (TENTATIVE)

   * Paper registration: April 13, 2015
   * Paper submission:   April 20, 2015
   * Notification:       June 1, 2015
   * Final versions due: June 15, 2015

VENUE

Lexington is a medium size, pleasant and quiet university town. It
is located in the heart of the so-called Bluegrass Region in
Central Kentucky. The city is surrounded by beautiful horse farms
on green pastures dotted with ponds and traditional architecture
stables, and small race tracks, and bordered by white or black
fences. The Horse Museum is as beautifully located as it is
interesting. Overall, the city has a nice feel that mixes well old
and new. The conference will be held in the Hilton Lexington
Downtown hotel.

GENERAL CHAIR
 Victor Marek, University of Kentucky, KY, USA

PROGRAM CHAIRS

 Giovambattista Ianni, University of Calabria, Italy
 Mirek Truszczynski, University of Kentucky, KY, USA

WORKSHOPS CHAIR

 Yuliya Lierler, University of Nebrska at Omaha, NE, USA

PUBLICITY CHAIR

 Francesco Calimeri, University of Calabria, Italy

PROGRAM COMMITTEE

 Agostino Dovier, Università di Udine, Italy
 Agustín Valverde, Universidad de Màlaga, Spain
 Alessandra Mileo, National University of Ireland, Galway, INSIGHT Centre for Data Analytics, Ireland
 Andrea Formisano, Dip. di Matematica e Informatica, Università di Perugia, Italy
 Axel Polleres, Vienna University of Economics and Business, Austria
 Bart Bogaerts, Department of Computer Science, KU Leuven, Belgium
 Chiaki Sakama, Wakayama University, Japan
 Chitta Baral, Arizona State University, USA
 Christoph Redl, Vienna University of Technology, Austria
 Daniela Inclezan, Miami University, USA
 David Pearce, Universidad Politécnica de Madrid, Spain
 Emilia Oikarinen, Aalto University, Finland
 Enrico Pontelli, New Mexico State University, USA
 Esra Erdem, Sabanci University, Istanbul, Turkey
 Eugenia Ternovska, Simon Fraser University, Canada
 Fangkai Yang, The University of Texas at Austin, USA
 Fangzhen Lin, Hong Kong University of Science and Technology, Hong Kong
 Francesco Calimeri, Università della Calabria, Italy
 Gerhard Brewka, Leipzig University, Germany
 Giovanni Grasso, Oxford University, UK
 Hannes Strass, Leipzig University, Germany
 Hans Tompits, Vienna University of Technology, Austria
 James Delgrande, Simon Fraser University, Canada
 Jia-Huai You, University of Alberta, Canada
 Joohyung Lee, Arizona State University, USA
 Jose Julio Alferes, Universidade Nova de Lisboa, Portugal
 Kewen Wang, Griffith University, Australia
 Marc Denecker, K.U.Leuven, Belgium
 Marcello Balduccini, Drexel University, USA
 Marina De Vos, University of Bath, UK
 Martin Gebser, University of Potsdam, Germany
 Matthias Knorr, CENTRIA, Universidade Nova de Lisboa, Portugal
 Mauricio Osorio, Fundacion de la Universidad de las Americas, Puebla, Mexico
 Michael Fink, Vienna University of Technology, Austria
 Michael Gelfond, Texas Tech University, USA
 Orkunt Sabuncu, University of Potsdam, Germany
 Paul Fodor, Stony Brook University, USA
 Pedro Cabalar, University of Corunna, Spain
 Saadat Anwar, Arizona State University, USA
 Stefan Woltran, Vienna University of Technology
 Stefania Costantini, Dipartimento di Ingegneria e Scienze dell'Informazione, e Matematica, Univ. di L'Aquila, Italy
 Terrance Swift, CENTRIA, Universidade Nova de Lisboa, Portugal
 Thomas Eiter, Vienna University of Technology, Austria
 Tomi Janhunen, Aalto University, Finland
 Torsten Schaub, University of Potsdam, Germany
 Tran Cao Son, New Mexico State University, USA
 Vladimir Lifschitz, University of Texas at Austin, USA
 Wolfgang Faber, University of Huddersfield, UK
 Yi Zhou, University of Western Sydney, Australia
 Yisong Wang, Guizhou University, China
 Yuliya Lierler, University of Kentucky, USA


CONTACT

 lpnmr2015@mat.unical.it
                                    
**************************** Call for Papers *********************************
**                                                                          **
**                           Special Issue on                               **
**                 SAT 2014 COMPETITIONS AND EVALUATIONS                    **
**                                                                          **
**    Journal on Satisfiability, Boolean Modeling and Computation (JSAT)    **
**                     http://satassociation.org/jsat/                      **
**                 ISSN: 1574-0617, published by OIS Press                  **
**                                                                          **
** Guest editors: Marijn Heule      The University of Texas at Austin, USA  **
**                Matti Jarvisalo   University of Helsinki, Finland         **
**                                                                          **
******************************************************************************


IMPORTANT DATES

Submission to the special issue is now open.

Submission deadline:     November 14, 2014
First round reviews:     January  30, 2015
Revision deadline:       March    30, 2015
Final notifications:     May      30, 2015

Final versions of accepted articles will be published online individually
as soon as received by the journal editors. The special issue will appear 
either as part of a regular volume or as a specific volume depending on the 
number of accepted papers.

MOTIVATION

Boolean satisfiability (SAT) and related solver competitions organized during 
the last two decades have been a stimulating force to improve SAT solvers and
related technologies.  These competitions have encouraged developing novel 
algorithms, optimized implementation-level techniques and data structures to 
increase the practical performance and robustness of solvers.  The competition 
benchmark suites are commonly used by the research community as the standard 
test set to evaluate progress.  Additionally, the competitions provide large 
amounts of openly available data on solver performance on a large spectrum of 
benchmark families that encode important real and artificial combinatorial
problems.

A lot more can be learned from these solver competitions than merely awarding 
and publishing the best-performing solvers. This special issue provides a venue 
to go beyond this, and welcomes research articles offering in-depth understanding 
of different aspects of the 2014 SAT-related solver competitions, inviting 
submissions describing solver techniques, benchmark families, competition reports, 
and thorough analysis and insights into the data produced by the competitions.


TOPICS OF INTEREST

Manuscripts addressing one or more of the following aspects of 2014 SAT-related
solver competitions are invited.

- Articles (full or system descriptions) presenting details on the algorithmic
  and implementation-level aspects of original solvers with remarkable performance
  during the SAT-related competitions within FLoC Olympic Games 2014:

    * SAT Competition,
    * Configurable SAT Solver Challenge,
    * MaxSAT Evaluation,
    * QBF Gallery,
    * Satisfiability Modulo Theories Competition,

  as well as other FLoC Olympic Games 2014 competitions tightly connected
  with Boolean satisfiability, such as the Hardware Model Checking Competition.
  Remarkable is to be interpreted broadly, from good overall performance to 
  very good performance on a specific set of benchmarks.

- Full articles by competition organizers reporting on SAT-related competitions 
  within FLoC Olympic Games 2014. The articles should describe the competition, 
  its criteria, why it is interesting to the SAT research community, execution 
  environment used, analysis of the results (including how they compare to 
  previous instantiations, if appropriate), and give a summary of the main 
  technical contributions to the field, as well as discussions on lessons 
  learned and suggestions for improvements for future competitions.

- Full articles presenting non-trivial in-depth analysis of the data produced 
  by SAT-related competitions within FLoC Olympic Games 2014. The articles 
  should give novel insights into the competition data, analyzing for example 
  the structure of competition benchmarks and their relation to the 
  effectiveness of different solver techniques in solving the benchmarks, 
  scoring methods for ranking solvers, sensitivity of competition results, etc.
  
- Full articles on new, relevant benchmark families submitted to the 
  competitions, and related analysis of the competition benchmarks.


SUBMISSION INFORMATION

Submissions should be written using the JSAT latex style files. System 
description submissions are limited to six pages in the JSAT style. 
Submission of manuscripts to the special issue are made via the JSAT journal
website http://satassociation.org/jsat/
by following the link "INFORMATION -> For Authors". 
After registering to the JSAT submission system, start a new submission,
and select "Special Issue on SAT 2014 Competitions and Evaluations" in the 
Journal Section selection menu in Step 1 of the submission procedure.

Submitted manuscripts should not have been published previously, nor be 
under review for publication elsewhere.

Please contact the special issue editors by email using 
satcompetitions2014@gmail.com
in case you have any questions regarding the special issue.
                                    
==================================================================
PostDoctoral position proposal in Propositional Satisfiability
==================================================================
Algorithms for Inference and Constraints group (CRIL, CNRS UMR 8188), at Lens (France), is offering a postDoctoral position.
---
ANR TUPLES wesite: http://www.lsis.org/tuples/
CRIL website: http://www.cril.univ-artois.fr/

Contact: 
Web: http://www.cril.univ-artois.fr/~sais/
E-mail: sais@cril.fr 

Requirements for a candidate: 
•	A PhD in Computer Science or equivalent diploma;
•	Expertise in Propositional Satisfiability (SAT), constraint programming (CP); Good programming skills. 

Offered: 
•	A full time, temporary appointment for a period of 6 months; 
•	Starting date: from September 2014 but possibly later (the postdoc has to take place between September 2014 and April 2015);
•	Monthly salary: 2000 euros net and negotiable based on the qualification profile;

This postdoc deals with the practical application of tractability results to enhance the efficiency of SAT solvers.
Until now, tractable classes have usually been studied from a purely theoretical point of view, their practical use
for solving general instances have not received much attention. For example, the current SAT solvers do not perform
any tractability analysis before or during the resolution of a given instance.

Our goal in this work is to bridge the gap between theory and practice by effectively exploiting the
tractability/intractability results to design the next generation of SAT solvers. The different results obtained in
the ANR project TUPLES “Tractability for Understanding and Pushing forward the Limits of Efficient Solvers” will
give us several possible research issues for the design of both strong simplification techniques (pre-processing) and
efficient solvers.
The consortium has a great experience in the development of SAT solvers. The CRIL team host and maintain several
solvers, which have won awards in the different SAT competitions.

Applications should include the following materials:
-	a motivation letter
-	a detailed CV (with publications)
-	two references 

Please apply as soon as possible. A first selection will be done during the last week of July 2014. Later applications
will be considered if no applicant has been selected at this date.

The position is located at CRIL, University of Artois, Lens (France).

Contact: Lakhdar Sais (sais@cril.fr) 
                                    
Call for Papers  *** Submission deadline July 9 2014 ***


                     ModRef 2014
The Thirteenth International Workshop 
on Constraint Modelling and Reformulation
http://cp2014.a4cp.org/workshops/modref14

at the

20th International Conference on the Principles and Practice 
of Constraint Programming (CP 2014) in Lyon, France, on 
September (TBD), 2014.

http://cp2014.a4cp.org/


Aims and Scope
==============

Constraint Programming (CP) is a powerful technology to model and
solve combinatorial problems, which are ubiquitous in academia and
industry. The last ten years or so have witnessed significant research
devoted to modelling and solving problems with constraints. CP is now
a mature field and has been successfully used for tackling a wide
range of real-life complex applications. However, such a technology is
currently accessible to only a small number of experts. For CP to be
more widely used by non-experts, more research effort is needed in
order to ease the use of the CP technology. We solicit original papers
that contribute to widen the use of the CP technology.

Workshop topics include (but are not limited to):

Application papers describing interesting problems and interesting
ways to model them;

Contributions to understanding modelling that could guide the manual
or automatic formulation of models;

Identification of the criteria that should be used in evaluating
models and the design of pragmatic techniques that facilitate the
choice and possibly combination among alternative models;

Design of higher-level modelling languages;

Automatic reformulation techniques.

The workshop will be held as a full-day or half-day workshop. Please
note that workshop-participants need to be registered for the
workshop. Past events of this workshop series can be found here
(http://www-users.cs.york.ac.uk/~frisch/ModRef/).


Important Dates
===============

Submission date:	July 9th, 2014
Notification of acceptance: August 15th, 2014
Camera ready version: August 22nd, 2014
Workshop day: September (TBD), 2014


Program Committee
=================

Carlos Ansotegui	Universitat de Lleida, Spain
Jessica Davies	University of Toronto
Ivan Dotu	UPC, Spain
Alan Frisch	University of York
Emmanuel Hebrard	LAAS, CNRS
George Katsirelos	INRA, Toulouse, France
Christopher Jefferson	University of St. Andrews, UK
Daniel Le Berre	Artois University, France
Jimmy Lee	The Chinese University of Hong Kong
Yuri Malitsky	Cork Constraint Computation Centre
Joao Marques-Silva	University College Dublin, Ireland
Ian Miqguel	University of St. Andrews, UK
Peter Nightingale	University of St. Andrews, UK
Jean-Charles Regin	University of Nice-Sophia Antipolis / I3S / CNRS
Ashish Sabharwal	IBM Research
Horst Samulowitz	IBM Research
Meinolf Sellmann	IBM Research
Roberto Sebastiani	University of Trento, Italy
Peter Stuckey	University of Melbourne, Australia
Mateu Villaret	Universitat de Girona, Spain

Submission
==========

Submissions must be formatted in the Lecture Notes in Computer Science
(LNCS) style and must be within 15 pages excluding
references. Submissions of shorter papers, including position papers,
are welcome.

Papers must be submitted in PDF format using EasyChair
(https://www.easychair.org/conferences/?conf=modref2014)

All submissions will be reviewed and those that are well-written and
make a worthwhile contribution to the topic of the workshop will be
accepted for publication in the workshop proceedings. The proceedings
will be available electronically at CP 2014. At least one author of
each accepted paper must attend the workshop. Please note that every
workshop participant needs to be registered for the workshop.

ModRef 2014 Chair:
=================

Carlos Ansotegui (carlos@diei.udl.es)
Call for Papers         *** Submission deadline June 30  2014 ***


                     Special Track on SAT and CSP
       http://www.cril.univ-artois.fr/ICTAI14-SAT-CSP-Track/

                                        at the

26th IEEE International Conference on Tools with Artificial
Intelligence (IEEE ICTAI’14)
                        http://ictai2014.cs.ucy.ac.cy/
                November 10-12 2014, Limassol, Chyprus


Constraint Solving Programming (CSP) and SAT-related technologies are
major related topics of research and application in A.I., opening up
new perspectives
about effective A.I. application domains.

Over the years, the ICTAI conference has become a major forum for the
CSP and SAT
research communities for presenting new high-quality results (see the
special track program in 2013:
http://www.cril.univ-artois.fr/ICTAI-SAT-CSP-Track/ICTAI-Schedule.htm )
The second edition of the special track is intended to further develop
the role of ICTAI in this respect.

Topics
=====

Topics of interest include, but are not limited to:

CSP methodologies and tools
Constraint networks
Global constraints
CSP and SAT Solvers
Applications of CSP and SAT-based technologies
Heuristic, complete and hybrid search techniques
Heuristics for SAT and CSP
SAT modulo theories
AI techniques based on SAT and CSP
Core, MUC and MUS extraction
MAX-SAT, MAX-CSP
Soft/Hard Constraints
Weighted CSP and SAT
Constraint optimization

Program Committee  (to be completed)
===============

Armin Biere
Manuel Bodirsky
Assef Chmeiss
Jean-François Condotta
Pierre Flener
Eric Gregoire (Co-Chair)
Katsumi Inoue
Jean-Marie Lagniez
Arnaud Lallouet
Daniel Le Berre
Christophe Lecoutre
Chu-Min Li
Mark Liffiton
Felip Manya
Joao Marques-Silva
Bertrand Mazure (Co-Chair)
Eric Monfroy
Barry O'Sullivan
Thierry Petit
Olivier Roussel
Michel Rueher
Lakhdar Saïs
Yakoub Salhi
Frédéric Saubion
Pierre Schaus
Naoyuki Tamura
Peter van Beek


Submissions
==========

Papers must be full papers up to 8 pages and obey the standard IEEE
formatting instructions
for conference papers (single-spaced, double-column, 10-point font size).

Papers must be submitted in pdf only through the Easychair special
track submission
page (NOT through the general ICTAI Easychair conference page).  See submission
instructions in  http://www.cril.univ-artois.fr/ICTAI14-SAT-CSP-Track/#submit

All papers will be reviewed by at least two members of the program committee.
Papers must report high-quality original work, be unpublished and not submitted
elsewhere during the whole ICTAI review process.

Each accepted paper must be presented by one of the authors and
accompanied by at
least one full ICTAI 2014 registration fee payment, to guarantee
publication in the
proceedings.

Proceedings and Special Journal Issue
=============================

All papers accepted in the CSP and SAT technologies special track will
be included in
the ICTAI 2014 main proceedings published by the IEEE Computer Society.
Extended versions of the best papers will be invited for publication in a
special issue of an International Journal after an additional round of reviews.

Important Dates
============

Paper submission                     30 June 2014
Notification                                3 September  2014
Camera-ready copy papers      24 September 2014

Contact
======

For reaching the PC Chairs (E. Gregoire and B. Mazure), please send email to
gregoire@cril.univ-artois.fr   mazure@cril.fr
                                    
Application Deadline is June 8, 2014.
Applicants will be informed of decision by June 17, 2014.

FLoC has some additional funds to provide travel grants of up to $750 for student attendees of FLoC’14.
Funds can be requested to cover airfare and lodging (registration fees and meals will not be funded).
We expect to award about 100 grants. The application deadline is June 8, 2014, and recipients will be
notified by June 17.

Funds will be provided after the conference, upon submission of receipts and a short report detailing
the student’s experience at and benefit from FLoC’14 (these reports will be used to compile a final
report to our sponsors). Awardees are expected to spend up to one day during the meeting helping with
logistics.

Applicants’ advisors should send a brief statement certifying their educational status and describing
their financial need, and merits. Special efforts will be made to bring to FLoC students from
under-represented groups. Applications must be received by the deadline. Applicants are required to
apply at the following web form:
https://docs.google.com/forms/d/1rdMGS8_YMKZRhm1MNiSZmIYCQ-QpyAe7vXGPsLt8eko/viewform

Advisor letters (plain text only) should be sent to floc14student@gmail.com by June 8, 2014.

If you have questions, please contact floc14student@gmail.com.
                                    
LogiCS - Doctoral College on Logical Methods in Computer Science

Funded Doctoral Positions in Computer Science

TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program LogiCS. The LogiCS doctoral college focuses on interdisciplinary research topics covering 

(i) computational logic, and applications of logic to
(ii) databases and artificial intelligence as well as to 
(iii) computer-aided verification.

THE PROGRAM

LogiCS is a doctoral college focusing on logic and its applications in computer science. Successful applicants will work with and be supervised by leading researchers in the fields of computational logic, databases and knowledge representation, and computer-aided verification.

FACULTY MEMBERS

M. Baaz     A. Biere  R. Bloem         A. Ciabattoni
U. Egly     T. Eiter  C. Fermuller     R. Grosu
A. Leitsch  M. Ortiz  R. Pichler       S. Szeider
H. Tompits  H. Veith  G. Weissenbacher

Details are provided on http://logic-cs.at/faculty/

POSITIONS AND FUNDING

We are looking for 1-2 doctoral students per faculty member, where 30% of the positions are reserved for highly qualified female candidates. The doctoral positions are funded for a period of 3 years according to the funding scheme of the Austrian Science Fund (details: http://www.fwf.ac.at/de/projects/personalkostensaetze.html)
The funding can be extended for one additional year contingent on a placement at one of our international partner institutions.

HOW TO APPLY

Detailed information about the application process is available on the LogiCS web-page http://logic-cs.at/phd/

The applicants are expected to have completed an excellent diploma or master's degree in computer science, mathematics, or a related field. Candidates with comparable achievements will be considered on a case-by-case basis. Applications by the candidates need to be submitted electronically.

HIGHEST QUALITY OF LIFE

The Austrian cities Vienna, Graz, and Linz, located close to the Alps and surrounded by beautiful nature, provide an exceptionally high quality of life, with a vibrant cultural scene, numerous cultural events, world-famous historical sites, a large international community, a varied cuisine and famous coffee houses.
                                    
First Workshop on Bridging the Gap Between Theory and Practice in Constraint Solvers
(http://cp2014.a4cp.org/workshops/bridginggap14)

This one-day workshop will be held at CP 2014, the 20th International
Conference on Principles and Practice of Constraint Programming
(http://cp2014.a4cp.org), on Monday 8 September 2014 in Lyon, France.


Aims and scope

For several years now, CP and SAT solvers have made tremendous advances that allow them to solve very large instances.
If the methods used to achieve this efficiency in practice are well-known, there does not exist to date any analytical explanation to justify the operational efficiency that seems totally at odds with the theoretical complexity of the problems addressed.

On the other hand, many studies have been developed for a long time on the detection of tractable classes in different areas or formalisms such as CSP, SAT, in planning, etc.
But these tractable classes are hardly ever used in practice and thus are generally not explicitly implemented in the solvers.

However, these two bodies of work seem to have been developed in parallel rather than in synergy, creating a real gap between these two aspects of constraint programming.
The purpose of this workshop is to better understand the reasons for the effectiveness of solvers, and also promote exchanges between researchers from both sides of the CP communities with the aim to reduce the gap between these two types of work.

The expected contributions cover a wide spectrum ranging from theoretical works on tractable classes, to implementations of solvers. They also concern the work on performance analysis of solvers. And ideally, work on the study of the properties explaining the behavior of efficient solvers.
We solicit original papers, but papers already published in journals or presented in conferences, particularly if they associate theory and practice are welcome.
This call for papers also includes position papers aimed at creating constructive and fruitful discussion between researchers working in theory and practice.
The workshop will be held as a full-day or half-day workshop. Please note that workshop-participants need to be registered for the workshop.

This workshop would like to bring together researchers interested in :
- implementation of solvers
- optimization of solvers
- analysis of solvers
- study and analysis of benchmarks
- experimentations
- analysis of practical efficiency
- competition of solvers
- complexity analysis
- tractability
- tractable classes
- complexity theory

Sponsorship

This workshop is sponsored by the Project TUPLES (http://www.lsis.org/tuples/) :
Tractability for Understanding and Pushing forward the Limits of Efficient Solvers
of the French National Agency for Research.

Important Dates

Submission date: June 30, 2014
Notification of acceptance: July 25, 2014
Camera ready version: August 15, 2014
Workshop day: September 8, 2014

Submission

Submissions must be formatted in the Lecture Notes in Computer Science (LNCS) style and must be at most 15 pages, excluding references. Submissions of short papers (no constraint for their lenght), including position papers, are welcome.
Papers must be submitted in PDF format by email to bgbtp.cp2014@gmail.com.
All submissions will be reviewed and those that are well-written and make a worthwhile contribution to the topic of the workshop will be accepted for publication in the workshop proceedings. The proceedings will be available electronically at CP 2014. At least one author of each accepted paper must attend the workshop. Please note that every workshop participant needs to be registered for the workshop.

Invited speaker

Joao Marques-Silva
Complex and Adaptive Systems Laboratory (CASL),
School of Computer Science and Informatics (CSI)
University College Dublin Belfield,
Dublin, Ireland

Organizers

- Philippe Jégou (main contact), LSIS - UMR CNRS 7296, Universite d'Aix-Marseille, France
  philippe.jegou@univ-amu.fr

- Martin Cooper, IRIT, Université de Toulouse III, France
  cooper@irit.fr

- Lakhdar Saïs, CRIL - CNRS, UMR 8188, Université Lille Nord de France, Artois, France
  sais@cril.fr
  
- Bruno Zanuttini, GREYC - UMR CNRS 6072, Universite de Caen Basse-Normandie, France
  bruno.zanuttini@unicaen.fr

Program Committee

- David Cohen (Royal Holloway, University of London, UK)
- Martin Cooper (IRIT-CNRS, Université de Toulouse III, France)
- Stéphane Grandcolas (LSIS-CNRS, Universite d'Aix-Marseille, France)
- Emmanuel Hébrard (LAAS-CNRS, France)
- Peter Jeavons (University of Oxford, UK)
- Philippe Jégou (LSIS-CNRS, Universite d'Aix-Marseille, France)
- Daniel Le Berre (CRIL-CNRS, Université Lille Nord de France, Artois, France)
- Fred Maris (IRIT-CNRS, Université de Toulouse III, France)
- Pierre Marquis (CRIL-CNRS, Université Lille Nord de France, Artois, France)
- Bertand Mazure (CRIL-CNRS, Université Lille Nord de France, Artois, France)
- Cyril Pain-Barre (LSIS-CNRS, Universite d'Aix-Marseille, France)
- Lionel Paris (LSIS-CNRS, Universite d'Aix-Marseille, France)
- Pierre Régnier (IRIT-CNRS, Université de Toulouse III, France)
- Lakhdar Saïs (CRIL-CNRS, Université Lille Nord de France, Artois, France)
- Cyril Terrioux (LSIS-CNRS, Universite d'Aix-Marseille, France)
- Bruno Zanuttini (GREYC-CNRS, Universite de Caen Basse-Normandie, France)
                                    
CALL FOR CONTRIBUTIONS

Configurable SAT Solver Challenge (CSSC) 2014

http://aclib.net/cssc2014/

Event affiliated with SAT 2013 conference

http://baldur.iti.kit.edu/sat2014/

July 14 - 17, 2014, Vienna, Austria

-----------------------

Most modern SAT solvers have a large number of parameters that can be altered to adjust their behavior and performance. Following last year's inaugural Configurable SAT Solver Challenge (CSSC), we will hold CSSC 2014, a competitive event that assesses the *peak performance* of such parametric solvers (i.e. performance with optimized parameters). Thereby, CSSC recognizes that the value of a SAT solver for a given application is often is due to its customizability rather than just its performance in a default configuration.

To obtain a good approximation of the peak performance attainable in practice, we will use a fixed computational budget to optimize parameter settings with state-of-the-art software (so-called “algorithm configuration” procedures) recently developed by several groups.

We will reward SAT solvers that can be flexibly configured to perform well in different circumstances (as opposed to having one single best configuration). The results will be presented at this year's SAT conference.

We invite submissions of both configurable SAT solvers and benchmark instance generators. Although we will accept closed-source solvers, only open-source submissions will be eligible for awards. To minimize the overhead for solver designers, the deadlines are arranged to fall just after those of the SAT competition.

More details about the submission process, and the rules of the competition, can be found on our website: http://aclib.net/cssc2014/

===== Important Dates =====

May 18: submission deadline for solvers and benchmarks

July 14-17: presentation of results during SAT 2013 conference


===== Organizers =====

Frank Hutter (University of Freiburg)

Marius Lindauer (University of Freiburg)

Sam Bayless (University of British Columbia)

Holger Hoos (University of British Columbia)

Kevin Leyton-Brown (University of British Columbia)


===== Contact =====

cssc.organizers@gmail.com
http://aclib.net/cssc2014/

                                    
                 WORKSHOP ON LOGIC AND SEARCH - LaSh 2014
           Representing and Solving Computational Search Problems

                       Final Call For Submissions

   With Revised Submission Deadline (May 15), Final PC, Confirmed Speakers

                     Vienna, Austria, July 18, 2014
                        http://vsl2014.at/lash/

            A FLoC 2014 Workshop, Associated with SAT and ICLP

OVERVIEW

The purpose of the LaSh workshops is to foster scientific exchange on
subjects related to languages for representing, and methods for solving,
computationally challenging search problems.  The scope includes study of
relevant logics, algorithms, and logic-based systems, and also study of
other languages and systems from the viewpoint of logic, broadly construed.

Hard combinatorial search and optimization problems abound in science,
engineering, and other areas.  Examples include planning, scheduling and
configuration problems. Several communities have developed general purpose
solving technologies for such problems, supported by declarative modelling
or specification languages.  These include answer set programming (ASP)
from knowledge representation (KR), constraint solvers and modelling languages
from constraint programming (CP), and integer linear programming (ILP) solvers
and algebraic modelling languages from mathematical programming.  Other
relevant areas include propositional satisfiability (SAT), satisfiability
modulo theories (SMT), and representation languages based on classical
logic and FO(ID).

Differences in emphasis notwithstanding, these share the same purpose.
Indeed, there are many similarities in solving technologies, and increasing
exchange between the areas both in solving and representational issues.
From a logical point of view, whether a given language or system is
described in logical terms or not, we have languages which define some
class of structures, and systems whose purpose is to compute structures
in the class.  Logic may be seen as an explicit basis for building systems,
as an analytic tool, or as a formal approach to viewing the diversity of
systems more uniformly.

Topics of interest include, but are not limited to:

    - Logics relevant to the study of search and optimization problems
    - Languages for specifying or modelling search or optimization problems
    - Reasoning about or with specifications of search problems
    - Grounding and related language transformation methods
    - Expressiveness and complexity of logics and languages
    - Ground Solvers and their languages: SAT, ASP, SMT, FlatZinc, etc.
    - New or extended ground solver languages: SAT+Cardinality, SAT+TC, etc.
    - Design of systems, solvers, and related tools
    - Approximation, tractable problem classes, etc.
    - Proof systems and inference methods underlying solvers.
    - Comparisons of different languages or methods
    - Interesting applications, either as case studies or challenges
    - Benchmark problems and instance collections

CONFIRMED SPEAKERS
Konstantin Korovin ("Plenary")
Tomi Janhunen
Stefan Woltran

IMPORTANT DATES

Submission:  May 15 (Extended)
Notification:   May 21 (Revised)
Final Versions: May 27 (Revised)
Workshop: July 18

ORGANIZERS

Marc Denecker, KU Leuven
David Mitchell, Simon Fraser University
Emilia Oikarinen, Aalto University

PROGRAM COMMITTEE

David Bergman (University of Connecticut)
Marc Denecker (K.U.Leuven) - chair
Alan Frisch (University of York)
Wolfgang Faber (University of Huddersfield)
Marijn Heule (The University of Texas at Austin)
Tomi Janhunen (Aalto University)
Matti Järvisalo (University of Helsinki)
Ian Miguel (University of St Andrews)
David Mitchell (Simon Fraser University) - chair
Emilia Oikarinen (Aalto University) - chair
Shahab Tasharrofi (Simon Fraser University)
Eugenia Ternovska (Simon Fraser University)
Mirek Truszczynski (Computer Science Department, University of Kentucky)

SUBMISSION INFORMATION

To encourage communication across areas, LaSh is a non-archival meeting.
In addition to new technical work, we welcome presentation of relevant material
which has appeared at conferences area-specific meetings or general conferences,
and also position papers, challenges, system descriptions and speculative work.

                                    

CFP: Extended Deadline for 11th International Workshop on Boolean Problems (IWSBP’14)

Freiberg (Sachs.), Germany, September 17 - 19, 2014

http://www.informatik.tu-freiberg.de/prof2/ws_bp11/index.html

Important Dates:

Submission deadline: May 10, 2014 (EXTENDED DEADLINE)

Notification of acceptance: June 6, 2014

Final version due: July 6, 2014

 

The workshop on Boolean problems has an emphasis on the problems related to the solution of
all kinds of high-dimension Boolean and discrete problems, and provides a forum for
researchers and engineers from different disciplines to exchange ideas. The workshop is
devoted to theoretical discoveries, as well as practical applications. An aim of the
workshop is to initiate possible collaborative research, and to find new areas of
application. It is intended to publish the papers in proceedings.

The invited speakers will be:

- Mitch Thornton (SMU Dallas (Texas), USA),
- Jaap van den Herik (Tilburg University, Netherlands), and
- Shinobu Nagayama (Hiroshima City University, Japan)

 

Topics of interest include, but are not limited to:

- Theory
- Properties and applications of Boolean Algebras
- Data Structures and Algorithms
- Modeling
- Specification of data structures/Algorithms
- Complexity
- Program Systems/Software
- Fundamental software for the solution of Boolean Problems
- Comparison of efficiency
- Practical Applications
- Application of Boolean Algebra in FPGA synthesis
- Quantum logic, reversible logic, and multi-valued logic
- Solution of real-world problems

 

Submissions:

To submit a paper, please send an extended abstract, as a PDF file no longer than 6 pages
using the workshop web page:
http://www.informatik.tu-freiberg.de/prof2/ws_bp11/

or send a PDF file to: iwsbp2014@informatik.tu-freiberg.de

by May 10, 2014.

 

General Chair: Prof. Dr.-Ing. B. Steinbach, TU Bergakademie Freiberg

Conference Coordinator: Dr.-Ing. G. Rudolf, TU Bergakademie Freiberg

Publicity Chair: M. Velev, Aries Design Automation, USA

 

Program Committee:

- M. Adamski, University of Zielona Gora, Poland
- J. Butler, Naval Postgraduate School Monterey, USA
- R. Berghammer, C-A-University of Kiel, Germany
- L. Cheremisinova, Minsk Academy of Science, Belarus
- D. Debnath, Oakland University, USA
- R. Drechsler, University of Bremen, Germany
- E. Dubrova, Royal Institute of Technology (KTH), Sweden
- G. Dueck, University of New Brunswick, Canada
- V. Gaudet, University of Waterloo, Ontario, Canada
- D. Große , University of Bremen, Germany
- A. Karatkevich, University of Zielona Gora, Poland
- P. Kerntopf, Warsaw University of Technology and University of Lodz, Poland
- I. Levin, Tel Aviv University, Israel
- T. Luba, Warsaw University of Technology, Poland
- M. Lukac, Tohoku University, Sendai, Japan
- M. Miller, University of Victoria, Canada
- C. Moraga, TU Dortmund, Germany
- M. A. Perkowski, Portland State University, USA
- Y. Pottosin, Minsk Academy of Science, Belarus
- T. Sasao, Kyushu Institute of Technology, Japan
- Ch. Scholl, University of Freiburg, Germany
- R. Stankovic, University of Nis, Serbia
- B. Steinbach, University of Freiberg, Germany
- R. Ubar, Tallinn Technical University, Estonia
- M. Velev, Aries Design Automation, USA
- R. Wille, University of Bremen, Germany
- S. Yanushkevich, University of Calgary, Canada

 

Conference Language: English
            

CALL FOR CONTRIBUTIONS

QBF Gallery 2014

http://qbf.satisfiability.org/gallery

Competition affiliated with

FLoC Olympic Games 2014, http://vsl2014.at/olympics/
SAT 2014 conference, http://baldur.iti.kit.edu/sat2014/
QBF 2014 workshop, http://vsl2014.at/qbf/

at the Vienna Summer of Logic 2014, July 14 - 17, 2014
http://vsl2014.at

-----------------------


The QBF Gallery 2014 is a competitive event to evaluate
the state-of-the-art in QBF solving.

The QBF Gallery 2014 invites submissions of competing
QBF solvers (PCNF as well as non-PCNF solvers),
related tools like preprocessors as well as novel benchmark
instances to challenge current solvers.


---------------
DETAILS
---------------

For details on the competition and instructions on how to submit,
visit the QBF Gallery Webpage at

http://qbf.satisfiability.org/gallery


---------------
IMPORTANT DATES
---------------

2014-04-15: final submission of PCNF solvers

2014-04-30: final submission of non-PCNF solvers, any tools, and benchmarks

April, May, June 2014: evaluation runs

2014-07-13: presentation of results at the QBF 2014 Workshop


---------------
CONTACT
---------------

For any questions, please contact  qbfgallery2014@easychair.org.

                                    
Job Description

Responsible for formal verification to enhance the performance and feature-set of the Atrenta Spyglass
product family.
Develop, prototype, and integrate new technologies into existing products.
Capture user requirements and write detailed specifications for implementation.
Provide technical direction and overall usability & use-model by gathering customer requirements and
work closely with engineering in India and US, marketing and other groups to define, architect and develop
these products.

Desired Skills & Experience

Ph.D. in CS/CE/EE or experience in developing advanced algorithms for EDA. In-depth knowledge and experience with
some of the following technologies:

Symbolic simulation and model checking (BMC, TI, IP, IC3/PDR)
Formal data structures and solvers (BDD, AIG, SAT, SMT)
Assertion languages and temporal logics (SVA, PSL, LTL, CTL)
Combinational and sequential equivalence checking
Logic synthesis and optimization
Expert knowledge in data structures, algorithm complexity analysis, graph theory
Expert knowledge in prototyping, benchmarking, and integrating algorithms using C++
Excellent software engineering skills, very hands on with standard development tools: 
Make, GCC, GDB and Valgrind
Familiar with System Verilog/VHDL and the VLSI design flow
Familiar with script languages (Python, Perl, Tcl/Tk)
Able to deliver projects in a timely manner with high quality and take responsibility for all deliverables

Other requirements

Able to learn new technologies and integrate them into existing products
Excellent technical interpretation skills
Excellent communication and interpersonal skills
Experience working with a remote development team
Please, apply to francejobs@atrenta.com
                 WORKSHOP ON LOGIC AND SEARCH - LaSh 2014
           Representing and Solving Computational Search Problems

                         Call For Submissions

                     Vienna, Austria, July 18, 2014
                        http://vsl2014.at/lash/

OVERVIEW

The purpose of the LaSh workshops is to foster scientific exchange on 
subjects related to languages for representing, and methods for solving,
computationally challenging search problems.  The scope includes study of 
relevant logics, algorithms, and logic-based systems, and also study of 
other languages and systems from the viewpoint of logic, broadly construed.  

Hard combinatorial search and optimization problems abound in science, 
engineering, and other areas.  Examples include planning, scheduling and 
configuration problems. Several communities have developed general purpose 
solving technologies for such problems, supported by declarative modelling 
or specification languages.  These include answer set programming (ASP) 
from knowledge representation (KR), constraint solvers and modelling languages 
from constraint programming (CP), and integer linear programming (ILP) solvers 
and algebraic modelling languages from mathematical programming.  Other 
relevant areas include propositional satisfiability (SAT), satisfiability 
modulo theories (SMT), and representation languages based on classical 
logic and FO(ID). 

Differences in emphasis notwithstanding, these share the same purpose.
Indeed, there are many similarities in solving technologies, and increasing 
exchange between the areas both in solving and representational issues.  
From a logical point of view, whether a given language or system is 
described in logical terms or not, we have languages which define some 
class of structures, and systems whose purpose is to compute structures 
in the class.  Logic may be seen as an explicit basis for building systems, 
as an analytic tool, or as a formal approach to viewing the diversity of 
systems more uniformly.  

Topics of interest include, but are not limited to:

    - Logics relevant to the study of search and optimization problems
    - Languages for specifying or modelling search or optimization problems
    - Reasoning about or with specifications of search problems
    - Grounding and related language transformation methods
    - Expressiveness and complexity of logics and languages
    - Ground Solvers and their languages: SAT, ASP, SMT, FlatZinc, etc. 
    - New or extended ground solver languages: SAT+Cardinality, SAT+TC, etc.
    - Design of systems, solvers, and related tools
    - Approximation, tractable problem classes, etc.
    - Proof systems and inference methods underlying solvers.
    - Comparisons of different languages or methods 
    - Interesting applications, either as case studies or challenges 
    - Benchmark problems and instance collections


IMPORTANT DATES

Submission:  April 17
Notification:   May 1
Final Versions: May 20
Workshop: July 18

ORGANIZERS

Marc Denecker, KU Leuven
David Mitchell, Simon Fraser University
Emilia Oikarinen, Aalto University  

PROGRAM COMMITTEE 

TBA

SUBMISSION INFORMATION 

To encourage communication across areas, LaSh is a non-archival meeting.  
In addition to new technical work, we welcome presentation of relevant material 
which has appeared at conferences area-specific meetings or general conferences, 
and also position papers, challenges, system descriptions and speculative work.
                                    
SAT Competition 2014
http://satcompetition.org/2014/

Affiliated with the SAT 2014 conference, July 14-17 in Vienna, Austria,
and the FLoC Olympic Games

SAT Competition 2014 invites submissions of both competing SAT solvers and new competition benchmark instances.

The SAT Competition 2014 is a competitive event for solvers for the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014) and stands in the tradition of the SAT Competitions that have been held yearly from 2002 to 2005 and biannually starting from 2007, the SAT-Races held in 2006, 2008 and 2010, and the SAT Challenge 2012.

The emphasis of SAT Competition 2014 is on evaluation of core solvers. As in SAT Competition 2013, the UNSAT tracks of the competition will require certification.

DETAILS

For details on the competition and instructions on how to submit solvers and benchmarks, visit the SAT Competition 2014 webpages at
http://satcompetition.org/2014/

IMPORTANT DATES

All dates are during the year 2014. Deadlines are 23:59 anywhere on earth (GMT −12).
April 21        Solver registration and testing period opens
April 21        Benchmarks and generators submission opens
April 30        Final versions of registered solvers due
April 30        Benchmarks and generators submission closes
May 1 - June 23         Execution of the competition
May 12  Last possible submission of latex sources of solver and benchmark descriptions
June 23 - June 30       Checking of the results by the participants
Around July 14 - 17     Announcement of results at the SAT 2014 conference
===============================================================================
                               CALL FOR PAPERS
                                 ASPOCP 2014
     7th Workshop on Answer Set Programming and Other Computing Paradigms
                    https://sites.google.com/site/aspocp2014
                              July 23rd, 2014
 
    Affiliated with the International Conference on Logic Programming 2014
                  (part of the Federated Logic Conference 2014)
                               Vienna, Austria
                              July 19-22, 2014

                Collocated with the Vienna Summer of Logic 2014
                               Vienna, Austria
                              July 12-24, 2014

===============================================================================

AIMS AND SCOPE
 Since its introduction in the late 1980s, answer set programming (ASP)
 has been widely applied to various knowledge-intensive tasks and
 combinatorial search problems. ASP was found to be closely related to
 SAT, which has led to a method of computing answer sets using SAT
 solvers and techniques adapted from SAT. While this has been the most
 studied relationship which is currently extended towards
 satisfiability modulo theories (SMT), the relationship of ASP to other
 computing paradigms, such as constraint satisfaction, quantified
 boolean formulas (QBF), first-order logic (FOL), or FO(ID) logic is
 also the subject of active research. New methods of computing answer
 sets are being developed based on the relation between ASP and other
 paradigms, such as the use of pseudo-Boolean solvers, QBF solvers, FOL
 theorem provers, and CLP systems.
 Furthermore, the practical applications of ASP also foster work on
 multi-paradigm problem-solving, and in particular language and solver
 integration. The most prominent examples in this area currently are the
 integration of ASP with description logics (in the realm of the
 Semantic Web), constraint satisfaction, and general means of external
 computation.  This workshop will  facilitate the discussion about
 crossing the boundaries of current ASP techniques in theory, solving,
 and applications, in combination with or inspired by other computing
 paradigms.


TOPICS
 Topics of interests include (but are not limited to):
 - ASP and classical logic formalisms (SAT/FOL/QBF/SMT/DL).
 - ASP and constraint programming.
 - ASP and other logic programming paradigms, e.g., FO(ID).
 - ASP and other nonmonotonic languages, e.g., action languages.
 - ASP and external means of computation.
 - ASP and probabilistic reasoning.
 - ASP and machine learning.
 - New methods of computing answer sets using algorithms or systems of
   other paradigms.
 - Language extensions to ASP.
 - ASP and multi-agent systems.
 - ASP and multi-context systems.
 - Modularity and ASP.
 - ASP and argumentation.
 - Multi-paradigm problem solving involving ASP.
 - Evaluation and comparison of ASP to other paradigms.
 - ASP and related paradigms in applications.
 - Hybridizing ASP with procedural approaches.
 - Enhanced grounding or beyond grounding.


SUBMISSIONS
 Papers must describe original research and should not exceed 15 pages
 in the Springer LNCS format .
 Paper submission will be handled electronically by means of the
 Easychair system. The submission page is available at
 https://www.easychair.org/conferences/?conf=aspocp14


IMPORTANT DATES
 Abstract and paper submission deadline:         April 1, 2014
 Notification:               	 		 May 1, 2014
 Camera-ready articles due:  	       		 May 20, 2014
 Workshop:             		       		 July 23, 2014


LOCATION 
 The workshop will be held in Vienna, Austria, collocated with
 the International Conference on Logic Programming (ICLP) 2014.


PROCEEDINGS
 Accepted papers will be made available online and published in the
 Computing Research Repository (CoRR) afterwards.

 A selection of extended and revised versions of accepted papers will
 appear in a special issue of the Journal of Logic and Computation
 (http://logcom.oxfordjournals.org/), provided that a sufficient
 amount of high quality papers is collected.

 Such papers will go through a second formal selection process to meet
 the high quality standard of the journal.


TIMELINE FOR THE SPECIAL ISSUE (PRELIMINARY)
 Expression of interest/invitation:		   Right after the workshop
 First submissions:				   Fall 2014
 Revision of manuscripts:		
 (for papers not already accepted or rejected)     Spring 2015
 Final notification/version of accepted papers 	   Summer 2015


WORKSHOP CO-CHAIRS
 Daniela Inclezan, Miami University, USA
 Marco Maratea, DIBRIS - University of Genova, Italy


PROGRAM COMMITTEE
 Marcello Balduccini, Drexler University, USA
 Gerhard Brewka, University of Leipzig, Germany 
 Pedro Cabalar, Corunna University, Spain
 Wolfgang Faber, University of Huddersfield, UK
 Cristina Feier, University of Oxford, UK
 Johannes Klaus	Fichte, Vienna University of Technology, Austria
 Michael Fink, Vienna University of Technology, Austria
 Gregory Gelfond, Arizona State University, USA
 Michael Gelfond, Texas Tech University, USA
 Enrico Giunchiglia, University of Genova, Italy
 Giovambattista Ianni, University of Calabria, Italy
 Tomi Janhunen, Aalto University, Finland
 Joohyung Lee, Arizona State University, USA
 Joao Leite, New University of Lisbon, Portugal
 Yuliya Lierler, University of Nebraska at Omaha, USA
 Vladimir Lifschitz, University of Texas at Austin, USA
 Alessandro Mosca, Free University of Bolzano, Italy
 Emilia Oikarinen, Aalto University, Finland
 Max Ostrowski, University of Potsdam, Germany
 Axel Polleres, Vienna University of Economics & Business, Austria
 Francesco Ricca, University of Calabria, Italy
 Guillermo R. Simari, Universidad Nacional del Sur, Argentina
 Evgenia Ternovska, Simon Fraser University, Canada
 Hans Tompits, Vienna University of Technology, Austria
 Miroslaw Truszczynski, University of Kentucky, USA
 Joost Vennekens, Catholic University of Leuven, Belgium
 Marina De Vos, University of Bath, UK
 Stefan Woltran, Vienna University of Technology, Austria
 Fangkai Yang, University of Texas at Austin, USA
 Jia-Huai You, University of Alberta, Canada
CALL FOR CONTRIBUTIONS

Date:     July 17-18, 2014
Location: Vienna, Austria (co-located with the Vienna Summer of Logic)
Web:      http://vsl2014.at/meetings/iPRA-index.html

IMPORTANT DATES

Submission deadline: April 30, 2014, AOE
Notification:        May 7, 2014
Workshop:            July 17-18, 2014

ORGANISATION AND COMMITTEE

Laura Kovacs and Georg Weissenbacher

SCOPE

Craig interpolation enjoys a continuing popularity in computer
science. Historically, Craig's interpolation theorem has received
ample attention in proof theory and mathematical logic as well as in
complexity theory. Recently, interpolants are increasingly used in
automated verification, synthesis, and description logics. The aim of
the workshop is to bring together theoreticians and practitioners from
these different fields.

We solicit submissions in form of an abstract of at most one page in
PDF format. The authors of accepted abstracts are required to
present their work at the workshop. There will be no published
proceedings.

We encourage submissions presenting work in progress, tools under
development, as well as research of PhD students, such that the
workshop can become a forum for active dialog between the groups
involved in applications of interpolation. We also encourage
contributions from outside the verification community.

Presentations of recently published papers are also allowed and
encouraged, but please indicate on your submission where the paper was
published/presented.

Relevant topics include (but are not limited to) applications of
interpolation in:

- Interpolating decision procedures
- Proof theoretic approaches to interpolation
- Proof systems and calculi for interpolation
- Proof transformation techniques
- Inductive Proofs
- Logical Abduction
- Interpolation techniques based on constraint solving, linear programming...
- Alternative techniques for interpolation
- Interpolation theorems (for theories and extensions, non-classical
logic, ...)
- Interpolation-based/Inductive invariant generation
- Program analysis and verification
- Tools for interpolation
- Applications of Craig interpolation (verification, synthesis,
automated reasoning, ...)
- Forgetting, variable elimination, and uniform interpolation
- Complexity results and limitations
...

FORMAT

The workshop will feature

- invited talks and tutorials by distinguished speakers,
- presentations (selected by a committee based on the submission of
abstracts) by workshop participants, and
- discussion and panel sessions.

INVITED TALKS

As part of the workshop program we will have invited talks given by
the following distinguished speakers:

- Orna Grumberg (Technion, Israel)
- Pavel Pudlák (Academy of Sciences, Czech Republic)
- Frank Wolter (University of Liverpool, UK)

The titles and abstracts of the talks/tutorials will be announced
on the workshop web-page closer to the date.

SUBMISSION INSTRUCTIONS

Abstracts (at most one page in PDF format) have to be submitted until
April 30 via the EasyChair system:

https://www.easychair.org/conferences/?conf=ipra2014

The authors will be notified on May 7, 2014.
There will be no formal workshop proceedings.

REGISTRATION

Registration for the workshop will be possible via the VSL
registration site http://vsl2014.at/registration/.
===========================================

FIRST CALL FOR PARTICIPATION


Fourth International SAT/SMT Summer School

Semmering, Austria, July 10-12, 2014

http://satsmt2014.forsyte.at/

===========================================


REGISTRATION:


The registration deadline for the summer school is April 19, 2014.
Full details of the registration procedure as well as travel and
accommodation grants are available at the school website
(http://satsmt2014.forsyte.at/).

ABOUT:

Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers
have become the backbone of numerous applications in computer science,
such as automated verification, artificial intelligence, program
synthesis, security, product configuration, and many more. The summer
school covers the foundational and practical aspects of SAT and SMT
technologies and their applications.

Besides providing a well structured introduction to SAT and SMT, this
year’s edition of the SAT/SMT Summer School covers timely topics and
novel applications such as

- parallel solvers,
- theories with quantifiers,
- the IC3 model checking paradigm,
- hardware and software verification,
- proofs and Craig interpolation,
- and cryptography,

presented by distinguished speakers and experts in these fields. In
addition to the theory sessions, we will have practicals in which the
participants will work state-of-the-art tools and solvers.

The fourth edition follows the schools that took place at MIT (SAT/SMT
Solver Summer School 2011), at Fondazione Bruno Kessler (SAT/SMT
School 2012) in Trento, Italy, and Aalto University in Espoo, Finland
in 2013.  The school location and schedule has been chosen to
integrate nicely with the Vienna Summer of Logic (VSL 2014,
seehttp://vsl2014.at/). As a reminder, VSL 2014 includes, among many
other events:

* the 17th International Conference on Theory and Applications of
Satisfiability Testing (SAT 2014)

* the 26th International Conference on Computer Aided Verification (CAV 2014)

* the 12th International Workshop on Satisfiability Modulo Theories (SMT 2014)

* the 7th International Joint Conference on Automated Reasoning (IJCAR 2014)


The Summer School program will feature four lectures per day, with the
first two days dedicated to SAT and SMT, and the last to special
topics. Two of the lectures will be organized as tutorials giving
hands-on experience on SAT/SMT-based modelling.


List of invited lectures:

* Introduction to SAT, Daniel Le Berre

* Practical Session SAT, Keijo Heljanko, Tomi Janhunen, Tommi Junttila

* Interpolation in SAT & SMT, Philipp Rümmer

* Parallel SAT Solving, Christoph Wintersteiger

* Proofs in SAT and CSP, Ofer Strichman

* Introduction to SMT, Alberto Griggio

* Quantifiers in SMT, Leonardo de Moura

* Practical Session SMT, Keijo Heljanko, Tomi Janhunen, Tommi Junttila

* SMT for Cryptography & Software Verification, Chao Wang

* Hardware Verification with IC3, Fabio Somenzi

* Software Verification with IC3, Nikolaj Bjørner


A more detailed program is available at the school website
(http://satsmt2014.forsyte.at/).


Organizers:

Clark Barrett (New York University)

Pascal Fontaine (Inria, Loria, University of Lorraine, France)

Dejan Jovanović (SRI, U.S.)

Georg Weissenbacher (TU Wien, Austria)
                    
* __________________________________________________________________________   *

                              Call for papers 

                           The 21st RCRA workshop:
             Experimental evaluation of algorithms for solving
                  problems with combinatorial explosion  

                             --- RCRA 2014 ---

           A FLoC workshop at the Vienna Summer of Logic (VSL 2014)
              Affiliated with SAT 2014, ICLP 2014, IJCAR 2014

                      Vienna, Austria, July 17-18, 2014

  RCRA group web site: http://rcra.aixia.it/
  Workshop web site:   http://rcra.aixia.it/rcra2014
  e-mail:              rcra2014@gmail.com

* __________________________________________________________________________   *

  The 21st edition of the RCRA workshop will take place in Vienna during 
  the Vienna Summer of Logic ( VSL - htpp://http://vsl2014.at ) which will 
  be the largest event in the history of logic. VSL will consist of twelve 
  large conferences and many workshops, attracting researchers from all over 
  the world.

  RCRA 2014 is a FLoC workshop affiliated with SAT 2014, ICLP 2014, IJCAR 2014.
  It will be held in the Workshop Block 2 ( see http://vsl2014.at/ataglance ) 
  after SAT 2014 and before ICLP2014 and IJCAR2014.

  As in previous editions (http://rcra.aixia.it/publications), authors of
  papers orally presented at the workshop will have the opportunity to 
  participate to the selection of a special issue that will appear on an 
  international journal.


IMPORTANT DATES 

  * Submission deadline for abstracts:  March 25, 2014
  * Submission deadline for papers:     April 1, 2014
  * Acceptance/reject notification:     May 1, 2014
  * Camera-ready papers due:            May 20, 2014
  * RCRA 2014:                          July 17-18, 2014


HISTORY OF THE WORKSHOP SERIES

  The RCRA workshops are organized by the RCRA (Knowledge Representation 
  & Automated Reasoning) group of the Italian Association for Artificial 
  Intelligence.

  The last editions have been as follows:

  * RCRA 2013, Rome, Italy - http://rcra.aixia.it/rcra2013
    Extended versions of the best papers will appear in a special issue of 
    Journal of Experimental and Theoretical Artificial Intelligence 
  * RCRA 2012 as a workshop of AI*IA 2012, Rome, Italy - http://rcra.aixia.it/rcra2012
    Extended versions of the best papers will appear in a special issue of 
    AI Communications
  * RCRA 2011 as a workshop of IJCAI 2011, Barcelona, Spain - http://rcra.aixia.it/rcra2011
    Extended versions of the best papers appear in a special issue of 
    AI Communications
  * Previous editions: http://rcra.aixia.it/workshops


AIMS AND SCOPE

  Many problems in Artificial Intelligence show an exponential explosion of the
  search space.  Although stemming from different research areas in AI, such
  problems are often addressed with algorithms that have a common goal: the
  effective exploration of huge state spaces.  Many algorithms developed in one
  research area are applicable to other problems, or can be hybridized with
  techniques in other areas. Artificial Intelligence tools often exploit or
  hybridize techniques developed by other research communities, such as
  Operations Research.
  In recent years, research in Artificial Intelligence has more and
  more focused on experimental evaluation of algorithms, the
  development of suitable methodologies for experimentation and
  analysis, the study of languages and the implementation of systems
  for the definition and solution of problems.

  Scope of the workshop is fostering the cross-fertilization of ideas stemming
  from different areas, proposing benchmarks for new challenging problems,
  comparing models and algorithms from an experimental viewpoint, and, in
  general, comparing different approaches with respect to efficiency, problem
  modeling, and ease of development.

  Topics of interest include, but are not limited to:
  * Experimental evaluation of algorithms for
       o knowledge representation
       o automated reasoning
       o planning
       o scheduling
       o machine learning
       o model checking
       o boolean satisfiability (SAT)
       o constraint programming
       o temporal reasoning
       o combinatorial optimization
       o quantified boolean formulae and quantified constraints
       o modal logics
       o logic programming
       o answer set programming 
       o ontological reasoning       
  * Definition and construction of benchmarks
  * Experimentation methodologies
  * Metaheuristics
  * Algorithm hybridization
  * Static analysis of combinatorial problems
  * Languages and systems for definition and solution of problems
  * Comparisons between systems and algorithms
  * Application experiences


WORKSHOP CHAIRS

  * Toni Mancini               Sapienza University, Rome, Italy
  * Marco Maratea              University of Genova, Genova, Italy
  * Francesco Ricca            University of Calabria, Rende, Italy


WORKSHOP PROGRAM COMMITTEE

  * Mario Alviano – Università della Calabria, Rende (Italy)
  * Laura Barbulescu – Carnegie Mellon University (CMU), Pittsburgh, PA (USA)
  * Roman Bartak – Charles University, Prague (Czech Republic)
  * Sara Bernardini – King's College London (UK)
  * Alessandro Dal Palù – Università di Parma (Italy)      
  * Francesco Donini – Università degli Studi della Tuscia, Viterbo (Italy)   
  * Wolfgang Faber – University of Huddersfield, Huddersfield (UK)
  * Andrea Formisano – Università di Perugia (Italy)
  * Marco Gavanelli – Università di Ferrara (Italy)
  * Philippe Laborie – ILOG, IBM, Gentilly (France)
  * Yuliya Lierler – University of Nebraska, Omaha, (USA)
  * Ines Lynce – Universidade Técnica de Lisboa (Portugal)
  * Joao Marques-Silva – University College Dublin (Ireland)
  * Marco Montali – Free University of Bolzano (Italy)
  * Angelo Oddi – National Research Council (CNR), Rome (Italy)
  * Andreas Pieris – University of Oxford (UK)
  * Luca Pulina – Università di Sassari (Italy)
  * Daniel Riera – Universitat Oberta de Catalunya, Barcelona (Spain)
  * Marco Roveri – FBK, Trento (Italy)
  * Francesco Scarcello – Università della Calabria, Rende (Italy)
  * Ivan Serina – Università degli Studi di Brescia (Italy)
  * Andrea Schaerf – Università di Udine (Italy)
  * Paolo Torroni – Università di Bologna (Italy)
  * Mirek Truszczynski – University of Kentucky, Lexington, KY (USA)
  * Stefan Woltran – Technische Universitat Wien (Austria)


HOST ORGANIZATION

  Vienna Summer of Logic, Vienna, Austria
  FLoC workshop affiliated with SAT 2014, ICLP 2014, IJCAR 2014


SUBMISSIONS

  Authors are invited to submit either original (full or short) papers, or papers 
  that appear on conference proceedings.

  Publications showing negative results are welcome, provided that the approach
  was original and very promising in principle, the experimentation was
  well-conducted, the results obtained were unforeseeable and gave important
  hints in the comprehension of the target problem, helping other researchers to
  avoid unsuccessful paths.

  At the time of submission, authors are requested to clearly specify whether their
  submission is original or already published.

  Workshop submissions must be in PDF format, do not exceed 15 (for full papers) or 
  8 (for short papers) pages, and should be written in LaTeX, using the LNCS-based 
  RCRA 2014 style available at the workshop web site.
  
  RCRA 2014 uses EasyChair for the submission of contributions. Details are available 
  on the web-site.

  Submissions will be reviewed by at least three members of the program committee.


SELECTION FOR THE POST-PROCEEDINGS

  Authors of papers orally presented at the workshop will have the
  opportunity to participate to the selection for the post-proceedings
  by submitting an extended version of their work.

  As in previous editions (http://rcra.aixia.it/publications), workshop
  post-proceedings will appear in a special issue of an international
  journal, provided that a sufficient amount of high quality papers is collected.

  All candidate articles must be original: they cannot have already been published
  in journals, and must contain significant additional material with respect to any
  formal publication.

  Such papers will go through a second formal selection process, and will be 
  reviewed by at least three reviewers. We aim at a short submission process, and 
  at most one re-submission stage will be allowed.
------------------------------------------------------------------------
            CALL FOR PAPERS

             QUANTIFY 2014
                --------
        1st International Workshop 
            on Quantification 

      Vienna, Austria, July 18, 2014
        http://vsl2014.at/quantify


    Affiliated to and co-located with: 

               IJCAR 2014
    Vienna, Austria, July 19-22, 2014
      http://cs.nyu.edu/ijcar2014/

       Vienna Summer of Logic 2014
           http://vsl2014.at/
------------------------------------------------------------------------

Quantifiers play an important role in language extensions of many logics. The
use of quantifiers often allows for a more succinct encoding than would be
possible without quantifiers. However, the introduction of quantifiers affects
the complexity of the extended formalism in general. Moreover, theoretical
results established for the quantifier-free formalism typically cannot be
directly transferred to the quantified case. Further, techniques successfully
implemented in reasoning tools for quantifier-free formulas cannot directly be
lifted to a quantified version.

The goal of the 1st International Workshop on Quantification (QUANTIFY 2014)
is to bring together researchers who investigate the impact of quantification
from a theoretical as well as from a practical point of view. Quantification
is a topic in different research areas such as in SAT in terms of QBF, in CSP
in terms of QCSP, in SMT, etc. This workshop has the aim to provide an
interdisciplinary forum where researchers of various fields may exchange their
experiences.

===============
IMPORTANT DATES
===============

Please follow the workshop website at http://vsl2014.at/quantify for any updates.

April 15 2014: paper submission
May    7 2014: notification of acceptance
July  18 2014: workshop 

==================
TOPICS OF INTEREST
==================

The workshop is concerned with all theoretical and practical aspects of
quantification in logics such as QBF, QCSP, SMT, and theorem proving.  The
topics of interest include (but are not limited to):

- Complexity results

- Encodings with and without quantification and comparisons thereof

- Applications of quantification  

- Implementations of reasoning tools

- Case studies and experimental results

- Intersections between the different research communities working working on
  quantification

- Surveys of state-of-the-art approaches to handling quantification

=================
PAPER SUBMISSIONS 
=================

Submissions will be managed via Easychair:

https://www.easychair.org/conferences/?conf=quantify2014

Submitted papers should be formatted in either LNCS format or a standard LaTeX
article format (paper size A4, font size 11pt).

We solicit two types of submissions:

1. Talk abstracts (maximum two pages, excluding references) describing already
published results.

2. Full papers (maximum 14 pages, excluding references) on novel, unpublished
work.

The talk abstracts of category 1 should include a relevant bibliography of
related work and an outline of the planned talk. For this category, we
explicitly advocate talks which survey results already published, maybe in
multiple articles or presentations capturing the commonalities and differences
of various quantification approaches (perhaps even interdisciplinary).

Please see the workshop website for further submission guidelines:

http://vsl2014.at/quantify

===================
WORKSHOP ORGANIZERS
===================

Hubie Chen
Universidad del País Vasco and Ikerbasque, Donostia-San Sebastián, Spain

Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl           
Johannes Kepler University Linz, Austria 

=================
PROGRAM COMMITTEE
=================

Albert Atserias (Universitat Politecnica de Catalunya)
Nikolaj Bjorner (Microsoft Research)
Mikolas Janota (INESC-ID Lisboa)
Hans Kleine Büning (University of Paderborn)
Konstantin Korovin (Manchester University)
Laura Kovacs (Chalmers University of Technology)
Francesco Scarcello (DIMES, University of Calabria)
Christoph M. Wintersteiger (Microsoft Research)

The ISQED Microelectronics Olympiad is an educational contest intended to spotlight engineering students and young engineers active in the field of microelectronics. The Olympiad consists of a written test covering a variety of topics related to digital and analog circuit design. The competition will take place during the ISQED-China event on Oct. 27th in Hangzhou, China.Topics included in the Olympiad:

  • Digital IC Design and Testing
  • Analog and Mixed Signal IC Design and Testing
  • Semiconductor Devices and Technology
  • Mathematical and Algorithmic Issues of EDA

The top ranking participants of the ASQED Microelectronics Olympiad will receive an award from ISQED and all registered attendees who complete the full test will receive a certificate of participation. The first place winner will also have the option to participate in an advanced competition at the International Microelectronics Olympiad in Armenia, where all his/her travel expenses will be paid by the Armenia Olympiad Committee.

A summer internship position is available for 2014 in the "AI for Optimization" group within the newly formed Cognitive Algorithms department at IBM Watson Research Center, Yorktown Heights, New York. The internship will last for about 3 months and will be scheduled between March and October, 2014.

Candidates should be exceptional Masters or PhD students in Computer Science and related areas, and not have already received their PhD by the internship start date. The successful candidate is expected to have strong interest and some experience in one or both of the following:

  • Advancing Black-Box / Simulation-Based Optimization approaches to solve real-world problems and/or to improve optimization methods themselves by, e.g., employing techniques from Machine Learning, Local Search, Constraint Reasoning, and Genetic Algorithms for automated algorithm selection and parameter tuning.
  • Exploring novel approaches to advance Machine Learning methods such as Deep Learning by, e.g., training and building Neural Networks using approaches from constraint reasoning and discrete, continuous, and black-box optimization.

Interested candidates should send their CV as well as names and contact information of at least two references to all of the following:

  • Ashish Sabharwal [ashish.sabharwal@us.ibm.com]
  • Horst Samulowitz [samulowitz@us.ibm.com]
  • Meinolf Sellmann [meinolf@us.ibm.com]

CSPSAT 2014: CALL FOR PAPERS 
CSPSAT 2014 – Fourth International Workshop on the Cross-Fertilization Between CSP and SAT 
In conjunction with SAT 2014
July 18, 2014 · Vienna, Austria
 

 

Important Dates
Deadline for abstract submissions	April 20, 2014
Deadline for paper submissions	April 27, 2014
Notifications to authors	May 18, 2014
Camera-ready copy submission	May 28, 2014



Aims and Scope

Constraint Satisfaction Problems (CSPs) and Boolean Satisfiability Problems (SAT) have much in common. 
However, they also differ in many important aspects. Algorithmic techniques such as local search and 
propagation-based search have been applied in both areas, but with major differences in the underlying 
algorithmic design and in specific heuristics. Recently, the success of lazy clause-generating solvers 
has drawn significant attention, and can serve as one example of how the interaction between the two 
frameworks can advance the fields. Similarly, the comparative theoretical study of CSP and SAT is of 
great interest with a potential for many exciting results. The CSP and SAT communities, while to a 
large extent interacting with each other, are still mostly separate communities with separate conferences 
and meetings. This workshop is designed as a venue for bridging this gap, and enhancing cross-fertilization 
between the two communities, in terms of problems, ideas, techniques, and results. 

This year's workshop is the fourth in the series, following successful occasions in SAT'11, SAT'12, and 
CP'13.  We plan to continue to alternate this workshop between the CP and SAT conferences in order to better 
facilitate the purpose of cross-fertilization. As in previous years, the workshop is expected to consist of 
peer-reviewed contributed papers, an invited talk, a tutorial, and ample time for informal interaction. 

Topics in the scope of the workshop include: 

Adaptation of CSP techniques to SAT problems.
Adaptation of SAT techniques to CSP's.
Efficient translations and encodings from one framework to the other, including SAT encodings of global constraints.
Consistency criteria of SAT encodings.
Lazy clause generation encodings and techniques.
Heterogeneous CSP/SAT problems.
Hybrid CSP/SAT solvers.
Local search in CSP and SAT.
Parallelization and real-time competition between CSP and SAT solvers, cross-talk between the solvers.
Commonalities and differences in the theory of CSP and SAT solving.
Intermediate problems (e.g., satisfiability modulo theories, pseudo-Boolean) and their relations to both CSP and SAT.
Applications: ways to determine which framework works best for which application.
Preprocessing techniques.
Restart methods.
Additional related topics. 

Paper Submissions
Authors should prepare their papers in the LNCS/LNAI format, following Springer's instructions. Submissions can 
be of one of the following types:

Full papers, maximum of 15 pages excluding references.
Short papers, maximum of 5 pages excluding references.
Authors should indicate whether the submitted work has been published or accepted for publication elsewhere. 
Priority will be given to original full papers and to important work recently presented in other venues. Each 
submission should identify one contact author, and provide the email address and phone number of this author. 
Papers and abstracts should be submitted via EasyChair:
https://www.easychair.org/conferences/?conf=cspsat2014

All submissions will be reviewed by at least two members of the program committee or their delegates. Decisions 
about acceptance or rejection will be made considering both the merit of the work and the available time for 
presentations. At least one author of each accepted submission must attend the workshop. Original papers will 
be published on the workshop website following the workshop.

Program Committee

Yael Ben-Haim (IBM Research) - chair
Nadia Creignou (Aix-Marseille Université)
Alan Frisch (University of York)
Enrico Giunchiglia (DIST - Univ. Genova)
George Katsirelos (INRA, Toulouse)
Valentin Mayer-Eichberger (NICTA and University of New South Wales) - chair
Ian Miguel (University of St Andrews)
Nina Narodytska (University of Toronto and University of New South Wales)
Yehuda Naveh (IBM) - chair
Steve Prestwich (Cork Constraint Computation Centre)
Vadim Ryvchin (Technion)
Meinolf Sellmann (IBM Research)
Bart Selman (Cornell University)
Ofer Strichman (Technion)
Toby Walsh (NICTA and UNSW)
                    
------------------------------------------------------------------------
            CALL FOR PAPERS

                QBF 2014
                --------
       2nd International Workshop on 
        Quantified Boolean Formulas 

      Vienna, Austria, July 13, 2014
        http://vsl2014.at/qbf


    Affiliated to and co-located with: 

          SAT 2014 conference
    Vienna, Austria, July 14-17, 2014
      http://baldur.iti.kit.edu/sat2014/

        Vienna Summer of Logic 2014
            http://vsl2014.at/
------------------------------------------------------------------------

The goal of the Second International Workshop on Quantified Boolean Formulas
(QBF 2014) is to bring together researchers working on theoretical and
practical aspects of QBF solving and applications. In addition to that, it
addresses (potential) users of QBF in order to reflect on the state-of-the-art
and to consolidate on immediate and long-term research challenges.

The QBF workshop 2014 is a follow-up edition of the QBF workshop which was
held in 2013 in the context of the SAT conference in Helsinki, Finland. The
first edition of the workshop in 2013 was attended by 40 participants, which
demonstrates the renewed interest in QBF across different research fields.

The QBF Workshop 2014 will include a presentation of the QBF Gallery 2014, a
competitive evaluation of QBF solvers and related tools:

http://qbf.satisfiability.org/gallery/

===============
IMPORTANT DATES
===============

Please follow the workshop website at http://vsl2014.at/qbf for any updates.

April 15 2014: submission of extended abstracts
April 30 2014: notification of acceptance
July  13 2014: workshop 

==================
TOPICS OF INTEREST
==================

The workshop is concerned with all aspects of current research on QBF.  The
topics of interest include (but are not limited to):

- QBF applications, encodings, and benchmarks  

- Applications of QBF in other formalisms which use quantifiers such as
  quantified constraint satisfaction problems (QCSP) or Satisfiability Modulo
  Theories (SMT)

- Case studies and experimental evaluations

- Certificates and proofs for QBF

- Formats of proofs and certificates

- Implementations of proof checkers and verifiers 

- Decision procedures for QBF

- Calculi for QBF

- Data structures, implementation details, and heuristics

- Pre- and inprocessing techniques 

- Structural QBF solving

================================
SUBMISSION OF EXTENDED ABSTRACTS
================================

Submitted extended abstracts should have a maximum overall length of 4 pages
in either LNCS format or a standard LaTeX article format (paper size A4, font
size 11pt) excluding references.

Please see the workshop website for further submission guidelines:

http://vsl2014.at/qbf

===============
WORKSHOP REPORT
===============

Accepted extended abstracts are collected in an informal report which will be
publicly available at the workshop's website.

===================
WORKSHOP ORGANIZERS
===================

Charles Jordan
Hokkaido University, Sapporo, Japan

Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl           
Johannes Kepler University Linz, Austria 
                    
The Logical Mind: Connecting Foundations and Technology Competition
(Organized by the Kurt Gödel Society)
The Kurt Gödel Society is proud to announce the commencement of the Kurt Gödel Research Prize Fellowships Program-
The Logical Mind: Connecting Foundations and Technology.

A.	The program has a particular emphasis on supporting young scholars as previous rounds of Kurt Gödel
Research Prize Fellowships showed that the impact on the careers of the young researchers had the most significance.
Young scholars are defined by being less or exactly 40 years old at the time of the commencement of the
Vienna Summer of Logic (July 9, 2014)!
The program will offer:
One fellowship award in the amount of EUR 100,000, in each of the following categories:
•	Logical Foundations of Mathematics,
•	Logical Foundations of Computer Science and
•	Logical Foundations of Artificial Intelligence
B.	The awards will be based on a categorized world-wide open competition by way of submission of up to
three-pages project description, CV and two letters of recommendation.
C.	The applicant will have to choose an applicable category him/herself.
D.	The following three Boards of Jurors will choose four finalists from their respective discipline
electronically:
Logical Foundations of Mathematics: Harvey Friedman (Chair),  Angus Macintyre, and Dana Scott.
Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas  (Chair).
Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel
The winners will be chosen by all three juries together.
The finalists will be invited to submit an extended project proposal version electronically before the
Vienna Summer of Logic and only the finalists shall be entitled to reviewer’s feedback.
E.	Finalists will be obliged to submit a full version of their proposal (up to 20 pages)
F.	All deliberations will be performed electronically. The same shall apply to all decisions
G.	All finalists except for the winners will receive silver medals and certificates per post.
H.	Gold medals will be awarded to the winners at the ceremony held in the Celebration Hall of
the Vienna University of Technology together with silver medals for the winners of fifteen major
competitions related to the conceptual progress in computer science.
I.	The winners will be obliged to write an article for publication in the book
containing planned contributions from the winners of all fellowships rounds organized
by the Kurt Gödel Society with support of the John Templeton Foundation.

Timeline
March 2, 2014 (midnight PST): Proposals submission deadline
March 31, 2014: Jury decision on finalists due
May 30, 2014: Full proposals due
June 20, 2014: Jury decision on winners due
July 17, 2014: Foundations and Technology Competitions Award Ceremony
August 1, 2014: Commencement of the fellowship
July 31, 2016: End of the fellowships program
=====================================================================
=                             28/01/2014                            =
=                    ONERA -- CENTRE DE TOULOUSE                    =
=          Information Processing and Modeling Department           =
=             Permanent Research Engineer Position                  =
=                          in the field of                          =
=         Formal Verification for Critical Embedded Software        =
=====================================================================


1) Position description:
========================

You are part of the LAPS research unit (Languages, Architectures and
Proofs for embedded Systems). This team is conducting research on
methods, techniques and tools for the development and verification of
aerospace embedded systems.

You contribute to research work on design and verification methods and
techniques for critical embedded software. The long term objective of
this work is the definition and implementation of a compilation and
verification chain for critical embedded software systems, more
specifically for avionics flight control systems and fault tolerant
systems (control algorithms, filtering algorithms, fault detection and
reconfiguration algorithms, ...).

This code generation chain will in particular allow the specification
of safety-related invariants and the verification/preservation of
these invariants at the implementation level. The verification will
use a combination of different state of the art formal techniques
(cf. section 2 below).

Your activity consists in:

- defining innovative verification techniques at model level
  (synchronous languages, software architectures) and at code level
  (ANSI C);
- prototyping tools implementing these techniques, making the best use
  of state-of-the-art verification engines;
- applying the proposed approaches to industrial case studies.

The research is conducted through collaborative projects involving
industrial partners (Airbus, Thalès, Astrium, Dassault Aviation...),
as well as european research labs.

2) Applicant Profile:
=====================

The candidate must hold a PhD in computer science. Expertise one of
the following verification techniques is also required:

- abstract interpretation;
- numerical optimization;
- SAT/SMT-based model checking (BMC, induction, property-directed
  reachability);
- mixed-theory quantifier elimination;
- invariant generation (quantifier elimination, template based,
  heuristics based);
- SAT/SMT-based synthesis.

Previous knowledge and experience with synchronous data-flow languages
(Scade, Lustre, Simulink) is highly appreciated.

3) Miscellaneous info. (spoken language, etc.):
===============================================

Applicants must have a good English level, French is *not* a
requirement as long as English is OK.

4) Application process:
=======================
The reference to indicate in all application documents is N°TIS/DTIM/LAPS/CDI/001791.
 
Applicants must upload their CV and motivation letter through the ONERA website at
http://www.onera.fr/fr/emploi-et-formation/offres-emploi

where the offer is labeled as follows:

Title:
"INGENIEUR DE RECHERCHE VERIFICATION FORMELLE DE LOGICIELS EMBARQUES H/F"
Domain: 
"Commande des systèmes | Développement informatique | Systèmes | Traitement de l'information"
                                    

Submission deadline: April 30, 2014

The workshop on Boolean problems has an emphasis on the problems related to the solution of all kinds of high-dimension Boolean and discrete problems, and provides a forum for researchers and engineers from different disciplines to exchange ideas. The workshop is devoted to theoretical discoveries as well as practical applications. An aim of the workshop is to initiate possible collaborative research and to find new areas of application. It is intended to publish the papers in proceedings. The invited speakers are:
- Mitch Thornton (SMU Dallas (Texas), USA),
- Jaap van den Herik (Tilburg University, Netherlands), and
- Shinobu Nagayama (Hiroshima City University, Japan)
are presenting essential results of their research.

Topics of interest (not limited to):
- Theory
- Properties and applications of Boolean Algebras
- Data Structures and Algorithms
- Modeling
- Specification of data structures/Algorithms
- Complexity
- Program Systems/Software
- Fundamental software for the solution of Boolean Problems
- Comparison of efficiency
- Practical Applications
- Application of Boolean Algebra in FPGA synthesis
- Quantum logic, reversible logic, and multi-valued logic
- Solution of real-world problems

Submissions

To submit a paper, please send an extended abstract, as a PDF file no longer than 6 pages using the workshop web page

http://www.informatik.tu-freiberg.de/prof2/ws_bp11/

or send a PDF file to: iwsbp2014@informatik.tu-freiberg.de

by April 30, 2014. Acceptance notices will be sent by June 6, 2014. The final version of the paper should be submitted by July 6, 2014.
The Ph.D. Forum at the Design Automation Conference is a poster session hosted by SIGDA for Ph.D. students to to present an discuss their dissertation research with people in the EDA community. It has become one of the premier forums for Ph.D. students in design automation to get feedback on their research and for industry to see academic work in progress: 400 - 500 people attended the last forums. Participation in the forum is competitive with acceptance rate of around 30%. Limited funds will be available for travel assistance, based on financial needs. The forum is open to all members of the design automation community and is free-of-charge. It is co-located with DAC to attract the large DAC audience, but DAC registration is not required in order to attend this event.

Eligibility
- Students with at least one published or accepted conference, symposium or journal paper.
- Students within 1-2 years of dissertation completion and students who have completed their dissertation during the 2011-2012 academic year.
- Dissertation topic must be relevant to the DAC community.
- Previous forum presenters are not eligible.
- Students who have presented previously at the DATE and ASP-DAC Ph.D. forums are eligible, but will be less likely to receive travel assistance.

Important Dates
- Submission Deadline: March 30. 2014
- Submission Link: http://www.easychair.org/conferences/?conf=daforum14
- Notification Date: April 25, 2014
- Forum Presentation: TBA

Submission Requirements
- A two-page PDF abstract of the dissertation (in two-column format, using 10-11 pt. fonts and single-spaced lines), including name, institution, adviser, contact information, estimated (or actual) graduation date, whether the work has been presented at ASP-DAC Ph.D. Forum or DATE PhD Forum, as well as figures, and bibliography (if applicable). The two-page limit on the abstract will be strictly enforced: any material beyond the second page will be truncated before sending to the reviewers. Please include a description of the supporting paper, including the publication forum. A list of all papers authored or co-authored by the student, related to the dissertation topic and included in the two-page abstract, will strengthen the submission.
- A published (or accepted) paper, in support of the submitted dissertation abstract. The paper must be related to the dissertation topic and the publication forum must have a valid ISBN number. It will be helpful, but is not required, to include your name and the publication forum on the first page of the paper. Papers on topics unrelated to the dissertation abstract or not yet accepted will not be considered during the review process.
========================================================================
   ==================================================================

              Fifth Answer Set Programming Competition 2014

                     Call for Participant Systems

     Aalto University, University of Calabria, University of Genova

                         Spring/Summer 2014

                https://www.mat.unical.it/aspcomp2014

                      aspcomp2014@mat.unical.it

   ==================================================================

Special edition of the ASP Competition series -system track- part of the
Olympic Games (http://vsl2014.at/olympics/) of the Vienna Summer of Logic 
2014 (http://vsl2014.at/).

 == Important Dates ==

 * March 1st, 2014: Participant registration opens

 * March 31st, 2014: The competition starts

 * July 2014: Awards are presented at FLoC (22nd) and at ICLP (19th-22nd)

========================================================================

Answer Set Programming (ASP) is a well-established paradigm of declarative
programming with close relationship to other declarative modeling
paradigms and languages, such as SAT Modulo Theories, Constraint Handling
Rules, FO(.), PDDL, CASC, and many others.

[...]

As anticipated during the 2013 presentation, in order to join the Vienna
Summer of Logic, which is expected to be the largest event in the history
of logic, ASP Competition departs, this year, from the "usual" timeline,
and the Fifth ASP Competition will be run in the first half of 2014, 
jointly at Aalto University (Finland), University of Calabria (Italy) and
University of Genova (Italy). The event is affiliated with the 30th
International Conference on Logic Programming (ICLP).  [...]

== Call for Participant Systems ==

[...]

The competition consists of a System Track (as called in past 
competitions), which compares dedicated solvers on ASP benchmarks.
Participants compete with solving systems for the ASP-Core-2 language.
Some more details are given in the following:

- The benchmark domains are taken from past editions.

- Systems of the 2013 edition will be considered. (Developers will have
  the chance of submitting up-to-date versions of their solvers.)

- Submissions of new solvers are encouraged.

The competition will not be limited to sub-tracks based on
"complexity" of problems (as in past events), but rather will take
into consideration language features: sub-tracks will range from a
basic language, to (by adding features such as aggregates and choice
rules) to the ASP-Core-2 language.  The aim is to clearly indicate what
(combinations of) techniques work for a particular (set of)
feature(s), and also widening the participation to teams that cannot
(yet) support the full standard.  The final sub-track design will depend
on the availability of benchmarks as well as systems.  Participants are
encouraged to inform us about any limitations or requirements of their
systems so that we can take them into account in the sub-track design.

We welcome the submission of parallel and portfolio systems making use of
multiple cores or multiple algorithms for solving the given instances.
These solvers will have dedicated tracks, assuming a sufficient number of
submissions in each track.  Of course, we also welcome the submission of
any kind of solvers, e.g., SAT solvers, SMT solvers, CP systems, FOL
theorem provers, Description Logics reasoners, Planning reasoners, or any
other that can be adapted/applied to the evaluation of logic programs
encoded in ASP-Core-2.

[...]

For further information and submission instructions please visit the
competition web site

            https://www.mat.unical.it/aspcomp2014

or contact us by email: aspcomp2014@mat.unical.it
                                    

=============================================================

First Call For Papers JELIA 2014

14th European Conference on Logics in Artificial Intelligence

Madeira Island, Portugal September 24-26, 2014

http://www.uma.pt/jelia2014

Submission Deadline: May 19 (Abstracts); May 23 (Papers)

=============================================================

================ Aims and Scope ================

The aim of JELIA 2014 is to bring together active researchers interested in all aspects concerning the use of logics in Artificial Intelligence to discuss current research, results, problems, and applications of both theoretical and practical nature. JELIA strives to foster links and facilitate cross- fertilization of ideas among researchers from various disciplines, among researchers from academia and industry, and between theoreticians and practitioners.

Authors are invited to submit papers presenting original and unpublished research in all areas related to the use of logics in Artificial Intelligence including: * Abductive and inductive reasoning * Answer set programming * Applications of logic-based AI systems * Argumentation systems * Automated reasoning including satisfiability checking and its extensions * Computational complexity and expressiveness * Deontic logic and normative systems * Description logics and other logical approaches to semantic web and ontologies * Knowledge representation, reasoning, and compilation * Logic-based data access and integration * Logic programming and constraint programming * Logics for uncertain and probabilistic reasoning * Logics in machine learning * Logics in multi-agent systems, games, and social choice * Non-classical logics, such as modal, temporal, epistemic, dynamic, spatial, paraconsistent, and hybrid logics * Planning and diagnosis based on logic * Preferences * Reasoning about actions and causality * Updates, belief revision and nonmonotonic reasoning

================ Paper Submission ================

There are two categories for submissions:

A. Regular papers Submissions should contain original research, and sufficient detail to assess the merits and relevance of the contribution. Submissions must not have been previously published or be simultaneously submitted for publication elsewhere.

B. System descriptions Submissions should describe an implemented system and its application area(s). A demonstration is expected to accompany a system presentation. Papers describing systems that have already been presented in JELIA before will be accepted only if significant and clear enhancements to the system are reported and implemented.

All submissions should not exceed 13 pages including figures etc., but excluding references. All submissions should be written in English, and should be formatted according to the standard Springer LNCS style. The proceedings of JELIA 2014 are published by Springer-Verlag in the Lecture Notes in Artificial Intelligence, a sub-series of Lecture Notes in Computer Science (Important note: Springer will require all the LaTeX source files of all accepted submissions).

================ Important Dates ================

Abstract submission deadline: May 19, 2014

Paper submission deadline: May 23, 2014

Author Rebuttal: June 26-27, 2014

Notification of acceptance: July 4, 2014

Final versions due: July 18, 2014

================ Contact address ================

jelia2014@easychair.org

The Formal Methods, Computational Intelligence and Constraint Programming for Software Assurance Workshop (FMCICA 2014) will be co-located with the 14th International Conference on Computational Science and Its Applications (ICCSA 2014) will be held on June 30 - July 3, 2014, in Guimaraes, Portugal.
The Department of Science & Technology (DST), Govt. of India and the State Committee on Science & Technology of the Government of Belarus (SCST), Invite proposals for Joint Research projects and Workshops in bilateral mode involving scientists & technologists from India and Belarus. Deadline to submit proposal is March 31, 2014. Duration is for 2 years. Researchers interested for proposal submission in the area of Algorithms for Satisfiability (SAT) solving, contact Dr Ateet Bhalla (bhalla.ateet@gmail.com)
Encode integer factorization as a SAT problem. Create unsolvable (UNSAT) problems by encoding a prime number. Easily control the difficulty of satisfiable problems by encoding larger numbers with fewer factors (that are also larger).
Appel à communications : JFPC 2014
Dixièmes Journées Francophones de Programmation par Contraintes, LERIA, Université d'Angers (UFR Sciences).

http://jfpc-jiaf2014.univ-angers.fr/jfpc

Congrès à l'initiative de l'Association Française de Programmation par Contraintes (AFPC) : http://www.afpc-asso.org/

Les JFPC sont le principal congrès de la communauté francophone travaillant sur les problèmes de satisfaction de contraintes (CSP) / programmation par contraintes (PPC), le problème de la satisfiabilité d'une formule logique propositionnelle (SAT) et / ou la programmation logique avec contraintes (CLP). La communauté de programmation par contraintes entretient également des liens avec la recherche opérationnelle (RO),  l'analyse par intervalles, et différents domaines de l'intelligence artificielle.

Les JFPC 2014 sont organisées conjointement avec les JIAF 2014 (Journées de l'Intelligence Artificielle Fondamentale)

Dates importantes :

* 24 février 2014 : date limite d'envoi des résumés d'articles
* 3 mars 2014 : date limite de soumission des articles complets longs (10p.) et courts (4p.)
* 11 avril 2014 : notification aux auteurs
* 28 avril 2014 : version définitive en français
* du 11 au 13 juin 2014 : JFPC 2014

Les soumissions peuvent être faites sous forme d'article long ou court. Les articles longs ne doivent pas dépasser 10 pages dans le style de la conférence. Les articles courts sont limités à 4 pages.

Lien pour les soumissions : https://www.easychair.org/conferences/?conf=jfpc2014

Président du comité de programme :
Thierry Petit, LINA, Mines de Nantes, France
Thierry.Petit@mines-nantes.fr

Président du comité d'organisation :
Frédéric Lardeux, LERIA, Université d'Angers, France
jfpc_jiaf_2014@contact.univ-angers.fr