http://www.satlive.org/Transformation of Dapp into RSSinfo@dapper.netFri, 13 Nov 2009 00:04:58 +000009-Nov-2009http://www.satlive.org/hits.jsp?id=827Summary Although this area has a history of over 80 years, it was not until the creation of efficient SAT solvers in the mid-1990s that it became practically important, finding applications in electronic design automation, hardware and software verification, combinatorial optimization, and more. Exploring the theoretical and practical aspects of satisfiability, Introduction to Mathematics of Satisfiability focuses on the satisfiability of theories consisting of propositional logic formulas. It describes how SAT solvers and techniques are applied to problems in mathematics and computer science as well as important applications in computer engineering. The book first deals with logic fundamentals, including the syntax of propositional logic, complete sets of functors, normal forms, the Craig lemma, and compactness. It then examines clauses, their proof theory and semantics, and basic complexity issues of propositional logic. The final chapters on knowledge representation cover finite runs of Turing machines and encodings into SAT. One of the pioneers of answer set programming, the author shows how constraint satisfaction systems can be worked out by satisfiability solvers and how answer set programming can be used for knowledge representation.03-Nov-2009http://www.satlive.org/hits.jsp?id=826SAT 2010 - First Call for Papers 13th International Conference on Theory and Applications of Satisfiability Testing July 11 - July 14, 2010, Edinburgh, Scotland, UK Important Dates: Abstract Submission: February 8, 2010 Paper Submission: February 15, 2010 Author Notification: March 22, 2010 Final Version: April 5, 2010 For further details see the conference website http://ie.technion.ac.il/SAT10/ SAT 2010 is part of FLoC 2010 http://www.floc-conference.org/18-Oct-2009http://www.satlive.org/hits.jsp?id=825Abstract: The best-performing algorithms for many hard problems are highly parameterized. Selecting the best heuristics and tuning their parameters for optimal overall performance is often a difficult, tedious, and unsatisfying task. This thesis studies the automation of this important part of algorithm design: the configuration of discrete algorithm components and their continuous parameters to construct an algorithm with desirable empirical performance characteristics. Automated configuration procedures can facilitate algorithm development and be applied on the end user side to optimize performance for new instance types and optimization objec- tives. The use of such procedures separates high-level cognitive tasks carried out by humans from tedious low-level tasks that can be left to machines. We introduce two alternative algorithm configuration frameworks: iterated local search in parameter configuration space and sequential optimization based on response surface models. To the best of our knowledge, our local search approach is the first that goes beyond local optima. Our model-based search techniques significantly outperform existing techniques and extend them in ways crucial for general algorithm configuration: they can handle categorical parameters, optimization objectives defined across multiple instances, and tens of thousands of data points. We study how many runs to perform for evaluating a parameter configuration and how to set the cutoff time, after which algorithm runs are terminated unsuccessfully. We introduce data-driven approaches for making these choices adaptively, most notably the first general method for adaptively setting the cutoff time. Using our procedures—to the best of our knowledge still the only ones applicable to these complex configuration tasks—we configured state-of-the-art tree search and local search algorithms for SAT, as well as CPLEX, the most widely-used commercial optimization tool for solving mixed integer programs (MIP). In many cases, we achieved improvements of orders of magnitude over the algorithm default, thereby substantially improving the state of the art in solving a broad range of problems, including industrially relevant instances of SAT and MIP. Based on these results, we believe that automated algorithm configuration procedures, such as ours, will play an increasingly crucial role in the design of high-performance algorithms and will be widely used in academia and industry.14-Oct-2009http://www.satlive.org/hits.jsp?id=823Important dates - The deadline for registration is October 15st (unchanged). - The new deadline for solvers and formulas submission is October 31st (NEW). Only registered participants can send their contribution.23-Sep-2009http://www.satlive.org/hits.jsp?id=822Greetings, CFP submission in the Special issue "Satisfiability Based Computing" for the Journal of Advances In Information Technology. We shall appreciate your efforts to contribute for the special issue of JAIT. With Kind Regards, Dr Ateet Bhalla and Dr Xishun Zhao Guest Editors, Special Issue, JAIT.02-Sep-2009http://www.satlive.org/hits.jsp?id=8212009 CAV Award Announcement August 30, 2009 Contact: Randal E. Bryant, Carnegie Mellon University (Randy.Bryant@cs.cmu.edu) The 2009 CAV (Computer-Aided Verification) award was presented on June 29, 2009 at the 21st annual CAV conference in Grenoble, France to seven individuals who made major advances in creating high-performance Boolean satisfiability solvers. The annual award, which recognizes a specific fundamental contribution or series of outstanding contributions to the CAV field, was given to Conor F. Madigan, Kateeva, Inc.; Sharad Malik, Princeton University; Joao P. Marques-Silva, University College Dublin, Ireland; Matthew W. Moskewicz, University of California, Berkeley; Karem A. Sakallah, University of Michigan; Lintao Zhang, Microsoft Research and Ying Zhao, Wuxi Capital Group. The award includes a $10,000 prize and was presented with the citation: “For fundamental contributions to the development of high-performance Boolean satisfiability solvers.” The CAV conference is the premier international event for reporting research on Computer Aided Verification, a subdiscipline of Computer Science that is concerned with ensuring that software and hardware systems operate correctly and reliably. The CAV award was established in 2008 by the conference’s steering committee and was given this year for the second time. Work Being Recognized The seven recipients of this year’s award worked in two different teams, one at the University of Michigan and one at Princeton University, where they created powerful programs for checking whether a logic formula has a consistent solution. This is known as a ”Boolean satisfiability problem” and is named for the 19th century British logician George Boole. Their work touched off a flurry of activity that continues to this day. Teams from around the world compete to produce new satisfiability solvers, or “SAT solvers,” that can solve the most difficult problems, and to find new ways to apply these solvers to a variety of practical problems. SAT solvers can be used to solve a number of different problems, where many constraints are imposed and it must be determined if there is any way of satisfying all of them. For example, the rules for a 9x9 Sudoku puzzle can be expressed as a number of constraints: that each square is assigned a number between 1 and 9, that no row or column contain any repeated digits, that no 3x3 square contain any repeated digits, and that some of the squares have predetermined values. These rules can all be expressed as a collection of around 12,000 constraints, which can readily be solved in around 0.01 seconds using a modern SAT solver.31-Aug-2009http://www.satlive.org/hits.jsp?id=820Abstract. In this work, we improve on existing work that studied the relationship between the proof system of modern SAT solvers and general resolution. Previous contributions such as those by Beame et al (2004), Hertel et al (2008), and Buss et al (2008) demonstrated that variations on modern clause-learning SAT solvers were as powerful as general res- olution. However, the models used in these studies required either extra degrees of non-determinism or a preprocessing step that are not utilized by any state-of-the-art SAT solvers in practice. In this paper, we prove that modern SAT solvers that learn asserting clauses indeed p-simulate general resolution without the need for any additional techniques. That paper got the best student paper award, and was a runner-up for the best paper at CP 200925-Aug-2009http://www.satlive.org/hits.jsp?id=819(sorry for double post, I resubmitted due to bad formatting...) RegSTAB is a SAT-solver able to deal with formulae patterns e.g. you can give it the pattern "P_1 / /i=1..n (P_i -> P_i+1) / -P_n" and RegSTAB will be able to tell you that this is unsatisfiable for all n>0 Main Page Manual A Schemata Calculus for Propositional Logic, by Vincent Aravantinos, Ricardo Caferra, and Nicolas Peltier , TABLEAUX 200925-Aug-2009http://www.satlive.org/hits.jsp?id=818RegSTAB is a SAT-solver able to deal with formulae patterns e.g. you can give it the pattern "P_1 / /i=1..n (P_i -> P_i+1) / -P_n" and RegSTAB will be able to tell you that this is unsatisfiable for all n>0 Main Page Manual A Schemata Calculus for Propositional Logic, by Vincent Aravantinos, Ricardo Caferra, and Nicolas Peltier , TABLEAUX 200918-Aug-2009http://www.satlive.org/hits.jsp?id=817Random QBFs track added at QBFEVAL'10. For all informations, please visit the QBFEVAL web portal (www.qbfeval.org).