 |
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
598 elements available | | | The results of the second ASP competition has just been unveiled. |
| |  | |  |
|  | |
 | |
Call for Papers
Formal Methods and Verification Track
Design, Automation & Test in Europe
Dresden, Germany
March 8-12, 2010
The Design, Automation and Test in Europe conference and exhibition is the
premiere European event bringing together designers and design automation
users, researchers and vendors, as well as specialists in the hardware and
software design, test and manufacturing of electronic circuits and systems.
This five-day event consists of a conference with plenary keynotes, regular
papers, interactive presentations, panels and hot-topic sessions,
tutorials, master courses and workshops. DATE is also Europe's leading
commercial exhibition showing the state-of-the-art in design and test
tools, methodologies, IP and design services. Both the conference and the
exhibition, together with the many user group meetings, fringe meetings,
university booth and social events offer a wide variety of opportunities to
meet and exchange information.
The Formal Methods and Verification Track (D8) is devoted to the
presentation and discussion of state-of-the-art advances in a variety of
focus areas, including but not limited to:
* Formal verification and specification techniques including equivalence
checking, model checking, symbolic simulation, theorem-proving,
abstraction and refinement techniques, and real time verification
* Technologies supporting formal verification, including SMT, SAT, BDD,
ATPG, and related work
* Semi-formal verification techniques
* Applications and case studies, including formal verification of IPs,
SoCs, cores and real-time/embedded systems
* Verification in practice, namely the integration of verification into
the design flow
Jason Baumgartner (Chair) IBM Corporation, jason.r.baumgartner@gmail.com
Joao Marques-Silva (Co-Chair) University College Dublin, jpms@ucd.ie
Armin Biere Johannes Kepler University
Per Bjesse Synopsys Inc.
Roderick Bloem Graz University of Technology
Gianpiero Cabodi Politecnico di Torino
Alessandro Cimatti FBK-IRST
Daniel Kroening Oxford University
Wolfgang Kunz University of Kaiserslautern
Panagiotis Manolios Northeastern University
All manuscripts must be submitted electronically by September 6th, 2009,
following the instructions on the conference Web page:
www.date-conference.com
|
| |  | |  |
|  | |
 | |
Context and scientific objectives: SAT (decide if a Boolean formula, typically in conjunctive normal form, admits a valuation which
makes it true?) is a fundamental problem in complexity theory with very large practical benefits. Modern SAT solvers can now
handle propositional satisfiability problems with hundreds of thousands of variables or more. However, many practical instances
remain difficult to all the available SAT solvers. Consequently, new approaches are clearly needed to solve these challenging
industrial problems. In this context and with the light of the next generation of computer architectures, the design of parallel
satisfiability solvers becomes a fundamental issue. The aim of this PhD is to provide new theoretical and practical advances for
parallel satisfiability solving.
Laboratory: CRIL - CNRS UMR 8188, Université d'Artois, Lens, France
Supervision:
Pr. Lakhdar Sais, CRIL, Lens, France
Dr. Youssef Hamadi, Microsoft Research, Cambridge, UK
Application: please send : CV, motivation letter, recommendation letters to : sais@cril.fr
|
| |  | |  |
|  | |
 | | | Call for Papers, Abstracts, and Discussion Topics: CROCS 2009
First International Workshop on Constraint Reasoning and Optimization
for Computational Sustainability
September 20, 2009, Lisbon, Portugal
To be held in conjunction with CP-09, the 15th International
Conference on Principles and Practice of Constraint Programming.
For more information on this workshop as well as the newly emerging interdisciplinary field of computational sustainability, please visit http://www.computational-sustainability.org/crocs09.
Best,
Ashish |
| |  | |  |
|  | |
 | |
SymCon'09 First Call for Papers
The Ninth International Workshop on Symmetry and Constraint Satisfaction Problems
To be held at the Fifteenth International Conference on Principles and Practice of Constraint Programming (CP 2009)
Lisbon, Portugal, September 20, 2009
Submission deadline: Monday, 29 June 2009
Notification of acceptance: Friday, 31 July 2009
Camera ready deadline: Friday, 14 August 2009
Workshop: Sunday, 20th September 2009
***For more information, please see the Call for Papers at: http://alexf04.maclisp.org/symcon09.html
Workshop topics include, but are not limited to:
- Symmetry definition: semantic symmetry, syntactic symmetry, constraint symmetry, solution symmetry
- Automatic symmetry detection: static approaches and dynamic approaches
- Global symmetry detection and elimination
- Dynamic symmetry detection and elimination
- Combining symmetry breaking techniques
- Exploiting weak forms of symmetries like "dominance" and "almost-symmetries"
- Case studies of problems that exhibit interesting symmetries
- Application of computational group theory techniques to symmetry breaking
- Heuristics that use information about symmetry to guide search - Elimination and avoidance of symmetry by re-modelling
- Dynamic avoidance of symmetric states during search
- Complexity analysis of symmetry breaking techniques
- Application of CSPs to symmetry and related algebraic problems - Comparing symmetry breaking techniques in constraint
programming with techniques for dealing with symmetry in other search domains
- Symmetry in CNF formulas and OBF formulas
- Symmetry in finite model search in first order logic
- Novel exploitation of symmetry in varied search domains of interest to the CP community
***For more information, please see the Call for Papers at: http://alexf04.maclisp.org/symcon09.html
|
| |  | |  |
|  | |
 | | | Recent years have shown a major architectural shift in computer hardware. The traditional efficiency gains upcoming from the relentless raise of chips frequencies has been stopped by a thermal wall and performance improvements have to be found elsewhere. The new direction is to add more computing units (cores) to a chip in order to raise its computational power. The products resulting from this multi-core strategy are now on every desktop and yet the horizon is wide open since the number of cores is expected to grow exponentially. This technological shift represents an important challenge for many computer sciences fields whose best algorithms have to be rethought for multi-core-based parallelization. The goal of this special issue is to officially acknowledge this evolution, and to present recent advanced in the parallel processing of SAT problems. |
| |  | |  |
|  | |
 | | | MiniQBF - A Basic Search-Based QBF Solver
This is the first version of MiniQBF - a search-based QBF solver based on MiniSAT 2.0 by Niklas Een and Nilkas Soerensson.
The current aim of this solver is to provide researchers that are interested in QBF with a light-weight and understandable baseline QBF solver. I tried to keep the extension and alternations to MiniSAT to a minimum so that it will be quite straight-forward for anyone who knows MiniSAT
to understand how the QBF version works. There are definitively parts of the code and techniques that can be improved (e.g., conflict / solution analysis), and in terms of updating/changing the code this should indeed be feasible. In total, I hope that this solver will enable people to try out new ideas without the need of developing a new QBF solver or to put a lot of effort in understanding a solver first.
In contrast to MiniSAT this solver is a not a state-of-the-art solver. However, it is quite competitive for a pure search-based solver. In addition, I also want to point out that I tried to verify the correctness of the solver empirically, but it might be the case that I made a mistake in the code. Therefore, I also hope that researcher interested in certifying or verifying the result of a QBF solver might find this small QBF solver relatively attractive as well.
I would also like to thank the following people for their comments on or contributions
to this solver:
Fahiem Bacchus
Christoph Wintersteiger
Lucas Bordeaux
Said Jabbour
The source code can be downloaded here:
MiniQBF 1.0
Please feel free to comment on this or to report bugs, or to improve the solver, etc.
If you prefer, you can also write me an email at: Email Me
Thanks,
Horst |
| |  | |  |
|  | |
 | | | NFLSAT is a new SAT solver that operates on the negation normal form (NNF) of the given Boolean circuits. The input to NFLSAT is a Boolean circuit in And Inverter Graph (AIG) format or ISCAS format. |
| |  | |  |
|  | |
 | | | The new release focuses mainly in simplifying the integration and the use of the solvers in Java programs.
The release includes also improved pseudo boolean and maxsat solvers.
SAT4J 2.1 core and pseudo packages will ship with Eclipse 3.5 next month. |
| |  | |  |
|  | |
 | | | Abstract Most, if not all, state-of-the-art complete SAT solvers are complex variations of the DPLL procedure described in the early 1960’s. Published descriptions of these modern algorithms and related data structures are given either as high-level state transition systems or, informally, as (pseudo) programming language code. The former, although often accompanied with (informal) correctness proofs, are usually very abstract and do not specify many details crucial for efficient implementation. The latter usually do not involve any correctness argument and the given code is often hard to understand and modify. This paper aims to bridge this gap by presenting SAT solving algorithms that are formally proved correct and also contain information required for efficient implementation. We use a tutorial, top-down, approach and develop a SAT solver, starting from a simple design that is subsequently extended, step-by-step, with a requisite series of features. The heuristic parts of the solver are abstracted away, since they usually do not affect solver correctness (although they are very important for efficiency). All algorithms are given in pseudo-code and are accompanied with correctness conditions, given in Hoare logic style. The correctness proofs are formalized within the Isabelle theorem proving system and are available in the extended version of this paper. The given pseudo-code served as a basis for our SAT solver argo-sat. |
| |  | |  |
|  | |
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.
|
 |