 |
Welcome to SAT Live!
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 Learningi 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.
You can take a look at all the current links,
see the links classified by keywords or add your
own reference (you must be subscribed to SAT Live! or propose it as
anonymous).
If you don't have some links to propose for now
but would like email notification of new additions to the repository,
you can subscribe to the SAT Live!
notification list or register to the site RSS feed (courtesy of Christian Muise, using Dapper).
Finally, a page with some
people interested by the SATisfaction problem is also available.
Last 10 new entries
832 elements available | | SECOND CALL FOR PARTICIPATION
Third International SAT/SMT Summer School
Aalto University, Otaniemi Campus
Espoo, Finland, July 3-5th, 2013
http://satsmt2013.ics.aalto.fi/
REGISTRATION:
The registration deadline for the school is May 20, 2013. Full
details of the registration procedure are available at the school
website (http://satsmt2013.ics.aalto.fi/).
ABOUT:
The SAT/SMT Summer School aims at providing graduate students and
researchers from universities and industry with a comprehensive
overview of research and methodology in satisfiability testing (SAT)
and satisfiability modulo theories (SMT). The lectures cover the
foundational and practical aspects of SAT and SMT technologies and
their applications.
The third edition follows the schools that took place at MIT (SAT/SMT
Solver Summer School 2011) and at Fondazione Bruno Kessler (SAT/SMT
School 2012) in Trento, Italy. The 16th International Conference on
Theory and Applications of Satisfiability Testing (SAT 2013) is
arranged at University of Helsinki the following week (see
http://sat2013.cs.helsinki.fi/).
The 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:
Proof Complexity by
Olaf Beyersdorff, University of Leeds, United Kingdom
Applications of SMT Solvers by
Alessandro Cimatti, IRST, Trento, Italy
Internals of Modern SMT Solvers by
Leonardo de Moura, Microsoft Research, Redmond, USA
Foundations and Theoretical Aspects of SAT by
John Franco, University of Cincinnati, USA
SAT-Based Planning by
Enrico Giunchiglia, University of Genoa, Italy
Preprocessing by
Marijn Heule, University of Texas at Austin, USA
CDCL SAT Solvers and SAT-Based Problem Solving by
Joao Marques-Silva, University College Dublin, Ireland
SMT Theory and DPLL(T) by
Albert Oliveras, Technical University of Catalonia, Barcelona, Spain
Modelling and Solving in Answer Set Programming by
Torsten Schaub, Potsdam University, Germany
Parametrized Complexity by
Stefan Szeider, Vienna University of Technology, Austria
A more detailed program is available at the school website
(http://satsmt2013.ics.aalto.fi/).
Organizing committee:
Keijo Heljanko, Aalto University,
Tomi Janhunen, Aalto University, and
Matti Jarvisalo, University of Helsinki.
|
| |  | |  |
|  | |
 | |
SAT 2013 Preliminary Conference Program
16th International Conference on Theory and Applications of
Satisfiability Testing
July 8-12, 2013, Helsinki, Finland
Registration (early registration deadline May 27)
http://sat2013.cs.helsinki.fi/registration.html
Program updates:
http://sat2013.cs.helsinki.fi/program.html
-----------------------------------------------------------------------------
MONDAY July 8
9:00-17:00: Workshops
SMT 2013: 11th International Workshop on Satisfiability Modulo Theories
PoS 2013: 4th International Workshop on Pragmatics of SAT
Breaks:
10:30-11:00 Coffee
12:30-14:00 Lunch
15:00-15:30 Coffee
--------------
TUESDAY July 9
9:00-12:30: Workshops
SMT 2013: 11th International Workshop on Satisfiability Modulo Theories
QBF 2013: International Workshop on Quantified Boolean Formulas
12:30-14:00 Lunch (only to participants with a full conference registration)
14:00-14:20 Welcome, best paper announcement
14:20-15:20 Invited talk: Albert Atserias
"The Proof-Search Problem between Bounded-Width Resolution and
Bounded-Degree Semi-Algebraic Proofs"
15:20-15:50 Coffee
15:50-16:50 Propositional Proof Complexity I
-Exponential Separations in a Hierarchy of Clause Learning Proof Systems
-The Complexity of Theorem Proving in Autoepistemic Logic
Social program: Welcome Reception
-----------------
WEDNESDAY July 10
9:00-10:30 Quantified Boolean Formulas
-On Propositional QBF Expansions and Q-Resolution
-Recovering and Utilizing Partial Duality in QBF
-Efficient Clause Learning for Quantified Boolean Formulas via
QBF Pseudo Unit Propagation
10:30-11:00 Coffee
11:00-12:30 Parallel Solving
-Soundness of Inprocessing in Clause Sharing SAT Solvers
-Concurrent Clause Strengthening
-Parallel MUS Extraction
12:20-14:00 Lunch
14:00-15:00 Invited talk: Edmund M. Clarke
"Turing's Computable Real Numbers and Why They Are
Still Important Today"
15:00-15:30 Coffee
15:30-16:50 Maximum Satisfiability
-A Modular Approach to MaxSAT Modulo Theories
-Exploiting the Power of MIPs Solvers in Maxsat
-Community-based Partitioning for MaxSAT Solving
General Assembly of the SAT Association (open to all conference participants)
----------------
THURSDAY July 11
9:00-10:30 Encodings and Applications
-Experiments with Reduction Finding
-A Constraint Satisfaction Approach for Programmable Logic Detailed Placement
-Minimizing Models for Tseitin-Encoded SAT Instances
10:30-11:00 Coffee
11:00-12:30 Beyond SAT
-Solutions for Hard and Soft Constraints Using Optimized
Probabilistic Satisfiability
-Quantified Maximum Satisfiability: A Core-Guided Approach
-Nested Boolean Functions as Models for Quantified Boolean Formulas
12:30-14:00 Lunch
14:00-15:00 Invited talk: Peter Stuckey
"There Are No CNF Problems"
15:00-15:30 Coffee
15:30-16:50 Solver Techniques and Analysis
-Factoring Out Assumptions to Speed Up MUS Extraction
-On the Interpolation between Product-Based Message Passing Heuristics for SAT
-Improving Glucose for Incremental SAT Solving with Assumptions:
Application to MUS Extraction
Social Program: Conference Banquet
--------------
FRIDAY July 12
9:00-9:30 Tool paper presentations
9:30-10:30 Competition Overviews
10:30-11:30 Combined tool demo and poster session, coffee
11:30-12:30 Clique-Width and SAT
-A SAT Approach to Clique-Width
-Cliquewidth and Knowledge Compilation
12:30-14:00 Lunch
14:00-15:00 Propositional Proof Complexity II
-A Rank Lower Bound for Cutting Planes Proofs of Ramsey's Theorem
-On the Resolution Complexity of Graph Non-Isomorphism
*** Note: no break here ***
15:00-15:50 Parameterized Complexity
-Local Backbones
-Upper and Lower Bounds for Weak Backdoor Set Detection
15:50: Closing Ceremony, Drinks
|
| |  | |  |
|  | |
 | |
[ We apologize if you receive multiple copies of this call. ]
-------------------------------------------------------------------------
CALL FOR PARTICIPATION
Sixteenth International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
--- SAT 2013 ---
Helsinki, Finland, July 8-12, 2013
http://sat2013.cs.helsinki.fi/
Registration to SAT 2013 is now open at
http://sat2013.cs.helsinki.fi/registration.html
Early registration deadline: May 27, 2013
-------------------------------------------------------------------------
SAT 2013 CONFERENCE HIGHLIGHTS
==============================
-Three high-quality INVITED TALKS:
+Albert Atserias:
"The Proof-Search Problem between Bounded-Width Resolution and
Bounded-Degree Semi-Algebraic Proofs"
+Edmund M. Clarke:
"Turing's Computable Real Numbers and Why They Are Still Important Today"
+Peter Stuckey:
"There are no CNF problems"
-Around 30 SCIENTIFIC TALKS on SAT 2013 accepted papers, see full list at
http://sat2013.cs.helsinki.fi/accepted.html
-WORKSHOPS:
SMT 2013: 1th International Workshop on Satisfiability Modulo Theories
PoS 2013: 4th International Workshop on Pragmatics of SAT
QBF 2013: International Workshop on Quantified Boolean Formulas
-COMPETITIONS AND SYSTEM EVALUATIONS:
SAT Competition 2013
Configurable SAT Solver Challenge 2013
Max-SAT Evaluation 2013
SMT-EVAL 2013
QBF Gallery 2013
SAT 2013 VENUE
==============
SAT 2013 takes place in Helsinki, the capital of Finland, a vibrant
scandinavian and international city that is easily access from various
destinations within Europe and around the world. SAT 2013 is organized at
University of Helsinki in the very heart of the city. SAT 2013 takes place
during the main summer season, allowing one to experience the whitenights
during which the sun almost never sets.
|
| |  | |  |
|  | |
 | |
The submission deadline for QBF 2013 has been extended a second time. The new deadline is:
*** Wednesday, May 8 23:59 (anywhere on Earth) ***
QBF 2013 (workshop at SAT 2013): http://fmv.jku.at/qbf2013/
|
| |  | |  |
|  | |
 | |
-------------------------------------------------------------------------
CALL FOR PRESENTATION-ONLY POSTERS
Sixteenth International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
--- SAT 2013 ---
Helsinki, Finland, July 8-12, 2013
http://sat2013.cs.helsinki.fi/
*** Acceptance notifications are sent within one week of submission ***
Poster abstract submissions by : May 17, 2013
Notifications by : May 22, 2013
Conference early registration deadline : May 27, 2013
-------------------------------------------------------------------------
The SAT 2013 conference invites submissions of 200-400 word poster
abstracts. Each submitted abstract will be checked for suitability for
presentation as a poster during a poster-session at the main conference.
The poster abstracts may be about (but not restricted to):
-SAT-related work-in-progress.
-SAT-related work recently published or accepted for publication
at other major conferences, workshops, or journals.
-Descriptions of SAT-related systems, interesting benchmark problems, etc.
-Overviews of SAT-related PhD theses or currently on-going PhD work.
-Overviews of SAT-related research projects.
To submit a poster abstract, send the title, list of authors and their
affiliations, and a 200-400 word abstract of your poster by email to
sat2013@easychair.org . The submissions should be in ASCII text.
The accepted poster abstracts will not appear in the SAT 2013 proceedings,
but will be included in the informal conference booklet made available to
all registered attendees. Each poster presenter is expected to register
to the main conference.
SAT 2013 includes three high-quality invited talks (by Albert Atserias,
Edmund M. Clarke, and Peter Stuckey), around 30 scientific presentations,
various satellite events including the SMT, PoS, and QBF workshops and
competition reports, as well as a lively social program.
|
| |  | |  |
|  | |
 | |
The QBF 2013 paper submission deadline is extended to
*** Sunday, April 28 23:59 (anywhere on Earth) ***
QBF 2013 (workshop at SAT 2013): http://fmv.jku.at/qbf2013/
|
| |  | |  |
|  | |
 | | | Department of Science and Technology (DST), Government of India and the French Embassy in India, Ministry of Foreign Affairs, Government of France, Indo French Centre for Promotion of Advanced Research (IFCPAR/CEFIPRA) invites applications from the PhD students of India and France for awarding the Raman-Charpak Fellowship 2013. The programme aims at developing and strengthening Indo-French scientific cooperation through close collaboration between Indian and French laboratories, by supporting the mobility of highly qualified PhD students registered in an Indian or French research institute/ university, to offer them an excellent opportunity for carrying out a part of their doctoral research work in France / India.
Deadline for application submission: May 31' 2013
contact:bhalla.ateet@gmail.com |
| |  | |  |
|  | |
 | | | The fourth Pragmatics of SAT workshop submission deadlines have been slightly extended: abstracts will be accepted until April 20, and papers until April 24. |
| |  | |  |
|  | |
 | |
CALL FOR CONTRIBUTIONS
Configurable SAT Solver Challenge (CSSC) 2013
http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/
Event affiliated with SAT 2013 Conference
http://sat2013.cs.helsinki.fi/
8-12 July 2013, Helsinki, Finland
-----------------------
Most modern SAT solvers have many parameters that can be altered to adjust their behavior and performance. This year, we are
introducing the first Configurable SAT Solver Challenge (CSSC), a competitive event that assesses the *peak performance* of such
parametric solvers (i.e., performance with optimized parameters). CSSC recognizes that the value of a SAT solver for a given
application is often due to the performance achieved after customization for that application rather than merely the performance
of its 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 each of several different state-of-the-art software packages (so-called algorithm configuration
procedures). 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 (8-12 July in Helsinki, Finland).
We invite submissions of both configurable SAT solvers and benchmark instance generators. Although we will accept proprietary
solvers, only open-source submissions will be eligible for prizes. 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 the CSSC 2013 website at
http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/
===== Important Dates =====
30 April 2013: Solver and benchmark registration opens
1 June 2013: final submission of solvers and benchmarks
9-12 July 2013: presentation of results during SAT 2013 Conference
===== Organizers =====
Frank Hutter (Freiburg University)
Adrian Balint (Ulm University)
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://www.cs.ubc.ca/labs/beta/Projects/CSSC2013
|
| |  | |  |
|  | |
 | |
[We apologize if you receive multiple copies of this call]
------------------------------------------------------------------------
CALL FOR PAPERS
QBF 2013
International Workshop on
Quantified Boolean Formulas
Helsinki, Finland, July 9, 2013
http://fmv.jku.at/qbf2013/
Affiliated to and co-located with:
SAT 2013 conference
Helsinki, Finland, July 8-12, 2013
http://sat2013.cs.helsinki.fi/
------------------------------------------------------------------------
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. The workshop also targets
researchers working with quantifiers in other formalisms like Constraint
Satisfaction Problems (CSP) and Satisfiability Modulo Theories (SMT) in order
to exchange experiences and ideas.
===============
IMPORTANT DATES
===============
Please follow http://fmv.jku.at/qbf2013/ 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
==================
TOPICS OF INTEREST
==================
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
================================
SUBMISSION OF EXTENDED ABSTRACTS
================================
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.
Please see the submission website for further guidelines:
http://fmv.jku.at/qbf2013/submission.html
===============
WORKSHOP REPORT
===============
Accepted extended abstracts are collected in an informal report which
will be publicly available at the workshop's website.
==============
PROGRAM CHAIRS
==============
Florian Lonsing
Vienna University of Technology, Austria
Martina Seidl
Johannes Kepler University Linz, Austria
=================
PROGRAM COMMITTEE
=================
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
|
| |  | |  |
|  | |
more...
© 2000-2001 Business & Technology Research Laboratory.
© 2001-2005 Centre de Recherche en Informatique de Lens.
Hosted by Innovation
and Technology Research Lab.
Please send any comment to daniel@satlive.org.
|
 |