Date: 29-Aug-2010 Title: DSHARP: An open source CNF-to-dDNNF compiler based on sharpSAT. Hits: 24 Contributed by: Christian Muise Keywords: DPLL, #P, Alternative approach, SAT tools, null, null, null         DSHARP is an open source CNF-to-dDNNF compiler based on sharpSAT. Similar to the c2d software, DSHARP takes a boolean theory in conjunctive normal form as input, and compiles it into deterministic decomposable negation normal form. This paper describes the DSHARP system, and demonstrates its capabilities. More information can be found on the DSHARP website: http://www.haz.ca/research/dsharp/

Date: 28-Aug-2010 Title: Haifa Verification Conference 2010 Award to be given to the SMT-LIB/SMT-COMP initiative authors Hits: 31 Contributed by: Daniel Le Berre Keywords: Verification, SAT application, General Interest, SAT-Based, Satisfiability Modulo Theory         The HVC 2010 award winners are (alphabetically): Clark Barrett, New York University Leonardo De-Moura, Microsoft Research Silvio Ranise, FBK Trento Aaron Stump, University of Iowa Cesare Tinelli, University of Iowa The HVC award is given to the most influential work in the last five years in the scope of HVC itself, namely formal and nonformal verification. The award is not limited to influential articles; it can also be a system or a collection of activities that promote the area. The HVC award committee has decided to give the award this year to those who played a pivotal and continuous role in building and promoting the Satisfiability Modulo Theories (SMT) community. The committee recognizes the fact that the development of the SMT community, as any other community, is a joint effort of many people, but nevertheless decided to limit the award to no more than five people, and accordingly selected (alphabetically) Clark Barrett, Leonardo De Moura, Silvio Ranise, Aaron Stump, and Cesare Tinelli, for their major role in developing the SMT-LIB standard, the SMT-LIB repository, the SMT-COMP competition, the web-based server farm for SMT solvers' developers SMT-EXEC, and more generally for bringing SMT, together with others, to the place it is in today in the industry and in the academia. ... Complete award citation available on the award page.

Date: 25-Aug-2010 Title: Workshop on Tractability: Slides Online Hits: 31 Contributed by: lucas bordeaux Keywords: Complexity, Verification, Structure of problems, SAT application         Following a workshop on Tractability organized at Microsoft Research Cambridge, the slides of (most of) the invited talks are available online: http://research.microsoft.com/tractability2010/ The workshop was cross-disciplinary and gave a very exciting picture of how problem structure is exploited in computer vision, verification, machine-learning, operations research... to practically solve problems that are in general intractable. List of the Talks: Nikolaj Bjorner: Engineering Satisfiability Modulo Theories solvers for intractable problems Nadia Creignou Phase transition for the satisfiability of random (quantified) Boolean formulas Georg Gottlob Hypertree Decompositions Miki Hermann What Makes Minimal Inference Tractable John Hooker Integrating Solution Methods through Duality Peter Jeavons Presenting Constraints Tony Jebara Graphical Modeling and Machine Learning with Perfect Graphs Vladimir Kolmogorov Scalable optimization techniques for certain graphical models Andreas Krause Submodular Optimization in Machine Learning and AI Joao Marques-Silva Boolean Satisfiability Solving: Past, Present and Future Dániel Marx Fixed-Parameter Algorithms Jakob Nordström Understanding Space in Proof Complexity Lakhdar Sais Structure-based simplification techniques of Boolean formulas Paul Vitanyi Introduction to Kolmogorov complexity and applications

Date: 07-Aug-2010 Title: PCCR 2010 - Workshop on Parameterized Complexity of Computational Reasoning - Final Call for Participation Hits: 55 Contributed by: Stefan Szeider Keywords: null         CALL FOR PARTICIPATION PCCR 2010 Parameterized Complexity of Computational Reasoning Satellite Workshop of MFCS & CSL Brno, Czech Republic, 28 August 2010 http://www.kr.tuwien.ac.at/drm/pccr2010 This workshop aims to support a fruitful exchange of ideas between the research on parameterized complexity on one side and the research on various forms of computational reasoning (such as nonmonotonic, probabilistic, and constraint-based reasoning) on the other. The workshop features invited and contributed talks and presentations of surveys and new technical results. Invited speakers are: * Mike Fellows, Charles Darwin University * Nicola Galesi, Sapienza University of Rome * Gregory Gutin, University of London * Petr Hlineny, Masaryk University Brno * Reinhard Pichler, Vienna University of Technology List of Presentations: * Mike Fellows: An Overview of Parameterized Complexity and Recent Research Directions in Constraint Satisfaction and Artificial Intelligence * Gregory Gutin, Keynote Talk: Complexity of Permutation Constraint Satisfaction Problems Parameterized Above Average * Petr Hlineny: Where Myhill-Nerode Theorem meets Parameterized Algorithmics * Reinhard Pichler: Bounded Treewidth in Non-Monotonic Reasoning * M. Praveen: Does Treewidth Help in Modal Satisfiability? * Fran Rosamond: On the Complexity of Some Constraint Satisfaction Problems with Global Constraints and Convexity * Nicola Galesi: The Complexity of Proofs in Parameterized Resolution * Yijia Chen: Optimal Proof Systems, Slicewise Monotone Parameterized Problems, and Logics for PTIME For the schedule of the talks, see http://www.kr.tuwien.ac.at/drm/pccr2010/ For information on how to register and local information please consult the MFCS-CSL 2010 web-site http://mfcsl2010.fi.muni.cz/ The workshop is organized by Igor Razgon, Marko Samer, Stefan Szeider (chair), and Stefan Woltran.

Date: 31-Jul-2010 Title: Source Code Release Lingeling / Plingeling Hits: 148 Contributed by: Armin Biere Keywords: null         Source code of Lingeling and its multi-threaded front-end Plingeling has been published under GPL.

Date: 20-Jul-2010 Title: Extended Clause Learning. To appear in Artificial Intelligence. Hits: 187 Contributed by: Jinbo Huang Keywords: null, null         This paper presents a new SAT algorithm that has the full power of extended resolution. Empirical results on an initial implementation indicate that very substantial, although at this stage not necessarily consistent, improvement can be observed.

Date: 20-Jul-2010 Title: CFP: CROCS Workshop at CP-10 Hits: 78 Contributed by: Ashish Sabharwal Keywords: CSP, call for papers, Constraint Programming, null, null         Call for papers for CROCS at CP-10, the 3rd International Workshop on Constraint Reasoning and Optimization for Computational Sustainability, to be held on September 6, 2010 in St Andrews, Scotland, in conjunction with the CP-10 conference. For submission and other details, please see http://www.computational-sustainability.org/crocs-at-cp10

Date: 16-Jul-2010 Title: Parallel SAT Solving on Peer-to-Peer Desktop Grids Hits: 168 Contributed by: Sven Schulz Keywords: SAT tools, Distributed Computing, distributed parallel dynamic learning, Divide-and-Conquer Algorithms, null, null         An article on "Parallel SAT Solving on Peer-to-Peer Desktop Grids" has been published in the Journal of Grid Computing (Springer). Abstract "Satciety is a distributed parallel satisfiability (SAT) solver which focuses on tackling the domain-specific problems inherent to one of the most challenging environments for parallel computing - Peer-to-Peer Desktop Grids. Satciety efficiently addresses issues related to resource volatility and heterogeneity, limited node and network capabilities, as well as non-uniform communication costs. This is achieved through a sophisticated distributed task pool execution model, problem size reduction through multi-stage SAT formula preprocessing, context-aware memory management, and adaptive topology-aware distributed dynamic learning. Despite the demanding conditions prevailing in Desktop Grids, Satciety achieves considerable speedups compared to state-of-the-art sequential SAT solvers."

Date: 15-Jul-2010 Title: 10 PhD student positions in Computational Logic at Vienna University of Technology Hits: 118 Contributed by: Stefan Szeider Keywords: null         The Vienna University of Technology is offering 10 PhD student positions within the doctoral program "Mathematical Logic in Computer Science" which is launched in Fall 2010; five of the positions are reserved for female applicants. Further details about the program and the application procedure are available at http://www.dbai.tuwien.ac.at/drkolleg/. For additional information, please send email to dk-info@dbai.tuwien.ac.at

Date: 15-Jul-2010 Title: Pseudo Boolean evaluation results disclosed Hits: 137 Contributed by: Daniel Le Berre Keywords: General Interest         The results of the Pseudo Boolean evaluation have been disclosed. The will be a new evaluation next year.