 |
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.
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
759 elements available | |
----- SAT Challenge 2012 -----
Affiliated with SAT 2012,
June 17-20, Trento, Italy
The SAT Challenge 2012 is a competitive event for solvers for the Boolean
Satisfiability (SAT) problem. It is organized as a satellite event to the
15th International Conference on Theory and Applications of Satisfiability
Testing (SAT 2012) and stands in the tradition of the SAT Competitions
that have been held yearly from 2002 to 2005 and biannually starting from
2007, and the SAT-Races held in 2006, 2008 and 2010.
The area of SAT solving has seen tremendous progress over the last years.
Many problems (e.g., in hardware and software verification) that seemed
to be completely out of reach a decade ago can now be handled routinely.
Besides new algorithms and better heuristics, refined implementation
techniques turned out to be vital for this success. To keep up the
driving force in improving SAT solvers, we want to motivate implementors
to present their work to a broader audience and to compare it with that
of others.
THE CHALLENGE
The SAT Challenge differs from both previous SAT Competitions and
SAT-Races. Similar to SAT Competitions, there will be several tracks
suitable for different kinds of solving algorithms (e.g. complete or
local search). Similar to SAT-Races, the time to solve each instance
will be limited to 15 minutes, and the solvers' source code need not
be made publicly available (although this is strongly encouraged).
The SAT Challenge 2012 will consist of 6 independent tracks, including:
* Four Main Tracks for Sequential Solvers:
- Application SAT+UNSAT:
problem encodings (both SAT and UNSAT) from real-world applications.
- Hard Combinatorial SAT+UNSAT:
hard combinatorial problems (both SAT and UNSAT) to challenge current
SAT solving algorithms.
- Random SAT:
randomly generated satisfiable instances.
- Random UNSAT:
randomly generated unsatisfiable instances.
* Parallel Solver Track:
Same problem instances as in the Application Main Track.
Four cores of a CPU can be used.
* Sequential Portfolio Solver Track:
Same problem instances as in the Application Main Track.
A portfolio solver combines different SAT algorithms.
IMPORTANT DATES
March 11, 2012:
Deadline for registering solvers.
March 26, 2012:
Deadline for handing in benchmarks.
March 26, 2012:
Test runs of solvers finished, begin of feedback/revision period.
April 11, 2012:
Deadline for submitting final versions of solvers.
Around June 20, 2012:
Announcement of results at the SAT 2012 conference.
ORGANIZING COMMITTEE
Adrian Balint University of Ulm, Germany
Anton Belov University College Dublin, Ireland
Matti Jarvisalo University of Helsinki, Finland
Carsten Sinz Karlsruhe Institute of Technology, Germany
|
| |  | |  |
|  | |
 | |
[apologies if you receive multiple copies of this message]
The Vienna Center for Logic and Algorithms (www.VCLA.at) is an initiative of
Vienna University of Technology (TU Vienna). Located at the Faculty of Informatics,
the Center promotes international scientific collaboration in logic and algorithms.
The Center celebrates its opening through the following three events:
SYMPOSIUM "LOGIC AND ALGORITHMS: A SCIENTIFIC PERSPECTIVE"
Wednesday, 25th January 2012, 9:00-15:00, Festsaal, TU Vienna
Invited Speakers:
* Edmund M. Clarke, Carnegie Mellon University
* Fedor V. Fomin, University of Bergen
* Thomas A. Henzinger, IST Austria
* Joao Marques-Silva, University College Dublin & IST/INESC-ID
* Georg Weissenbacher, Princeton University
OFFICIAL OPENING CEREMONY
Wednesday, 25th January 2012, 15:00-16:00, Festsaal, TU Vienna
Speakers:
* Sabine Seidler, Rector of the TU Vienna
* Gerald Steinhardt, Dean of the Faculty of Informatics, TU Vienna
* Stefan Szeider and Helmut Veith, VCLA, Co-chairs, TU Vienna
AWARD OF A HONORARY DOCTORATE TO E.M. CLARKE
Thursday, 26th January 2012, 10:00, Boecklsaal, TU Vienna
For details see the Center's website at http://www.VCLA.at
|
| |  | |  |
|  | |
 | |
The Software Design Group in MIT’s Computer Science and Artificial Intelligence Lab (CSAIL) is hiring a Research Scientist to participate in research and development of the Alloy language and analyzer.
Alloy (http://alloy.mit.edu) is a lightweight modeling language with an automatic analyzer based on SAT. It has been used in a wide range of applications in software engineering, including the design of access control schemes, security mechanisms, network protocols, ontologies, and so on. In addition to design analysis, Alloy has also been used for code verification, test case generation and automatic configuration. Alloy was introduced in 1997, and is now in version 4. Hundreds of papers have been written describing research based on Alloy; for examples, see http://alloy.mit.edu/applications.html. Alloy has also been taught in dozens of university courses.
Our plan now is to take Alloy in new directions, and dramatically improve the usability and scalability of the analyzer. We are looking for someone who is is excited by these possibilities and will be deeply involved not only in design and implementation but also in strategic planning. There are also opportunities to co-advise students and participate in research proposals.
Qualifications should include:
- a PhD in computer science or a related field;
- superb programming skills, preferably with experience of writing compiler-like tools;
- familiarity with logic and model checking;
- a passion for design;
- excellent communication and writing skills;
- ability to work both independently and cooperatively with others.
Please apply online to MIT (http://jobs.mit.edu/) with resume and cover letter, and include the following in your application (sent separately to djresci@csail.mit.edu): (A) A list of languages and technologies you're familiar with; (B) A short sample of something you've written in English, and a small code sample; (C) A short answer to the question: "If you could make one big change to the Alloy system, what would it be?" Please reference MIT job number 00008292 in your application.
|
| |  | |  |
|  | |
 |  | |  | | | | | Date: | 11-Jan-2012 | | Title: | Call for Papers - IWSBP 2012
| | Hits: | 37 | | Contributed by: | Miroslav Velev | | Keywords: | Repository, Verification, Structure of problems, EDA, Benchmark, SAT application, Equivalency Reasoning, Instance simplification, Satisfiable Problems Generation, SAT tools, call for papers, null, null |
| | | |  |  | |
 | |
Call for Papers - IWSBP 2012
-------------------------------------------------------------------------
Please, feel free to forward this message to interested people.
We apologize if you receive this email more than once.
-------------------------------------------------------------------------
Dear colleague,
the 10th International Workshop on Boolean Problems will be held on
September 19-21, 2012, in Freiberg, Germany.
More information you can find on the workshop web page
http://www.informatik.tu-freiberg.de/prof2/ws_bp10/
Deadlines
Submission - May 5, 2012
Acceptance notices - June 9, 2012
Final version submission - July 7, 2012
Sincerely,
Prof. Dr.-Ing. habil. Bernd Steinbach
Call for Papers
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
- Mitch Thornton (SMU Dallas (Texas), USA),
- Raimund Ubar (TTU Tallinn, Estonia), and
- Vincent Gaudet (University of Waterloo, Canada) 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, no longer than 6 pages, as a PDF file to
iwsbp2012@informatik.tu-freiberg.de
or using the workshop web page
http://www.informatik.tu-freiberg.de/prof2/ws_bp10/
by April 25, 2012. Acceptance notices will be sent by June 9, 2012.
The final version of the paper should be submitted by July 7, 2012.
Program Committee
- J. Butler, Naval Postgraduate School Monterey, USA
- R. Berghammer, C-A-University of Kiel, Germany
- L. Cheremisinova, Minsk Academy of Science, Belarus
- D. Debnath, Oakland University, USA
- R. Drechsler, University of Bremen, Germany
- E. Dubrova, Royal Institute of Technology (KTH), Sweden
- G. Dueck, University of New Brunswick, Canada
- D. Große , University of Bremen, Germany
- I. Levin, Tel Aviv University, Israel
- T. Luba, Warsaw University of Technology, Poland
- M. Miller, University of Victoria, Canada
- C. Moraga, TU Dortmund, Germany
- M. A. Perkowski, Portland State University, USA
- Y. Pottosin, Minsk Academy of Science, Belarus
- T. Sasao, Kyushu Institute of Technology, Japan
- Ch. Scholl, University of Freiburg, Germany
- R. Stankovic, University of Nis, Serbia
- B. Steinbach, University of Freiberg, Germany
- R. Ubar, Tallinn Technical University, Estonia
- M. Velev, Aries Design Automation, USA
- A. De Vos, University of Gent, Belgium
- S. Yanushkevich, University of Calgary, Canada
- A. D. Zakrewskij, Minsk Academy of Science, Belarus
Conference Language: English
Conference Location: Freiberg University of Mining and Technology, Freiberg (Sachs.), Germany
|
| |  | |  |
|  | |
 | | CPAIOR 2012 - CALL FOR WORKSHOP PROPOSAL
Ninth International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming,
Cité des Congrès, Nantes, France,
May 28 - June 1, 2012.
http://www.emn.fr/z-info/cpaior-2012/
The CPAIOR 2012 conference chairs invite proposals for the workshop program.
CPAIOR 2012 workshops will provide an informal setting where workshop participants will have the opportunity to discuss specific technical topics in an atmosphere that facilitates the active exchange of ideas. It is an opportunity to disseminate work in progress or to promote new and emerging areas on the intersection of CP, AI, and OR.
All workshops will take place on May 29, 2012, at the site of the main conference. Workshops can be proposed for a full or a half day. The internal format of the workshop will be determined by the organizers of each workshop.
Proposals for workshops should contain the following information:
- The title and a brief technical description of the workshop, specifying the goals and the technical issues it will focus on (this description is meant to be published on the main conference homepage).
- The intended duration of the workshop (full/half day).
- A brief discussion of why and to whom the workshop is of interest.
- A list of related workshops held within the last three years, if any, and their relation to the proposed workshop.
- The names of the proposed organizing committee.
- The name and email address of the main organizer.
Each workshop main organizer will be responsible for:
- Creating a web site for the workshop that will be linked from the CPAIOR 2012 website.
- Organizing the technical program: call for papers, selecting submissions, inviting attendant, etc.
- Providing working pdf notes to be duplicated for the workshop by May 11, 2012.
The CPAIOR 2012 conference chairs will be responsible for the following:
- Providing publicity for the workshop series as a whole.
- Providing logistics support and a meeting place for the workshop.
- Scheduling workshops in cooperation with the workshop organizers.
- Duplicating working notes (possibly in electronic form) and distributing them to the participants.
All proposals should be submitted by electronic mail (in ASCII), to the workshop chair.
Important Dates:
February 6, 2012: Proposal submission deadline.
February 13, 2012: Acceptance notification.
February 27, 2012: Deadline for receipt of the URL and Call for Papers/Participation for the workshop.
May 11, 2012: Deadline for workshop working notes.
May 29, 2010: CPAIOR 2012 workshops.
CPAIOR 2012 Workshop Chair:
Thierry Petit, Co-Head TASC, LINA / Ecole des Mines de Nantes.
Thierry.Petit@mines-nantes.fr |
| |  | |  |
|  | |
|  | |
 | |
The SAT/SMT Summer School 2012 (2nd edition) aims at providing graduate
students and researchers from universities and industry with a
comprehensive overview of the research in SAT, SMT, and their
application. The lectures cover the foundational and practical aspects
of SAT and SMT solvers, as well as their application to verification,
planning, scheduling, and optimization problems.
This second edition follows the Summer School of 2011 organized by Vijay
Ganesh at MIT, and is co-located with the SAT 2012 conference. The
school will take place in Trento, Italy, from June 12th to June 15th
2012.
The program will feature four lectures per day, with the first two days
dedicated to SAT and SMT foundations, and the last two to applications
on various domains.
List of speakers:
- Armin Biere (Johannes Kepler University, Linz, Austria)
- Leonardo de Moura (Microsoft Research Redmond, USA)
- Bruno Dutertre (SRI International, USA)
- Martin Fränzle (Carl von Ossietzky Universität Oldenburg, Germany)
- John Franco (University of Cincinnati, USA)
- Silvio Ghilardi (Università di Milano, Italy)
- Patrice Godefroid (Microsoft Research Redmond, USA)
- Holger Hoos (University of British Columbia, Vancouver, Canada)
- Tomi Janhunen (Aalto University, Finland)
- Pete Manolios (Northeastern University, USA)
- Joao Marques-Silva (University College Dublin, Ireland)
- Ken McMillan (Microsoft Research Redmond, USA)
- Jussi Rintanen (Austrialian National University, Australia)
- Fabio Somenzi (University of Colorado, Boulder, USA)
- Gunnar Stålmarck (Prover Technology and Gain Sweden AB, Sweden)
- Cesare Tinelli (University of Iowa, USA)
A more detailed program is available at the school website
(http://satsmtschool2012.fbk.eu).
It is expected that we will be able to provide a limited number of
grants for students that will attend the school. More details about the
procedure for applying and the registration deadlines will appear on the
school website as soon as possible. Interested students are however
encouraged to contact us at any moment.
The school organizers,
Alberto Griggio <griggio@fbk.eu> and
Stefano Tonetta <tonettas@fbk.eu> |
| |  | |  |
|  | |
 | |
---------------------------------------------------------------------------
[[[ We apologize if you receive multiple copies of this message ]]]
---------------------------------------------------------------------------
Job Description:
=================
The research activity will aim at investigating and developing novel techniques,
methodologies and support tools for the verification of circuit designs in
particular the use of Satisfiability Modulo Theories (SMT), however researcher
with background on other verification techniques are also encouraged to apply.
Candidate Profile:
=================
World class researcher in EE/CS/Math (particularly formal theory), familiar with
predicate logic, temporal logic (e.g., CTL, LTL), model checking, familiar with
complexity of algorithms, very strong in algorithm development -- including
design and implementation of large programs, very strong in mathematical
considerations in the development of CAD tools/EDA and familiarity with design practice.
Intimate knowledge of solvers such as BDD, SAT, ATPG, SMT and symbolic simulation algorithms.
Capability of working with prospective customers. Experience in a Semiconductor
company is helpful but not absolutely essential.
Job Requirements:
=================
BS in EE/CS/Math. with 9+ years of relevant experience, MS with 7+ years of relevant experience, or related Ph.D.
It is essential that the individual has strong desires to learn and explore new technologies and are
able to demonstrate good analysis and problem solving skills. Prior knowledge and experience of CAD
tool/EDA development are a big plus.
Job site:
=========
The researcher will be part of Atrenta's EU based advanced research center and can work from any EU country.
The company will not sponsor immigration visa.
Contact Person
==============
Fahim@atrenta.com
|
| |  | |  |
|  | |
 | |
-------------------------------------------------------------------------
15th International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT'12
Trento, Italy, June 17-20th, 2012 http://sat2012.fbk.eu/
CALL FOR WORKSHOP PROPOSALS
-------------------------------------------------------------------------
CALL FOR SAT'12-ASSOCIATED WORKSHOPS PROPOSALS
Researchers and practitioners are invited to submit proposals for
associated workshops on topics related to the SAT conference.
The workshops will be held in parallel the day before the conference
(June 16th 2011), immediatly after the SAT/SMT school.
See http://sat2012.fbk.eu.
Proposals should consist of two parts.
* a short scientific justification of the proposed topic, its
significance, and the particular benefits of the workshop to the
community, as well as a list of previous or related workshops (if
relevant).
* an organizational part should include contact information of the
workshop organizers, procedures for selecting papers and
participants, estimate of the audience size and a tentative list of
the program committee.
Proposals are due by 20.12.2012 and must be submitted by email to both
SAT'12 Conference Chairs: cimatti@fbk.eu and rseba@disi.unitn.it.
If you are interested in proposing a workshop, or you're considering
doing that, please contact us in advence.
Alessandro Cimatti and Roberto Sebastiani
SAT2012 Chairs
|
| |  | |  |
|  | |
 | | World class researcher in EE/CS/Math (particularly formal theory),
familiar with predicate logic, temporal logic (e.g., CTL, LTL), model
checking, familiar with complexity of algorithms, very strong in
algorithm development -- including design and implementation of large
programs, very strong in mathematical considerations in the
development of CAD tools/EDA and familiarity with design
practice. Intimate knowledge and familiarity with one of this
techniques BDD, SAT, SMT, ATPG and symbolic simulation
algorithms. Capability of working with prospective
customers. Experience in a Semiconductor company is helpful but not
absolutely essential.
Job Requirements: BS in EE/CS/Math. with 9+ years of relevant
experience, MS with 7+ years of relevant experience, or related Ph.D.
It is essential that the individual has strong desires to learn and
explore new technologies and are able to demonstrate good analysis and
problem solving skills. Prior knowledge and experience of CAD tool/EDA
development is a definite plus.
|
| |  | |  |
|  | |
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.
|
 |