Date: 01-Jul-2009 Title: Second ASP competition results available! Hits: 78 Contributed by: Daniel Le Berre Keywords: Answer Set Programming         The results of the second ASP competition has just been unveiled.

Date: 26-Jun-2009 Title: CFP: DATE'10 Formal Methods and Verification Track Hits: 79 Contributed by: Joao Marques-Silva Keywords: Satisfiability Modulo Theory, null, null, null, null         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

Date: 21-Jun-2009 Title: MSR PhD Scholarship on Parallel SAT Solving Hits: 45 Contributed by: Daniel Le Berre Keywords: Distributed Computing, distributed parallel dynamic learning, null         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

Date: 15-Jun-2009 Title: CROCS-09: Call for Submissions (computational sustainability) Hits: 46 Contributed by: Ashish Sabharwal Keywords: SAT application, General Interest, New research position, null, null         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

Date: 06-Jun-2009 Title: First CFP: Symcon'09 - The Ninth International Workshop on Symmetry and Constraint Satisfaction Problems Hits: 45 Contributed by: Alex Fukunaga Keywords: CSP, symmetry, Constraint Programming, SAT/CP         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

Date: 05-Jun-2009 Title: JSAT special issue on // SAT solving available! Hits: 139 Contributed by: Daniel Le Berre Keywords: Distributed Computing, distributed parallel dynamic learning, SAT-solver, null         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.

Date: 03-Jun-2009 Title: MiniQBF 1.0 Hits: 68 Contributed by: Horst Samulowitz Keywords: DPLL, QBF, null         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

Date: 29-May-2009 Title: NFLSAT Non-clausal Formulas Satisfiability Checker released! Hits: 124 Contributed by: Daniel Le Berre Keywords: Verification, Structure of problems, SAT tools, Boolean functions         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.

Date: 27-May-2009 Title: SAT4J 2.1 released! Hits: 81 Contributed by: Daniel Le Berre Keywords: SAT tools, pseudo boolean optimization, MAXSAT         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.

Date: 27-May-2009 Title: Formalization and Implementation of Modern SAT Solvers, Filip Marić, Journal of Automated Reasoning, Volume 43, Number 1 / june 2009 Hits: 136 Contributed by: Daniel Le Berre Keywords: null         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.