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
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
859 elements available
|Appel à communications : JFPC 2014|
Dixièmes Journées Francophones de Programmation par Contraintes,
LERIA, Université d'Angers (UFR Sciences).
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
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 :
LINA, Mines de Nantes, France
Président du comité d'organisation :
Frédéric Lardeux, LERIA,
Université d'Angers, France
| || |
CALL FOR PAPERS
6th International workshop on Constraints in Software Testing,
Verification and Analysis
A workshop of ICSE'14, 36th International Conference on Software
Engineering, Hyderabad, India, 31st May - 7th June 2014
* Workshop paper submissions due January 24, 2014
* Notification to authors February 24, 2014
* Camera-ready copies of authors' papers March 14, 2014
Research papers: Authors are invited to submit original contributions,
presenting novel ideas, results or systems in constraint-based
software engineering. Papers should not be published or submitted
elsewhere during the time of evaluation.
Tool demo papers or fast abstract papers: Authors are invited to
propose tool demonstrations or fast abstract, presenting new tools,
new challenges or breaking results in constraint-based software
Submitted papers must be in PDF format, formatted according to the ACM
Formatting Guidelines. (Please see
LaTeX users, please use the "Option 2" style), and must not exceed the
following size limits:
* Research papers: max 10 pages for the main text, including figures,
tables, appendices, references may be included on up to 2 additional
* Tool demo/fast abstract papers: max 6 pages
All accepted papers will be published in the workshop proceedings.
Recent years have seen an increasing usage and consequent impact of
Boolean SAT, SMT and Constraint Programming (CP or CSP) solvers in
testing, verification and analysis of software systems. The primary
reason for this is the dramatic improvement in the efficiency and
expressive power of solvers. As newer and more powerful solvers are
built, software engineering researchers dramatically scale existing
applications such as symbolic-execution methods, or find unexpected
applications for them, e.g., software product lines or fault
This workshop will bring together researchers in solvers and software
engineering applications in order to raise the awareness of constraint
solving in the broader software engineering research community, and
encourage development of new applications based on tunable,
extensible, and programmable solvers. The workshop will cover a broad
range of topics where solvers have already made an impact, e.g.,
symbolic-execution based testing, verification and analysis, as well
as newer applications where their use is still nascent, e.g.,
synthesis, software product lines and fault localization. Submission
topics include, but are not limited to, the following:
- Constraint-based analysis of programs and models
- Constraint-based test input generation and fault localization
- Solvers and computer security
- SMT solvers for testing, verification, analysis, and synthesis
- Programmable SMT solvers
- Combinations of constraint solvers
- Solvers for software product lines
Following the 5 previous editions of this workshop, held first at the
CP and then the ICST conferences, this year’s CSTVA workshop will
be held at ICSE with the goal of strengthening the links between the
solver and software engineering research communities. The workshop
aims to encourage newer applications of solvers, showcase their rich
extensible APIs, and act as a forum for feedback from users to solver
Vijay Ganesh, Univ. Waterloo, Canada, email@example.com
Nicky Williams, CEA LIST, France, firstname.lastname@example.org
| || |
CALL FOR PAPERS
Seventeenth International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
--- SAT 2014 ---
Vienna, Austria, July 14-17, 2014
Abstract submission deadline: January 17, 2014
Paper submission deadline: January 24, 2014
The International Conference on Theory and Applications of
Satisfiability Testing (SAT) is the primary annual meeting for
researchers studying the theory and applications of the propositional
It includes, besides plain propositional satisfiability, 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 encoded as SAT instances, in the
broad sense mentioned above, including problems in formal verification
(hardware and software), artificial intelligence, and operations
research. More recently, biology, cryptology, data mining, machine
learning, and mathematics have been added to the growing list.
The SAT conference aims to further advance the field by soliciting
original theoretical and practical contributions in these areas with a
clear connection to satisfiability.
SAT 2014 takes place in Vienna, Austria, and will be part of the
Vienna Summer of Logic. With over two thousand expected participants,
the Vienna Summer of Logic 2014 will be the largest event in the
history of logic, and will consist of twelve large conferences and
numerous workshops, attracting researchers from all over the world.
Vienna, the capital of Austria, is well known for its historic role in
music (Mozart, van Beethoven, Liszt, and Brahms, among others, came
there to work), its churches (e.g., St. Stephen's Cathedral), museums
and architecture. Moreover, Vienna was ranked the world's most livable
city in 2005.
(Follow http://baldur.iti.kit.edu/sat2014 for updates.)
January 17, 2014: Abstract submission deadline
January 24, 2014: Paper submission deadline
March 17, 2014 (approx.): Response from authors begins, lasts 72 hours
March 27, 2014: Acceptance notifications
April 17, 2014: Final camera-ready versions
July 14-17, 2014: Main conference and workshops
SAT 2014 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), 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;
Implementation-level details of SAT solving tools and SAT-based
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
All accepted papers will be published in the proceedings of the
conference, which will be published within the Springer LNCS series.
WORKSHOPS AND COMPETITONS
Affiliated with SAT 2014 are several workshops and competitions.
For a list and detailed information about these events see the SAT 2014
Uwe Egly Vienna University of Technology, Austria
Carsten Sinz Karlsruhe Institute of Technology, Germany
Ines Lynce Technical University of Lisbon, Portugal
| || |
The source code of open-wbo is available at http://sat.inesc-id.pt/open-wbo/
Open-wbo is a competitive open source Maximum Satisfiability (MaxSAT) solver based on wbo solver.
It includes several of the most recent techniques for MaxSAT. You can plug in any minisat-like SAT solver with minimum effort.
| || |
|call-for-proposals India-Hungarian Strategic Research Fund (IHSRF), being supported by the Governments of India and Hungary. Deadline to submit proposal is 15 January 2014. Tentative start date is June 2014. Duration is for 2 years. Hungarian Researchers interested for proposal submission in the area of Algorithms for Satisfiability (SAT) solving, please contact Dr Ateet Bhalla (email@example.com)|| |
| || |
One year after his invited talk at SAT12, Donald Knuth released his own implementation of the CDCL architecture in the solver named SAT13. The solver is written in Cweb (literate programming), but can be translated into plain C using Cweb toolbox. Note that such solver does not take as input the classical Dimacs format used in the community but a specific one. A translator from Dimacs format is also provided.
Note that several other SAT solvers are available from the same web page, including local search solvers, lookahead solvers and a preprocessor.
Those solvers were designed when Donald Knuth was working on SAT for his Volume 4B of the Art of computer Programming, to appear.
| || |
| What's new in the Glucose 3.0 version?
- We don't use anymore the
Satelite external preprocessor. We rely on the
simp directory, preprocessing the instance right in Glucose (thanks to the mechanism already implemented in Minisat).
- We have included two new operating mode:
- Certified UNSAT, you can output the proof for UNSAT and independently check it (thanks to Marijn Heule implementation of the DRUP trace).
- Incremental mode of operation, when you want to use Glucose inside a MUS extractor, for instance, or any other Incremental SAT Solving solver. We experimented a significant gain by using our new version of incremental Glucose w.r.t. the previous one (see our paper below about Incremental SAT Solving).
- A few other optimisations, as described in the SAT competition 2013 Companion Paper.
- Too bad we don't have any In-Processing techniques. 2013 was the year of this new technique in SAT solvers.
- Note: The default mode of Glucose now doesn't print the final Model if SAT. You have to use
-model to turn it on now.
| || |
|Master, PhD student, PostDoc interested to work on project "Software Test Automation through efficient Model-Checking Technology". Interested candidates should inquire for further information by sending email to Dr. Ateet Bhalla (firstname.lastname@example.org)|| |
| || |
One post-doc position in ICT on the research project
"Advanced SMT Techniques for Word-level Formal Verification - (WOLF)"
is available in Trento, Italy, under the joint supervision of
- Alessandro Cimatti, FBK, Trento, and
- Roberto Sebastiani, DISI, University of Trento.
The research activity will be carried out jointly within the Embedded
Systems (ES) Research Unit of the Center for Scientific and
Technological Research of the Fondazione Bruno Kessler (FBK), Trento,
and the Software Engineering, Formal Methods & Security Research
Program, at Department of Information Engineering and Computer Science
(DISI) of University of Trento.
Aim and Scope
The research activity will aim at investigating and developing novel
techniques, methodologies and support tools for Satisfiability Modulo
Theories (SMT) for the formal verification of systems. This work will
be part of the "Advanced SMT Techniques for Word-level Formal
Verification - (WOLF)" project, a three-year research project
supported by SRC/GRC (http://www.src.org/compete/s201113/), in strict
collaboration with the Formal Verification Group at Intel, Haifa, and
other major HW companies.
The ultimate goal of the WOLF project is to provide a comprehensive
SMT package to support effective formal verification of systems
ranging from RTL circuits all the way up to high-level hardware
description languages (e.g. SystemC) and software. The package will be
implemented on top of the MathSAT SMT platform
(http://mathsat.fbk.eu/), and provided as an API.
The ideal candidate should have an PhD in computer science or related
discipline, and combine solid theoretical background and excellent
software development skills (in particular C/C++).
A solid background knowledge and/or previous experience on one of the
following topics (in order of preference) is required:
Satisfiability Modulo Theory (SMT), Propositional Satisfiability (SAT),
Model Checking, Automated Reasoning.
Previous experience in the following areas will also be considered
favourably: Constraint Solving and Optimization, Embedded Systems
Design Languages (e.g. Verilog, VHDL).
The candidate should be able to work in a collaborative environment,
with a strong committment to reaching research excellence and achieving
Terms and dates
The position will start as soon as possible, and will have to be
renewed yearly, for a maximum of two years. The expected salary
will range from about 2200 to 2400 euros net income, and the gross
will include previdential (social security) contributions. Facilities
for meals at the local canteen can be provided.
Applications and Inquiries
Interested candidates should inquire for further information and/or
apply by sending email to email@example.com, with subject
'POSTDOC ON WOLF PROJECT'.
Applications should contain a statement of interest, with a Curriculum
Vitae, and the names of reference persons. PDF format is strongly
encouraged. It should also indicate an estimated starting date.
Early availability will be considered with much favour.
Dr. ALESSANDRO CIMATTI,
Embedded Systems Research Unit,
via Sommarive 18, I-38123 Povo, Trento, Italy
Prof. ROBERTO SEBASTIANI
Software Engineering, Formal Methods & Security Research Program
DISI, University of Trento,
via Sommarive 14, I-38123 Povo, Trento, Italy
| || |
|Abstract submission deadline: September 30;
Paper submission deadline: October 7;
Notification of acceptance: October 15;
Camera-ready version deadline: November 5;
Workshop date: November 21;
Formal verification is of crucial significance in the development of hardware and software systems. In the last few years, tremendous progress was made in both the speed and capacity of constraint technology. Most notably, SAT solvers have become orders of magnitude faster and capable of handling problems that are orders of magnitude bigger, thus enabling the formal verification of more complex computer systems. As a result, the formal verification of hardware and software has become a promising area for research and industrial applications.
The main goals of the Constraints in Formal Verification workshop are to bring together researchers from the CSP/SAT and the formal verification communities, to describe new applications of constraint technology to formal verification, to disseminate new challenging problem instances, and to propose new dedicated algorithms for hard formal verification problems.
This workshop will be of interest to researchers from both academia and industry, working on constraints or on formal verification and interested in the application of constraints to formal verification.
The scope of the workshop includes topics related to the application of constraint technology to formal verification, namely:
- application of constraint solvers to hardware verification;
- application of constraint solvers to software verification;
- dedicated solvers for formal verification problems;
- challenging formal verification problems.
The workshop will take place in the Hilton Hotel in San Jose, California, on November 21, 2013, right after ICCAD'13. It will be structured to allow ample time for discussion and demonstration of new tools and new problem instances.
Submissions should be in the IEEE style and in one of the following types:
- a regular paper of up to 6 pages;
- a short paper of up to 4 pages, describing an industrial experience.
Papers should be e-mailed in pdf format to the workshop chair: firstname.lastname@example.org
- Thomas Ball, Microsoft, U.S.A.
Talk title: Efficient Modular SAT Solving for Property-Directed Reachability
- Kristin Rozier, NASA, U.S.A.
Talk title: Application of Constraints to Formal Verification of Software at NASA
Miroslav Velev, Aries Design Automation, U.S.A.
Maciej Ciesielski, University of Massachusetts, U.S.A.
Masahiro Fujita, University of Tokyo, Japan
Alex D. Groce, Oregon State University, U.S.A.
Sumit Jha, University of Central Florida, U.S.A.
Susmit Jha, Intel, U.S.A.
Andreas Veneris, University of Toronto, Canada|| |
| || |
© 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 email@example.com.