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 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