posted by user: mseidl || 2319 views || tracked by 5 users: [display]

QBF 2013 : International Workshop on Quantified Boolean Formulas


When Jul 9, 2013 - Jul 9, 2013
Where Helsinki
Submission Deadline Apr 24, 2013
Notification Due May 20, 2013
Final Version Due Mar 6, 2014
Categories    computer science

Call For Papers


QBF 2013
International Workshop on
Quantified Boolean Formulas

Helsinki, Finland, July 9, 2013

Affiliated to and co-located with:
SAT 2013 conference
Helsinki, Finland, July 8-12, 2013

Quantified Boolean formulas (QBF) are an extension of propositional
logic which allows for explicit quantification over propositional
variables. The decision problem of QBF is PSPACE-complete compared to
NP-completeness of the decision problem of propositional logic (SAT).

Many problems from application domains such as model checking, formal
verification or synthesis are PSPACE-complete, and hence could be
encoded in QBF. Considerable progress has been made in QBF solving
throughout the past years. However, in contrast to SAT, QBF is not
widely applied to practical problems in industrial settings. For
example, the extraction and validation of models of (un)satisfiability
of QBFs and has turned out to be challenging.

The goal of the International Workshop on Quantified Boolean Formulas
(QBF 2013) is to bring together researchers working on theoretical and
practical aspects of QBF solving. 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.

As the efforts of extending languages with quantifiers have not only be
made for propositional logic in terms of QBFs, but in many other
formalism like Constraint Satisfaction Problem (CSP) and Satisfiability
Modulo Theories (SMT), QBF 2013 also targets researchers working in
these fields in order to exchange experiences and ideas.


Please follow for any updates.

April 24 2013: paper submission
May 20 2013: notification of acceptance
June 15 2013: camera-ready version of papers
July 9 2013: workshop


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

- QBF applications, encodings and benchmarks
- 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
- Quantifiers in other formalisms like SMT or CSP
- Tools related to any aspect of QBF/CSP/SMT reasoning


Submissions of extended abstracts are solicited and will be managed via

Submitted extended abstracts should have an overall length of 4 pages in
LNCS format excluding references. Authors may decide to include an
appendix with additional material. Appendices will be considered at the
reviewers' discretion.

Submissions related to completed work as well as work in progress are
welcome. Submissions will be reviewed with respect to novelty,
originality and scope. Authors are encouraged to provide additional
material such as source code of tools, experimental data, benchmarks and
related publications.

Submissions which describe novel applications of QBF in various domains
are particularly welcome. Additionally, this call comprises known
applications which have been shown to be hard for QBF solvers in the
past as well as new applications for which present QBF solvers might
lack certain features still to be identified. Reports on ongoing
research are particularly welcome.

Previously published work or extensions thereof may be submitted to the
workshop but that case has to be explicitly stated in the extended
abstract. This regulation also applies to work which is currently under
review elsewhere.

Since the workshop does not have official proceedings, work related to
accepted submissions can be resubmitted to other venues without

Authors of accepted extended abstracts are expected to give a talk at
the workshop.


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


Florian Lonsing
Vienna University of Technology, Austria

Martina Seidl
Johannes Kepler University Linz, Austria


Fahiem Bacchus
Armin Biere
Nikolaj Björner
Uwe Bubeck
Hans Kleine Büning
Hubie Chen
Nadia Creignou
Uwe Egly
Allen Van Gelder
Enrico Giunchiglia
Mikoláš Janota
Massimo Narizzano
Stefan Szeider

Related Resources

IEEE Xplore-Ei/Scopus-CSPIT 2023   2023 Asia Conference on Communications, Signal Processing and Information Technology (CSPIT 2023) -EI Compendex
IEEE Xplore-Ei/Scopus-DMCSE 2023   2023 International Conference on Data Mining, Computing and Software Engineering (DMCSE 2023) -EI Compendex
IEEE Xplore-Ei/Scopus-CACEE 2023   2023 International Conference on Automation, Control and Electronics Engineering (CACEE 2023) -EI Compendex
ICDM 2024   24th Industrial Conference on Data Mining
IEEE Xplore-Ei/Scopus-AICME 2023   2023 International Conference on Artificial Intelligence, Communications and Mechatronics (AICME 2023) -EI Compendex
ECCSIT 2023   2023 European Conference on Computer Science and Information Technology (ECCSIT 2023)
IEEE ICA 2022   The 6th IEEE International Conference on Agents
SDMPR 2023   2023 Asia Conference on Statistics, Data Mining and Pattern Recognition (SDMPR 2023)
ICSC 2024   IEEE International Conference on Semantic Computing
NLDML 2024   3rd International Conference on NLP, Data Mining and Machine Learning